Stream: Nix toolbox devs & users

Topic: ✔ Findlib error with master + nix

Wolf Honore (Feb 09 2022 at 14:27):

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'

Guillaume Melquiond (Feb 09 2022 at 14:34):

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?

Wolf Honore (Feb 09 2022 at 14:39):

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

Wolf Honore (Feb 09 2022 at 14:41):

But this wasn't an issue for me until very recently so I'm not sure what changed

Guillaume Melquiond (Feb 09 2022 at 14:42):

The use of findlib in Coq is relatively new.

Théo Zimmermann (Feb 09 2022 at 14:47):

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

Théo Zimmermann (Feb 09 2022 at 14:48):

This was also discussed here: https://github.com/coq/coq/pull/15220#issuecomment-1030597338

Théo Zimmermann (Feb 09 2022 at 14:49):

I have unfortunately been too busy myself to look into this yet.

Enrico Tassi (Feb 09 2022 at 15:03):

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

Lars Rasmusson (Jul 08 2022 at 12:59):

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"; }

Paolo Giarrusso (Jul 08 2022 at 13:49):

@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

Lars Rasmusson (Jul 08 2022 at 13:56):

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 !

Emilio Jesús Gallego Arias (Jul 08 2022 at 16:14):

@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.

Notification Bot (Jul 08 2022 at 18:48):

This topic was moved here from #Coq devs & plugin devs > Findlib error with master + nix by Théo Zimmermann.

Notification Bot (Jul 12 2022 at 20:30):

Wolf Honore has marked this topic as resolved.

Last updated: Jun 11 2023 at 01:30 UTC