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?
I'm reading the documentation of nix-shell , I guess that's the answer, but not sure what is the right nix-build checkpoint
I will also update the nix part to build https://github.com/coq/coq/pull/13617
Trying pkgs.breakpointHook
I called nix-build twice and no re-use happened, :( :(
I'll ping @Théo Zimmermann @Vincent Laporte just in case they have a minute
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?
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.
We could also do a splitting of the Nix package similar to the one of the opam packages.
In principle, nix-build . -K
allows keeping build outputs and reproducing the build environment. I'm running it now. We'll see.
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.
Though $out/bin/coqtop
works fine (doesn't complain about not finding the stdlib or anything).
Re-running the last line of preInstallCheck
(export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH
) then ocamlfind -query coq-core
seems to fix the issue...
I'm trying to re-run the test-suite with this change.
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...
But I'll try to compare with how it works in master
.
Hi, I’m trying to understand what’s going on…
So basically the build in master
confirms that ocamlfind -query coq
already didn't work.
And for some mysterious reasons, the test-suite still went through fine, which it does not after the stdlib splitting PR.
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//
IIUC, the test-suite does not use ocamlfind to find the coq (OCaml) library.
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?
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.
tools/CoqMakefile.in:COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)")
And this variable is then appended to CAMLFLAGS
Unfortunately, the COQCORELIB variable is not properly set…
the test suite does whatever coq_makefile does I think
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()
?
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.
We should fix 1. , setting COQMF_COQCORELIB is like working around the bug 1 would fix
Indeed, I found the problem, the test suite makefile sets COQLIB incorrectly when not in local mode, in this case COQLIB should be specified.
So the culprit is line 49
COQLIB := $(shell ocaml ocaml_pwd.ml ..)
(or the guard on the preceding line that is true too often)
Yes, that's the culprit @Vincent Laporte , I am improving the logic here (hopefully)
Cool. Thanks.
The local mode is about to disappear too hopefully
thanks to you, I didn't spot that problem without your help
Last updated: May 31 2023 at 15:01 UTC