Stream: Coq devs & plugin devs

Topic: make ci-jasmin (locally)


view this post on Zulip Hugo Herbelin (Sep 03 2023 at 11:17):

I had a failure of make ci-jasmin locally, apparently due to mathcomp-word installing in _install_ci and mathcomp installing in _build/install/default. I failed to understand how to fix it properly.

view this post on Zulip Karl Palmskog (Sep 03 2023 at 11:24):

isn't the problem something along the lines of that $CI_INSTALL_DIR needs to be set to the _install_ci directory? If not, then Dune uses the default install location

view this post on Zulip Karl Palmskog (Sep 03 2023 at 11:26):

(deleted)

view this post on Zulip Hugo Herbelin (Sep 03 2023 at 11:34):

IIUC, mathcomp-word uses dune (with the --prefix $CI_INSTALL_DIR option) while mathcomp uses coq_makefile's install.

view this post on Zulip Paolo Giarrusso (Sep 03 2023 at 12:17):

(Did you swap the install folders? Output in _build suggests you're using dune)

view this post on Zulip Hugo Herbelin (Sep 03 2023 at 13:15):

I'm working locally in a Coq archive, with dune. make ci-mathcomp installs in _build/install/default and make ci-mathcomp_word installs in _install_ci.

view this post on Zulip Paolo Giarrusso (Sep 03 2023 at 15:24):

hmm, is https://github.com/coq/coq/blob/master/dev/ci/ci-common.sh#L18-L39 relevant? CI_INSTALL_DIR doesn't seem used by any of the coq_makefile builds, but if GITLAB_CI is unset, that sets COQLIB="$PWD/_build/install/default/lib/coq" (and also a bunch more vars) — maybe those are used by coq_makefile?

view this post on Zulip Karl Palmskog (Sep 03 2023 at 15:28):

we have this in the makefile generated by coq_makefile:

COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)

Last updated: Jun 23 2024 at 01:02 UTC