Nix package for coq theories with dependencies

Miscellaneous
1

I am new to the nix package manager, so perhaps this question is trivial.

I want to add coq-itree to coqPackages in nixpkgs but building fails because it can’t find the Paco and ExtLib libraries.

I have already fixed the nix files for those two by updating their nix files in a local copy of the nixpkgs, so this works:

env NIX_PATH=$HOME/HACK nix-shell --packages coqPackages_8_13.{coq,coq-ext-lib,paco}

but adding coq-itree fails

env NIX_PATH=$HOME/HACK nix-shell --packages coqPackages_8_13.{coq,coq-ext-lib,paco,coq-itree}

I think the problem is how I build.

How to I write in the nix file so that it requires coq-ext-lib and paco to be installed?

This is what I have in the nix file so far:

cat HACK/nixpkgs/pkgs/development/coq-modules/coq-itree/default.nix


{ lib, mkCoqDerivation, coq, version ? null }:

with lib; mkCoqDerivation rec {
  pname = "InteractionTrees";
  owner = "DeepSpec";
  inherit version;
  defaultVersion = with versions; switch coq.coq-version [
    { case = range "8.10" "8.13";  out = "4.0.0"; }
  ] null;
  release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
  releaseRev = v: "${v}";

  meta = {
    description = "A Library for Representing Recursive and Impure Programs in Coq";
    maintainers = with maintainers; [ lysxia ];
  };
}
1 Like
2

AFAICS, all you need to do is adding a propagatedBuildInputs = [ coq-ext-lib paco ] line in the attributes that you give to mkCoqDerivation and extending the arguments of the function at the beginning of the file ({ lib, mkCoqDerivation, coq, coq-ext-lib, paco, version ? null }:).

Let me know if that still doesn’t work.

2 Likes
3

It worked like a charm! Thanks!

1 Like