Stream: MetaCoq

Topic: CI


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

view this post on Zulip Gaëtan Gilbert (Mar 05 2021 at 12:32):

what stops it from working with master?

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Mar 05 2021 at 13:13):

master is what we test in ci

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

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

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

view this post on Zulip Yannick Forster (Mar 05 2021 at 13:49):

The branch corresponding to the PR is strictly ahead of coq-8.11

view this post on Zulip Yannick Forster (Mar 05 2021 at 13:49):

But it doesn't compile, so it won't serve as an instant solution for you

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

view this post on Zulip Danil Annenkov (Mar 05 2021 at 13:55):

Cool, thanks @Yannick Forster , we'll wait a bit until the PR is merged.

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

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

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

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

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

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

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

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

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

view this post on Zulip Yannick Forster (Aug 05 2022 at 09:23):

@Kenji Maillard is our nix expert

view this post on Zulip Yannick Forster (Aug 05 2022 at 09:23):

I unfortunately don't know, but it's on my list to find out

view this post on Zulip Yannick Forster (Aug 05 2022 at 09:23):

We habe other projects as well which would profit from CI to avoid bit rot

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

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

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

view this post on Zulip Théo Zimmermann (Aug 05 2022 at 10:37):

Not the coqdevs: anyone with Nix packaging experience.

view this post on Zulip Théo Zimmermann (Aug 05 2022 at 10:38):

Maybe you meant the metacoq devs?


Last updated: Aug 11 2022 at 03:02 UTC