Stream: Coq devs & plugin devs

Topic: Local CI


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2021 at 09:31):

make world is a good start

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Jun 22 2021 at 09:33):

@Guillaume Melquiond if you've got a commit I can tag just tell me

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Oct 16 2021 at 07:02 UTC