On my machine, make ci-vst
from coq's repository fails with:
Makefile:150: *** FIRST BUILD COMPCERT, by: cd /home/pierre/depots/coq/_build/default/../install/default/lib/coq/user-contrib/compcert; make clightgen.
I think there is something broken for local execution of the ci. I have found a workaround, but first, could anyone please confirm that make ci-vst
fails locally?
probably the problem is ci-compert script does -coqdevdir ${CI_INSTALL_DIR}/lib/coq/user-contrib/compcert
which is incorrect when local
I don't know if passing -coqdevdir is aven necessary
cc @Pierre Roux for https://github.com/coq/coq/commit/f9bc0eb5297687250de912e48806c0cbda5eeff0
IIRC, it's necessary for compcert to install its .vo in a place Coq can find them when required by VST (without an explicit dir, the .vo are put in some nonsensical place) Maybe the script should retrieve COQLIB from coqc -config
?
we already set COQLIB in ci-common, no need to call coqc
The main problem seems to be that ci-compert.sh
uses CI_INSTALL_DIR
which is not the same as $(coqc -where)
when the CI is called locally (whereas in gitlab CI, it is the same)
I'll try to solve this properly tomorrow.
CI_INSTALL_DIR is correct for putting random executables and such (without using it they would go to the user's opam switch which is not what we want)
it is just not correct for .vo files and other stuff used by coq itself
I've worked on this. Would you say that this picture is correct?
build_dirs.png
If it is correct, then https://github.com/coq/coq/pull/18335 should fix local ci-vst.
(works locally, not 100% sure it works on gitlab)
Apparently, @Pierre Roux bet me into proposing a PR. Can this pipeline https://gitlab.inria.fr/coq/coq/-/pipelines/886144 be cancelled?
Last updated: Oct 13 2024 at 01:02 UTC