Stream: MetaCoq

Topic: MetaCoq CI / Coq Community CI


view this post on Zulip Yannick Forster (Sep 30 2020 at 13:11):

We have discussed in the MetaCoq team that we need a CI to be able to see whether changes to upstream MetaCoq break projects depending on it (like plugins written in MetaCoq, or the CertiCoq compiler). Before setting up our own CI, we wanted to ask whether there is any hope for a more centralised coq-community CI where projects can just join. I'll ping @Théo Zimmermann and @Erik Martin-Dorel in this message, but everyone feel free to contribute thoughts!

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 13:41):

Yes, I'm definitely interested in opening a discussion on this topic. It looks like a more and more common requirement for Coq projects. I'd like to hear more about the use case though.

view this post on Zulip Karl Palmskog (Sep 30 2020 at 13:42):

how would a "coq-community CI" work? You mean it's like some secondary set of projects that follows the general Coq CI setup?

view this post on Zulip Karl Palmskog (Sep 30 2020 at 13:44):

our basic CI scripts in coq-community are unfortunately not usable for anything in this direction, we don't even have good support for "two projects in the same repo where one depends on the other being installed"

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 13:47):

I didn't start to throw ideas around because I wanted to hear more of the use case first but one possibility would be to have some sort of monorepo for CI where PR are reproduced and the universe of reverse dependencies is rebuilt at every change. This would be more conveniently done if every project was using Dune as their build system though.

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 13:48):

FTR there already exists some basic ci_test_dependants feature in the CI templates. I think it is used for coq-ext-lib.

view this post on Zulip Karl Palmskog (Sep 30 2020 at 13:48):

ah, but quite a few of coq-community projects do have Dune support now at least

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 13:48):

And math-comp already has its own reverse dependecy testing + overlay mechanism as well, which shows the raising interest for such a system.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2020 at 14:14):

Indeed that's an interesting subject, we should maybe do a work group about it?

view this post on Zulip Karl Palmskog (Sep 30 2020 at 14:45):

I think it would be better to base the tentative CI off of explicit repo URLs and Dune rather than opam dependencies and the extra-dev repo, since the latter is typically not in the best shape (people don't submit updated packages to extra-dev often)

view this post on Zulip Yannick Forster (Sep 30 2020 at 15:22):

MetaCoq doesn't work with Dune yet I think, but that's not necessarily a hindrance for a Coq Community CI project

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:24):

well, my secret plan is that we provide an incentive to support building with Dune by making it a CI requirement

view this post on Zulip Yannick Forster (Sep 30 2020 at 15:24):

My concrete use case that triggered me to write the message was that a commit in MetaCoq (which just did refactoring) broke CertiCoq. Now it wasn't hard to fix at all, but I first had to understand where the error is coming from, and a CI which would have told us even earlier saying "this PR breaks CertiCoq"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 30 2020 at 16:01):

Yannick Forster said:

MetaCoq doesn't work with Dune yet I think, but that's not necessarily a hindrance for a Coq Community CI project

Note that I have a branch that added Dune support, so far it was stuck on an extraction bug but surely we could workaround it [a file that extraction produces requires patching]

view this post on Zulip Matthieu Sozeau (Sep 30 2020 at 16:24):

Yep, the patching should be unnecessary now

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2020 at 14:00):

@Matthieu Sozeau it seems the patch is still needed:

File "metacoq/template-coq/extraction/CRelationClasses.ml", line 1:
Error: The implementation metacoq/template-coq/extraction/CRelationClasses.ml
       does not match the interface metacoq/template-coq/extraction/.metacoq_template_plugin.objs/byte/cRelationClasses.cmi:
       Values do not match:
         val eq_equivalence : ('_weak1, '_weak2) coq_Equivalence
       is not included in
         val eq_equivalence : ('a1, Obj.t) coq_Equivalence
       File "metacoq/template-coq/extraction/CRelationClasses.mli", line 107, characters 0-46:
         Expected declaration
       File "metacoq/template-coq/extraction/CRelationClasses.ml", line 204, characters 4-18:
         Actual declaration

view this post on Zulip Matthieu Sozeau (Oct 01 2020 at 16:19):

Ah right. That’s another problem I don’t know how to solve. Linked to the value restriction IIRC

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2020 at 17:25):

There is already an open bug indeed :S

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2020 at 17:25):

@Kazuhiko Sakaguchi had an idea to hack around this, given that indeed a few developments seem to be hit by this maybe it would be nice to do the workaround.


Last updated: Aug 11 2022 at 02:03 UTC