Yannick Forster (Sep 30 2020 at 13:11): 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!
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.
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?
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"
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.
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.
Karl Palmskog (Sep 30 2020 at 13:48):ah, but quite a few of coq-community projects do have Dune support now at least
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.
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?
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)
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
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
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"
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]
Matthieu Sozeau (Sep 30 2020 at 16:24):Yep, the patching should be unnecessary now
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
Ah right. That’s another problem I don’t know how to solve. Linked to the value restriction IIRC
Emilio Jesús Gallego Arias (Oct 01 2020 at 17:25):There is already an open bug indeed :S
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: May 31 2023 at 10:01 UTC