Stream: Coq devs & plugin devs

Topic: Relocating Coq install?


view this post on Zulip Jason Gross (May 21 2021 at 22:26):

I'm trying to reuse artifacts from Coq's CI to run the bug minimizer. Because I need to run two different versions of Coq, I can't reuse the install location; instead of the prefix /builds/coq/coq/_install_ci/, I use the prefixes /github/workspace/builds/coq/coq-passing/_install_ci/ and /github/workspace/builds/coq/coq-failing/_install_ci/. Since some of the CI targets use make && make install, running make ci-elpi fails because it installs files to /builds/coq/coq/_install_ci/ and then subsequently can't find them in /github/workspace/builds/coq/coq-passing/_install_ci/. How can I relocate the Coq CI artifacts in a way that targets like make ci-elpi will succeed? (Is there some extra environment variable I can set? Do I have to use a chroot or something?)

view this post on Zulip Gaëtan Gilbert (May 21 2021 at 22:41):

it's coqlib based IIRC

view this post on Zulip Théo Zimmermann (May 22 2021 at 12:27):

Indeed, relocating should normally be possible and therefore a chroot seems overkill.


Last updated: Oct 15 2021 at 19:03 UTC