Coq master builds fail using the simple CI workflow

[palmskog]

I'm using the Nix toolbox-based simple CI workflow that @Zimmi48 set up for our templates. However, the Coq master CI builds now give errors like this:

Findlib error: zarith not found in:
/nix/store/z5g7xb2ql05idyicf7c2r9h2c7l2rsfx-coq-dev/lib/coq/../coq-core/..
/nix/store/z5g7xb2ql05idyicf7c2r9h2c7l2rsfx-coq-dev/lib/coq/user-contrib/Ltac2
/nix/store/q8xz588kv95cr7kwzpg6kdsm50h6kmcj-ocaml-findlib-1.9.1/lib/ocaml/4.12.0/site-lib
required by `coq-core.interp'

All of this is probably related to the findlib changes in Coq.

Recall that the simple CI workflow makes the following invocation:

nix-build https://coq.inria.fr/nix/toolbox --argstr job huffman --arg override '{ ${{ matrix.overrides }}; huffman = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'

[CohenCyril]

@proux01 @gares since you've looked into this recently, is it related to coq/coq#15220 ?

[Zimmi48]

Yes, AFAICS this is the same issue.

The OCAMLPATH as displayed by the findlib error is missing the location where zarith is installed. Could it be that Coq is overriding it?

[gares]

there was another report saying that OCAMLPATH is only filled in by nix in "dev" (or maybe "build") mode, but is otherwise empty.
The paths seem almost empty there, no?

[gares]

I recall all ocaml paths to be coaleshed via OCAMLPATH, there I only have the config of findlib and the 2 added by coq.

[Zimmi48]

The other related discussion was this one: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Findlib.20error.20with.20master.20.2B.20nix

Indeed, the errors look very similar. Furthermore, what I hadn't realized so far was that it's not the build of Coq that makes these CI jobs fail, it's the build of Coq packages. Thus, the explanation might be that until now, we've put packages such as zarith in the buildInputs but now they should be in the propagatedBuildInputs (in the case of opam, every build input is "propagated" so this kind of issues do not show up).

[whonore]

A potential fix might be to set OCAMLPATH with wrapProgram. As a quick test I tried nix-build with the following file and running ./result/bin/coqtop no longer prints the findlib error, but ./result/bin/coqc still does since I didn't wrap it.

{ pkgs ? import <nixpkgs> { } }:

(pkgs.coq.override { version = "master"; }).overrideAttrs (old: {
  postInstall = old.postInstall + ''
    wrapProgram $out/bin/coqtop --prefix OCAMLPATH : $OCAMLPATH
  '';
})

Some similar examples in nixpkgs:

• https://github.com/NixOS/nixpkgs/blob/be5974a48ccd39111bfb6557054f1854f863ae17/pkgs/development/compilers/reason/default.nix#L46
• https://github.com/NixOS/nixpkgs/blob/be5974a48ccd39111bfb6557054f1854f863ae17/pkgs/development/ocaml-modules/bap/default.nix#L60

[Zimmi48]

This is not the first time that this dependency is moved from non-propagated to propagated BTW, but this might have been reverted as part of changes discussed in NixOS/nixpkgs#105877 (comment).

[Zimmi48]

Indeed, @whonore is probably right that the best fix needs to take into account the use where Coq is run outside an environment which can set up OCAMLPATH, so such wrapping might be necessary. My suggestion to move zarith to the propagated dependencies would probably only have fixed the use case from within nix-build / nix-shell (I'm not using the experimental Nix 2.0 command-line, so I am not sure which command the latter corresponds to, but perhaps nix develop).

[Zimmi48]

cc @vbgl BTW

[gares]

wrapProgram $out/bin/coqtop --prefix OCAMLPATH : $OCAMLPATH

can someone post here the resulting wrapper?

[whonore]

can someone post here the resulting wrapper?

bin/coqtop

#! /nix/store/phqa311klldrcbwid1i22dwnpfc9dnma-bash-5.1-p8/bin/bash -e
export GIO_EXTRA_MODULES='/nix/store/s56s1cjix45c560q6i14n29i2y3ihyy8-dconf-0.40.0-lib/lib/gio/modules'${GIO_EXTRA_MODULES:+':'}$GIO_EXTRA_MODULES
export GDK_PIXBUF_MODULE_FILE='/nix/store/v8y7sskf8xm10lr4sx2dv42v3kn9vkgz-librsvg-2.52.0/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache'
export XDG_DATA_DIRS='/nix/store/wrh9c2h8aban3fnn8q4f9rv83s0id6k8-cups-2.3.3op2/share:/nix/store/rpcfc4iynhjn64ixfqmfxsira6qn37pr-gtk+3-3.24.30/share:/nix/store/ywm3qsy3slfas0lh0m4r2lrdq932xi58-adwaita-icon-theme-41.0/share:/nix/store/n6x9d45c8p3ajklw3akb4xz8m6l1vqq0-hicolor-icon-theme-0.17/share'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
export XDG_DATA_DIRS='/nix/store/06lpzmck907k8rzxccxkn8iizcy3xx1q-gsettings-desktop-schemas-41.0/share/gsettings-schemas/gsettings-desktop-schemas-41.0:/nix/store/rpcfc4iynhjn64ixfqmfxsira6qn37pr-gtk+3-3.24.30/share/gsettings-schemas/gtk+3-3.24.30'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
export XDG_DATA_DIRS='/nix/store/41wkxvqi0khl4v9x35yggai8hkqm0k85-coq-dev/share'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
exec -a "$0" "/nix/store/41wkxvqi0khl4v9x35yggai8hkqm0k85-coq-dev/bin/.coqtop-wrapped_"  "$@"

bin/.coqtop-wrapped_

#! /nix/store/phqa311klldrcbwid1i22dwnpfc9dnma-bash-5.1-p8/bin/bash -e
export OCAMLPATH='/nix/store/jl2wyvb25nfyryq1l2n57yx934a3ablv-ocaml-findlib-1.9.1/lib/ocaml/4.10.2/site-lib/:/nix/store/h5clycwllwxjw9c8brlaxwlydmsmnraz-ocaml4.10.2-zarith-1.12/lib/ocaml/4.10.2/site-lib/:/nix/store/kffpnia3i1aksbc4kfk51zvsnhiv8d5b-ocaml4.10.2-lablgtk3-sourceview3-3.1.1/lib/ocaml/4.10.2/site-lib/:/nix/store/g54j8j9virjswmpcspdi1sm9cjvd340z-ocaml4.10.2-lablgtk3-3.1.1/lib/ocaml/4.10.2/site-lib/:/nix/store/8wlr90zi7wh3b9d9xj97p5vynbbxjbfw-ocaml4.10.2-cairo2-0.6.2/lib/ocaml/4.10.2/site-lib/:/nix/store/bgn8m285k45cbjsnps353jly13franwx-dune-2.9.1/lib/ocaml/4.10.2/site-lib/'${OCAMLPATH:+':'}$OCAMLPATH
exec -a "$0" "/nix/store/41wkxvqi0khl4v9x35yggai8hkqm0k85-coq-dev/bin/.coqtop-wrapped"  "$@"

bin/.coqtop-wrapped

#! /nix/store/phqa311klldrcbwid1i22dwnpfc9dnma-bash-5.1-p8/bin/bash -e
export GIO_EXTRA_MODULES='/nix/store/s56s1cjix45c560q6i14n29i2y3ihyy8-dconf-0.40.0-lib/lib/gio/modules'${GIO_EXTRA_MODULES:+':'}$GIO_EXTRA_MODULES
export GDK_PIXBUF_MODULE_FILE='/nix/store/v8y7sskf8xm10lr4sx2dv42v3kn9vkgz-librsvg-2.52.0/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache'
export XDG_DATA_DIRS='/nix/store/wrh9c2h8aban3fnn8q4f9rv83s0id6k8-cups-2.3.3op2/share:/nix/store/rpcfc4iynhjn64ixfqmfxsira6qn37pr-gtk+3-3.24.30/share:/nix/store/ywm3qsy3slfas0lh0m4r2lrdq932xi58-adwaita-icon-theme-41.0/share:/nix/store/n6x9d45c8p3ajklw3akb4xz8m6l1vqq0-hicolor-icon-theme-0.17/share'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
export XDG_DATA_DIRS='/nix/store/06lpzmck907k8rzxccxkn8iizcy3xx1q-gsettings-desktop-schemas-41.0/share/gsettings-schemas/gsettings-desktop-schemas-41.0:/nix/store/rpcfc4iynhjn64ixfqmfxsira6qn37pr-gtk+3-3.24.30/share/gsettings-schemas/gtk+3-3.24.30'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
export XDG_DATA_DIRS='/nix/store/41wkxvqi0khl4v9x35yggai8hkqm0k85-coq-dev/share'${XDG_DATA_DIRS:+':'}$XDG_DATA_DIRS
exec -a "$0" "/nix/store/41wkxvqi0khl4v9x35yggai8hkqm0k85-coq-dev/bin/..coqtop-wrapped-wrapped"  "$@"

[gares]

I guess it is well founded...

[gares]

More seriously, I don't see OCAMLPATH there

[whonore]

More seriously, I don't see OCAMLPATH there

Line 2 of bin/.coqtop-wrapped_

[gares]

oh right, then it looks ok to me

[gares]

I've been thinking about this and I don't get how all the relevant paths could be there (disclaimer, I don't know nix).
When is the wrapping actually done? My worry is the following: I have coq installed, then I install, say, coq-elpi which has his own files in .../lib/ocaml/4.10.2/site-libs. How is this path visible to coqtop? Is the wrap redone every time a package setting OCAMLPATH gets installed in the current shell?

[vbgl]

[…] coq-elpi […] has his own files in .../lib/ocaml/4.10.2/site-libs. How is this path visible to coqtop?

It is not.

Is the wrap redone every time a package setting OCAMLPATH gets installed in the current shell?

No. The nix store is read-only. Moreover, nix package management is functional: if you do A and then B, the execution of B cannot have any effect on the result of A.

[gares]

So, how do you deal with plugins in general? I mean, Coq is not the only piece of software with addons that are packaged separately. How is the main program supposed to find them?

[CohenCyril]

AFAIU, the $COQPATH environement variable is currently augmented via a hook: every installed package declares itself upon addition to the shell/build environement.
In other ecosystems, there are some sorts of meta-derivation generators (which I never completely understood, so excuse my approximate vocabulary) which take a set of package and generate a wrapper for the main program together with the packages, I'd love to avoid that, cannot we put hooks for ocaml packages?

[gares]

Moreover, nix package management is functional: if you do A and then B, the execution of B cannot have any effect on the result of A.

So... I guess hooks make this less true ;-)

[CohenCyril]

@vbgl is what I said correct?

[Zimmi48]

Basically, there are two ways of using Coq in Nix: either you install it or you load an environment with it with commands such as nix-shell. With the former, it used to work as long as you were not using any external Coq packages. The latter is the only solution if you need external Coq packages (and this is fine because this is how things are supposed to work in Nix).

The wrapper solution would solve the issue that now the former apparently does not work anymore. It would not change the fact that you still need to create an environment (that can populate OCAMLPATH) if you want external Coq packages (unless with implement coqWithPackages as mentioned by Cyril, but I would also rather avoid that).

[vbgl]

I’ve seen three different mechanisms.

1. Non-recommended, imperative style. I use this for some emacs packages.
   Plug-ins are globally installed in the user profile (which is mutable) at a predictable location. Said location is hard-coded in the main package or in its configuration file.
   When I install why3 (using e.g., nix-env -iA nixpkgs.why3), this creates a symlink ~/.nix-profile/share/emacs/site-lisp/why3.el to the (immutable) nix store and in my .emacs I have (add-to-list 'load-path "~/.nix-profile/share/emacs/site-lisp").
   In practice it’s a pain: hard to debug, you have to manually ensure that all paths are consistent, etc.

2. The withPlugins pattern. Used for instance for why3 provers (https://github.com/NixOS/nixpkgs/blob/21.11/pkgs/applications/science/logic/why3/with-provers.nix) or for python libraries (https://nixos.org/manual/nixpkgs/stable/#ad-hoc-temporary-python-environment-with-nix-shell).
   The main package is “naked” (without any plug-in) and there is a nix function to generate a package with the plug-ins that you give as arguments. So for each set of plug-ins, said function can produce the ad-hoc package with exactly this set of plug-ins available. Building this package usually requires no compilation: it’s just a matter of setting environment variables, symbolic links, and writing proper configuration files.
   This is very robust and also convenient: you can use the software-with-plug-ins as a regular package, embed it in a larger environment without issues. It is also very flexible because the ad-hoc package is written in nix (the programming language) and can use various tricks (env var, conf file, hard link, etc).

3. The “hook” pattern. Used for OCaml and Coq libraries.
   The main software can be configured through an environment variable. The hook is a shell script that will populate this environment variable. Whenever an environment is created that includes the hook, the hook is run and receives as arguments the other inputs to the environment.
   This is very similar to the previous case but the hook is written in bash and can only change environment variables (in fact a shell program can do whatever but the user might not appreciate).

What Cyril wrote is correct and does not contradict what I had written before.

[Zimmi48]

It looks like the fact that zarith is not propagated / available when building a Coq library might not be the only issue here. As I wrote in coq/coq#15718, I also get this error while trying to run make -j4 plugin_tutorial in the Coq repository from within a nix-shell. And yet, ocamlfind -query zarith works and reports the location of zarith, so I'm thinking the OCAMLPATH is incorrectly overridden by the Coq (coq_makefile?) build system. (this looks specific to the plugin_tutorial target according to coq/coq#15718 (comment))

[whonore]

Has a decision been reached on how to solve this?

[Zimmi48]

@CohenCyril has worked on NixOS/nixpkgs#161977 to propagate the OCaml build inputs. This will solve the issue initially reported here (CI builds failing) but might not solve the issue in general. In particular, that it is no longer be possible to use a globally installed Coq. When 8.16 is released, this is likely to be considered a serious regression for many users, and we should at least add a wrapper so that Coq alone can be run as it used to, when it is globally installed.

[gares]

What do you mean to use a global coq installation ? Is that nix only?

[Zimmi48]

Is that nix only?

Quite the opposite, what I mean is using a Coq installed in the global environment rather than in a local nix-shell, so this corresponds to the most standard non-Nix way of doing.