Bas Spitters (Mar 05 2021 at 12:25): Bas Spitters (Mar 05 2021 at 12:25):We'd like to put our work on ConCert in Coq CI, but for that it should work with master. According to:
https://github.com/coq/coq/blob/master/dev/ci/README-users.md
https://github.com/AU-COBRA/ConCert
@Théo Zimmermann What's the best way forward?
Gaëtan Gilbert (Mar 05 2021 at 12:32):what stops it from working with master?
Danil Annenkov (Mar 05 2021 at 12:40):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)
Théo Zimmermann (Mar 05 2021 at 12:55):@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.
Théo Zimmermann (Mar 05 2021 at 12:56):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.
Danil Annenkov (Mar 05 2021 at 13:12):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?
Gaëtan Gilbert (Mar 05 2021 at 13:13):master is what we test in ci
Yannick Forster (Mar 05 2021 at 13:13):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
Danil Annenkov (Mar 05 2021 at 13:31):@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.
Yannick Forster (Mar 05 2021 at 13:48):I was wrong, sorry. Here is my PR against master with all the fixes for coq-8.13: https://github.com/MetaCoq/metacoq/pull/537
Yannick Forster (Mar 05 2021 at 13:49):The branch corresponding to the PR is strictly ahead of coq-8.11
Yannick Forster (Mar 05 2021 at 13:49):But it doesn't compile, so it won't serve as an instant solution for you
Yannick Forster (Mar 05 2021 at 13:50):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)
Danil Annenkov (Mar 05 2021 at 13:55):Cool, thanks @Yannick Forster , we'll wait a bit until the PR is merged.
Matthieu Sozeau (Mar 08 2021 at 13:17):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
Yannick Forster (Jun 09 2021 at 16:20):@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
Bas Spitters (Jul 06 2022 at 07:52):With metacoq being released what's the status of the Nix CI, which I understand should facilitate tracking reverse dependencies.
Yannick Forster (Jul 06 2022 at 08:05):Thanks to @Kenji Maillard proper nix support is on its way: https://github.com/MetaCoq/metacoq/pull/706
Bas Spitters (Jul 06 2022 at 08:32):Thanks!
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?
Yannick Forster (Jul 06 2022 at 08:34):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)
Bas Spitters (Jul 06 2022 at 10:33):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!
Yannick Forster (Jul 06 2022 at 10:50):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!
Bas Spitters (Aug 05 2022 at 09:22):@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.
https://github.com/coq-community/coq-nix-toolbox
Yannick Forster (Aug 05 2022 at 09:23):@Kenji Maillard is our nix expert
Yannick Forster (Aug 05 2022 at 09:23):I unfortunately don't know, but it's on my list to find out
Yannick Forster (Aug 05 2022 at 09:23):We habe other projects as well which would profit from CI to avoid bit rot
Bas Spitters (Aug 05 2022 at 09:25):Yes, metacoq is becoming a central project, so tracking reverse dependencies should be useful for a number of projects.
Théo Zimmermann (Aug 05 2022 at 09:57):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.
Bas Spitters (Aug 05 2022 at 10:35):@Théo Zimmermann Great so that's something the coqdevs can/should do once @Danil Annenkov has completed the port to 8.14 ?
Théo Zimmermann (Aug 05 2022 at 10:37):Not the coqdevs: anyone with Nix packaging experience.
Théo Zimmermann (Aug 05 2022 at 10:38):Maybe you meant the metacoq devs?
Last updated: Oct 13 2024 at 01:02 UTC