Jason Gross (May 21 2021 at 22:26): 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?)
Gaëtan Gilbert (May 21 2021 at 22:41):it's coqlib based IIRC
Théo Zimmermann (May 22 2021 at 12:27):Indeed, relocating should normally be possible and therefore a chroot seems overkill.
Last updated: May 31 2023 at 16:01 UTC