Guillaume Melquiond (Jun 22 2021 at 09:30): Guillaume Melquiond (Jun 22 2021 at 09:30):What is the fastest way to check a given CI contribution? (I am trying to find a suitable commit for MetaCoq for the 8.14 CI.) Just doing make ci-metacoq fails because it does not find any Coq executable files. Are there other Make targets that I need to build first or some environment variables that I need to set?
Pierre-Marie Pédrot (Jun 22 2021 at 09:31):make world is a good start
Emilio Jesús Gallego Arias (Jun 22 2021 at 09:31):With the current setup doing make {,-f Makefile.dune} world is the usual previous step
Matthieu Sozeau (Jun 22 2021 at 09:33):@Guillaume Melquiond if you've got a commit I can tag just tell me
Guillaume Melquiond (Jun 22 2021 at 09:34):As far as the CI is concerned, I do not need tags, since hashes are used. (So, tag only if you yourself need one.)
Guillaume Melquiond (Jun 22 2021 at 13:12):make -f Makefile.dune world was sufficient for make ci-metacoq.
Now I am trying to find a suitable pin for Coqtail. But make ci-coqtail fails with Failed: Failed to create Coqtop instance. Any idea?
Emilio Jesús Gallego Arias (Jun 22 2021 at 13:14):There is a bug open about that, I am not sure what env variable was coqtail using to detect coqtop
Emilio Jesús Gallego Arias (Jun 22 2021 at 13:16):The CI runs from an installed Coq so that avoids this problem it seems
Last updated: Dec 01 2023 at 06:01 UTC