due to parallel pr merge
I'll make the fix
EDIT upstream independently made a fix for the Tacticals.New change
actually something looks deeply messed up in the build system
https://gitlab.com/coq/coq/-/jobs/1783077180
COQC theories/PatriciaR.v
COQC theories/PatriciaR.v
File "./theories/PatriciaR.v", line 4338, characters 0-44:
Warning: Removed file ./theories/PatriciaR.vo
Error: Anomaly "Uncaught exception End_of_file."
Please report at http://coq.inria.fr/bugs/.
hmm, could that be related to the use of multiple _CoqProject
-like files?
also it seems itauto has no CI
perhaps it should be removed from coq's CI until that's changed
eg https://gitlab.com/coq/coq/-/jobs/3940699733
it seems to be due to the switch to dune (https://gitlab.inria.fr/fbesson/itauto/-/commit/ad31f305f281d89b7a9cf5f809062bd7ffd6e445)
What would be a correct fix for this?
cc @Emilio Jesús Gallego Arias
have you opened an issue in the repo? We can also ping Frédéric here.
I pinged him in private messages to avoid subscribing him to the stream
I have rerun my Coq CI, it runs... https://gitlab.inria.fr/fbesson/itauto/-/jobs/2957313
Am I doing something wrong?
it's specifically when used in coq CI, something about being built in a subdirectory of a project that also uses dune I guess
It is because dune build
will detect the workspace root as the Coq folder.
Unfortunately this is not very well structured in Dune, best solution is to never vendor, so indeed your testing workspace containts a checkout of every project and no submodules
In Coq we should actually set DUNE_ROOT=
to the right root before calling sub-scripts in CI
however I'm not sure Dune offers such a variable
The fix we have in other projects is to use --root .
, but that's a PITA for other reasons
So a fix would be dune build --root .
?
Yes, --root .
or the corresponding path where the main root is located
but indeed we should change our CI layout
You could actually improve the workflow a bit, as you are interested in having the binary in the source folder, you can do dune build --root . mlpatch
, and add a promotion rule so dune will copy it from the build directory, that way you don't have to guess these kind of _build/default/patch/foo.exe
Thanks. This should be fixed by https://gitlab.inria.fr/fbesson/itauto/-/commit/ce158859ce74c49b0c7a668582ca9b00e8403d6f
to those who notice that it still fails, cf https://github.com/coq/coq/pull/17399
I had no reason to not use dune 2.9
https://gitlab.inria.fr/fbesson/itauto/-/commit/a5a6f8e9887f40d526c087d72b56e094622aab2f should solve the issue.
@Frédéric Besson but the Dune 2.9 thing would have been fixed by the PR of @Gaëtan Gilbert I believe... Can't the Dune 3.6 features be kept?
my understanding is that flambda CI of Coq uses Dune 3.6
I did not pay attention to the dune number. I see no reason to require 3.6 if 2.9 is enough. And this does not prevent anyone from using dune 3.6 if they wish. Or am I missing something, again?
OK, so you were not using any specific features from Dune 3.6?
I was reading https://gitlab.inria.fr/fbesson/itauto/-/commit/a5a6f8e9887f40d526c087d72b56e094622aab2f and thinking something had changed w.r.t. testing of mathcomp-ssreflect
(in addition, if I remember correctly the opam build
property should not be used for dune, i.e., I think the convention is to use simply "dune" {>= "2.9"}
)
https://gitlab.inria.fr/fbesson/itauto/-/merge_requests/11 got merged early so it will be broken in CI until https://github.com/coq/coq/pull/17664 is merged (it still needs a coqhammer overlay, I'll do it later today)
Last updated: Oct 13 2024 at 01:02 UTC