Hugo Herbelin (Sep 03 2023 at 11:17): 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.
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
Karl Palmskog (Sep 03 2023 at 11:26):(deleted)
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.
Paolo Giarrusso (Sep 03 2023 at 12:17):(Did you swap the install folders? Output in _build suggests you're using dune)
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.
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?
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: Nov 29 2023 at 21:01 UTC