If I install Coq master through nix (e.g., nix shell --impure --expr 'let pkgs = import <nixpkgs> {}; in pkgs.coq.override { version = "master"; }'
), I get an error about zarith when I try to run coqtop.
> coqtop
Welcome to Coq 8.16+alpha
Error:
Findlib error: zarith not found in:
/nix/store/k4728jpg7i8mvik8fvdfjglklp52ah4y-coq-dev/lib/coq/../coq-core/..
/nix/store/k4728jpg7i8mvik8fvdfjglklp52ah4y-coq-dev/lib/coq/user-contrib/Ltac2
/nix/store/jl2wyvb25nfyryq1l2n57yx934a3ablv-ocaml-findlib-1.9.1/lib/ocaml/4.10.2/site-lib
required by `coq-core.interp'
Can you do echo $OCAMLPATH
? According to Nix' documentation, "A hook in the findlib package will automatically populate this variable with the paths to the other libraries." But it seems like this is not the case for you, is it?
It seems to be an issue with using nix shell
vs nix develop
. In nix shell
$OCAMLPATH
is empty, but with nix develop
it gets populated and coqtop
works
But this wasn't an issue for me until very recently so I'm not sure what changed
The use of findlib
in Coq is relatively new.
We have already noticed some related breakage on CI jobs since the findlib change. Example: https://github.com/coq-community/reglang/runs/5120238256?check_suite_focus=true
This was also discussed here: https://github.com/coq/coq/pull/15220#issuecomment-1030597338
I have unfortunately been too busy myself to look into this yet.
Since OCAMLPATH is also used to load plugins (not just in Coq), I guess it's a bug to empty it in non-dev mode
I'm trying to build a specific coq git-version with nix. What is the right way to do ?
nix-shell -E 'with import <nixpkgs> {}; mkShell { buildInputs = [ (coq.override {version = "V8.16+rc1"; }) ];}'
works, but
nix-shell -E 'with import <nixpkgs> {}; mkShell { buildInputs = [ (coq.override {version = "master"; }) ];}'
gives the error
make: *** No rule to make target 'revision'. Stop.
--
Some more digging shows that the file Makefile.common (which specifies the target revision
) was removed in commit c17390f30fca3. So I can build earlier coq versions, i.e.
(coq.override {version = "09e32cace56219c131b6a162401783c165797870"; }
@Lars Rasmusson AFAICT as a clueless outsider, Nixpkgs had to be updated (recently) for the new Coq build system —
https://coq.zulipchat.com/#narrow/stream/290990-Nix-toolbox-devs-.26-users/topic/Update.20for.20Coq.208.2E17.2Balpha points to https://github.com/NixOS/nixpkgs/pull/180370 which was _just_ merged
Wow, I just did a pull of the most recent nixpkgs, and now it seems I can build (coq.override { version = "672b1443441df4e4777c4d2f7f6fb953bd97544a"; })
Big thanks to the authors of the patch @Théo Zimmermann ! And for the info @Paolo Giarrusso !
@Wolf Honore we've been using findlib to detect zarith
for years, so indeed, if Nix returns a bad list when running ocamlfind list
, Coq won't work.
This topic was moved here from #Coq devs & plugin devs > Findlib error with master + nix by Théo Zimmermann.
Wolf Honore has marked this topic as resolved.
Last updated: Jun 11 2023 at 01:30 UTC