Stream: Coq devs & plugin devs

Topic: make ci-vst


view this post on Zulip Pierre Rousselin (Nov 18 2023 at 19:36):

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?

view this post on Zulip Gaëtan Gilbert (Nov 18 2023 at 19:40):

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

view this post on Zulip Pierre Roux (Nov 18 2023 at 20:40):

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?

view this post on Zulip Gaëtan Gilbert (Nov 18 2023 at 20:43):

we already set COQLIB in ci-common, no need to call coqc

view this post on Zulip Pierre Rousselin (Nov 18 2023 at 20:49):

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)

view this post on Zulip Pierre Rousselin (Nov 18 2023 at 20:54):

I'll try to solve this properly tomorrow.

view this post on Zulip Gaëtan Gilbert (Nov 18 2023 at 21:42):

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

view this post on Zulip Pierre Rousselin (Nov 19 2023 at 10:26):

I've worked on this. Would you say that this picture is correct?
build_dirs.png

view this post on Zulip Pierre Rousselin (Nov 19 2023 at 10:33):

If it is correct, then https://github.com/coq/coq/pull/18335 should fix local ci-vst.

view this post on Zulip Pierre Rousselin (Nov 19 2023 at 10:33):

(works locally, not 100% sure it works on gitlab)

view this post on Zulip Pierre Rousselin (Nov 19 2023 at 10:38):

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