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.
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
IIUC, mathcomp-word uses dune (with the --prefix $CI_INSTALL_DIR option) while mathcomp uses coq_makefile's install.
(Did you swap the install folders? Output in _build suggests you're using dune)
I'm working locally in a Coq archive, with dune.
make ci-mathcomp installs in
make ci-mathcomp_word installs in
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
we have this in the makefile generated by
COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
Last updated: Nov 29 2023 at 21:01 UTC