Emilio Jesús Gallego Arias (Mar 01 2021 at 23:11): 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?
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
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
Emilio Jesús Gallego Arias (Mar 01 2021 at 23:26):Trying pkgs.breakpointHook
Emilio Jesús Gallego Arias (Mar 01 2021 at 23:29):I called nix-build twice and no re-use happened, :( :(
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
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?
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.
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.
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.
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.
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).
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...
Théo Zimmermann (Mar 02 2021 at 10:06):I'm trying to re-run the test-suite with this change.
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...
Théo Zimmermann (Mar 02 2021 at 10:24):But I'll try to compare with how it works in master.
Vincent Laporte (Mar 02 2021 at 10:43):Hi, I’m trying to understand what’s going on…
Théo Zimmermann (Mar 02 2021 at 10:45):So basically the build in master confirms that ocamlfind -query coq already didn't work.
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.
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//
Vincent Laporte (Mar 02 2021 at 10:46):IIUC, the test-suite does not use ocamlfind to find the coq (OCaml) library.
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?
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.
Vincent Laporte (Mar 02 2021 at 10:53):tools/CoqMakefile.in:COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)")
Vincent Laporte (Mar 02 2021 at 10:54):And this variable is then appended to CAMLFLAGS
Vincent Laporte (Mar 02 2021 at 10:55):Unfortunately, the COQCORELIB variable is not properly set…
Gaëtan Gilbert (Mar 02 2021 at 10:56):the test suite does whatever coq_makefile does I think
Vincent Laporte (Mar 02 2021 at 11:27):I have two patches that both fix the issue (but may introduce other…):
--- 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;
--- 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;
This .. business looks wrong, can't we have a separate coqcorelib()?
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.
Enrico Tassi (Mar 02 2021 at 13:29):We should fix 1. , setting COQMF_COQCORELIB is like working around the bug 1 would fix
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.
Vincent Laporte (Mar 02 2021 at 13:52):So the culprit is line 49
COQLIB := $(shell ocaml ocaml_pwd.ml ..)
Vincent Laporte (Mar 02 2021 at 13:55):(or the guard on the preceding line that is true too often)
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)
Vincent Laporte (Mar 02 2021 at 13:58):Cool. Thanks.
Emilio Jesús Gallego Arias (Mar 02 2021 at 13:58):The local mode is about to disappear too hopefully
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: Dec 07 2023 at 09:01 UTC