We'd like to put our work on ConCert in Coq CI, but for that it should work with master. According to:
@Théo Zimmermann What's the best way forward?
what stops it from working with master?
Hi @Gaëtan Gilbert , we depend on MetaCoq and we use the version compatible with Coq 8.11 currently (which is the main stable branch, if I understand correctly)
@Danil Annenkov My understanding is that the MetaCoq maintainers simultaneously maintain several branches with the same features: in January, they released 1.0-beta2 for Coq 8.13, 8.12 and 8.11.
Given that MetaCoq also has a branch tracking Coq master, I think it should be doable for you to also test your project with this version.
Thanks @Théo Zimmermann , it's a good point. I can see that the branches for Coq 8.12 and Coq 8.13 have the same features, but for master "This branch is 129 commits ahead, 103 commits behind coq-8.11. ".
@Matthieu Sozeau , do you know which branch is compatible with Coq's master?
master is what we test in ci
There is a MetaCoq
master branch compatible with Coq
master. When I created the
coq-8.13 branch I firsted synced
master with the rest, so it should not be terribly out of date regarding features
@Yannick Forster thanks for your answers! Currently, for MetaCoq's master I see "103 commits behind coq-8.11.", I should check with @Jakob Botsch Nielsen what features we rely on, which are not yet in master.
I was wrong, sorry. Here is my PR against
master with all the fixes for
The branch corresponding to the PR is strictly ahead of
But it doesn't compile, so it won't serve as an instant solution for you
I would guess that it's not too much work to make it compile with
master (and we need to do that anyways for MetaCoq, inependently of ConCert)
Cool, thanks @Yannick Forster , we'll wait a bit until the PR is merged.
Yeah, it was left lying, apparently we're hitting an issue in compilation of extracted code with the primitive integers. I'll try to see what's up with that
@Danil Annenkov @Bas Spitters MetaCoq's master is now in sync with the other branches again, meaning it is roughly on the feature level from the beta2 release of MetaCoq. Thus porting work on MetaCoq to Coq master / the upcoming 8.14 release should be feasible again
With metacoq being released what's the status of the Nix CI, which I understand should facilitate tracking reverse dependencies.
Thanks to @Kenji Maillard proper nix support is on its way: https://github.com/MetaCoq/metacoq/pull/706
Since the CI passed the PR can be merged ?
So, after @Danil Annenkov finishes the port of concert to 8.14 we can use the metacoq Nix CI to check that concert does not break on changes in metacoq?
Yes, that's my understanding. (still worth mentioning, although kind of circumvented due to nix: Coq 8.16 makes MetaCoq compilation a lot faster, something like factor 2. So it's maybe worth directly porting everything on to 8.16)
I think @Danil Annenkov hoped going from 8.14 to 8.16 would not be too hard. Does that sound reasonable?
A factor 2 speed up would be great!
MetaCoq exposes more or less literally the same files on 8.14-8.16, and if I recall correctly there are no major hurdles in general when porting code between these versions - so yes, that sounds very reasonable!
@Yannick Forster With Nix merged into metacoq do you understand how to track reverse dependencies (ConCert) in the CI.
There's some documentation here, but we don't understand the full picture yet.
@Kenji Maillard is our nix expert
I unfortunately don't know, but it's on my list to find out
We habe other projects as well which would profit from CI to avoid bit rot
Yes, metacoq is becoming a central project, so tracking reverse dependencies should be useful for a number of projects.
Basically, the answer is we need to add a Nix package for ConCert (and other reverse dependencies) either directly in nixpkgs or (temporarily in
.nix/coq-overlays/). Then, regenerating the CI files should be all that takes to add (packaged) reverse dependencies to the CI.
@Théo Zimmermann Great so that's something the coqdevs can/should do once @Danil Annenkov has completed the port to 8.14 ?
Not the coqdevs: anyone with Nix packaging experience.
Maybe you meant the metacoq devs?
Last updated: Mar 02 2024 at 17:02 UTC