search

coq-community / coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
MIT License
32 stars 10 forks source link

Coq master builds fail using the simple CI workflow #95

Open palmskog opened 2 years ago

palmskog commented 2 years ago

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 commented 2 years ago

@proux01 @gares since you've looked into this recently, is it related to https://github.com/coq/coq/pull/15220 ?

Zimmi48 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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:

Zimmi48 commented 2 years ago

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 https://github.com/NixOS/nixpkgs/pull/105877#discussion_r542365347.

Zimmi48 commented 2 years ago

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 commented 2 years ago

cc @vbgl BTW

gares commented 2 years ago 
wrapProgram $out/bin/coqtop --prefix OCAMLPATH : $OCAMLPATH

can someone post here the resulting wrapper?

whonore commented 2 years ago

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 commented 2 years ago

I guess it is well founded...

gares commented 2 years ago

More seriously, I don't see OCAMLPATH there

whonore commented 2 years ago

More seriously, I don't see OCAMLPATH there

Line 2 of bin/.coqtop-wrapped_

gares commented 2 years ago

oh right, then it looks ok to me

gares commented 2 years ago

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 commented 2 years ago

[…] 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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

@vbgl is what I said correct?

Zimmi48 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 https://github.com/coq/coq/issues/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 https://github.com/coq/coq/issues/15718#issuecomment-1047051692)

whonore commented 2 years ago

Has a decision been reached on how to solve this?

Zimmi48 commented 2 years ago

@CohenCyril has worked on https://github.com/NixOS/nixpkgs/pull/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 commented 2 years ago

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

Zimmi48 commented 2 years ago

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.