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 rocq-prover/rocq#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