Stream: Coq devs & plugin devs

Topic: Debugging a Nix problem


view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 23:11):

Hi folks, I just installed Nix to debug the build problem I'm seeing in https://github.com/coq/coq/pull/12567

I want to get to the shell where the right context the test suite is gonna be run is present, how can I do that?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 23:12):

I'm reading the documentation of nix-shell , I guess that's the answer, but not sure what is the right nix-build checkpoint

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 23:15):

I will also update the nix part to build https://github.com/coq/coq/pull/13617

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 23:26):

Trying pkgs.breakpointHook

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 23:29):

I called nix-build twice and no re-use happened, :( :(

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 00:17):

I'll ping @Théo Zimmermann @Vincent Laporte just in case they have a minute

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 08:33):

Sorry about that. Nix builds can be hard to debug. I can try to help debug this. But IINM, it's the only job that tests running the test-suite after installation. So, have you tried to do this manually in another context?

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 08:40):

And unfortunately, incrementality in Nix is at the derivation / package level, so there is no benefit if the package fails, even during the installCheck phase. What we could do though would be to remove this installCheck and run the test-suite separately, after the package has been installed.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 08:40):

We could also do a splitting of the Nix package similar to the one of the opam packages.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 09:22):

In principle, nix-build . -K allows keeping build outputs and reproducing the build environment. I'm running it now. We'll see.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 09:54):

I've cd into this directory and loaded the environment of the build (. env-vars). ocamlfind is there but ocamlfind query coq or ocamlfind query coq-core do not work.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 09:55):

Though $out/bin/coqtop works fine (doesn't complain about not finding the stdlib or anything).

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:02):

Re-running the last line of preInstallCheck (export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH) then ocamlfind -query coq-core seems to fix the issue...

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:06):

I'm trying to re-run the test-suite with this change.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:24):

So I'm not enough of a Nix expert to know how to properly rebuild the test-suite in this updated context and to explain why the export OCAMLPATH line was not taken into account previously...

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:24):

But I'll try to compare with how it works in master.

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:43):

Hi, I’m trying to understand what’s going on…

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:45):

So basically the build in master confirms that ocamlfind -query coq already didn't work.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:45):

And for some mysterious reasons, the test-suite still went through fine, which it does not after the stdlib splitting PR.

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:45):

What the coqlib function from lib/envars.ml is expected to return? I can see the following in some Makefile.conf generated during the execution of the test-suite:

COQMF_COQLIB=/build/pr-12567/
COQMF_COQCORELIB=/build/pr-12567/../coq-core//

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:46):

IIUC, the test-suite does not use ocamlfind to find the coq (OCaml) library.

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:50):

Vincent Laporte said:

IIUC, the test-suite does not use ocamlfind to find the coq (OCaml) library.

That's the core question then, because @Emilio Jesús Gallego Arias claimed it does. Could it be that this changed in Emilio's PR?

view this post on Zulip Théo Zimmermann (Mar 02 2021 at 10:52):

Vincent Laporte said:

IIUC, the test-suite does not use ocamlfind to find the coq (OCaml) library.

Do you recall how it works? Maybe @Enrico Tassi or @Gaëtan Gilbert know.

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:53):

tools/CoqMakefile.in:COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)")

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:54):

And this variable is then appended to CAMLFLAGS

view this post on Zulip Vincent Laporte (Mar 02 2021 at 10:55):

Unfortunately, the COQCORELIB variable is not properly set…

view this post on Zulip Gaëtan Gilbert (Mar 02 2021 at 10:56):

the test suite does whatever coq_makefile does I think

view this post on Zulip Vincent Laporte (Mar 02 2021 at 11:27):

I have two patches that both fix the issue (but may introduce other…):

  1. change the default value of COQCORELIB (current value is wrong; proposed value is also wrong; someone may know a correct value…).
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -205,7 +205,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   let open Printf in
   fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
-  fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (if Coq_config.local then coqlib () else coqlib () / "../coq-core/");
+  fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib ());
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
  1. Override the wrong value of COQCORELIB when running the test-suite in nix:
--- a/default.nix
+++ b/default.nix
@@ -109,6 +109,7 @@ stdenv.mkDerivation rec {
   '';

   installCheckTarget = [ "check" ];
+  installCheckFlags = [ "COQMF_COQCORELIB=$(OCAMLFIND_DESTDIR)/coq-core" ];

   passthru = {
     inherit coq-version ocamlPackages;

view this post on Zulip Gaëtan Gilbert (Mar 02 2021 at 11:28):

This .. business looks wrong, can't we have a separate coqcorelib()?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 13:16):

Yup, gonna add a coqcorelib function so things are clearer, thanks @Vincent Laporte for having a look to the problem, for some reason the call to coqlib does work fine when running the test-suite manually in this context [returns the install path] so I wonder why on Nix is returning the source directory.

view this post on Zulip Enrico Tassi (Mar 02 2021 at 13:29):

We should fix 1. , setting COQMF_COQCORELIB is like working around the bug 1 would fix

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 13:43):

Indeed, I found the problem, the test suite makefile sets COQLIB incorrectly when not in local mode, in this case COQLIB should be specified.

view this post on Zulip Vincent Laporte (Mar 02 2021 at 13:52):

So the culprit is line 49
COQLIB := $(shell ocaml ocaml_pwd.ml ..)

view this post on Zulip Vincent Laporte (Mar 02 2021 at 13:55):

(or the guard on the preceding line that is true too often)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 13:57):

Yes, that's the culprit @Vincent Laporte , I am improving the logic here (hopefully)

view this post on Zulip Vincent Laporte (Mar 02 2021 at 13:58):

Cool. Thanks.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 13:58):

The local mode is about to disappear too hopefully

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2021 at 13:58):

thanks to you, I didn't spot that problem without your help


Last updated: Oct 16 2021 at 07:02 UTC