Stream: Coq devs & plugin devs

Topic: Findlib error with master + nix


view this post on Zulip 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'

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Feb 09 2022 at 14:42):

The use of findlib in Coq is relatively new.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 09 2022 at 14:48):

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

view this post on Zulip Théo Zimmermann (Feb 09 2022 at 14:49):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jul 08 2022 at 18:48):

This topic was moved to #Nix toolbox devs & users > Findlib error with master + nix by Théo Zimmermann.


Last updated: Feb 02 2023 at 13:03 UTC