Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

[MSoegtropIMC]

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-serapi.8.16+rc1+0.16.0
from official repository https://coq.inria.fr/opam/extra-dev/packages/coq-serapi/coq-serapi.8.16+rc1+0.16.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

[ejgallego]

Hi @MSoegtropIMC , I'd like to see a newer version on the platform, however Coq 8.16 needs to be released first, right?

[palmskog]

@ejgallego the point here is that when 8.16.0 is released, you can do the SerAPI new release, then tell @MSoegtropIMC about it in this issue and close the issue.

[ejgallego]

What I mean is that I can only work on this issue as indiciated if Coq 8.16 reaches opam before the stated deadline (Aug 31st)

[palmskog]

I think it's implicit that Platform 2022.09 will be delayed commensurately if 8.16.0 is delayed. So for example, if 8.16.0 only comes out at the end of August, 2022.09 will be pushed to October.

[MSoegtropIMC]

@ejgallego : in Coq Platform main there is a preview version with 8.16+rc1 - which is good enough for most things.

The delay between 8.16.0 and Coq Platform 2022.09 will be a bit shorter when 8.16.0 is delayed - there is some work which depends on 8.16.0 and some not. But one likely wants a Platform beta with 8.16.0 of two weeks since 8.16+rc1 has some issues (e.g. coq-interval does not work).

[MSoegtropIMC]

You can tell me which version you want (for the preview - not for the beta - also a commit is fine) - Coq Platform has its opam patch repo which allows me to do some tricks.

[MSoegtropIMC]

@ejgallego : since 8.16.0 is out, I wanted to ask what your plans are.

[ejgallego]

Hi @MSoegtropIMC , I will upload a release to the main OPAM repos ASAP.

[ejgallego]

Closed by ocaml/opam-repository#22087

[Zimmi48]

I believe we are in this case:

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.

[MSoegtropIMC]

@ejgallego : can you please reopen this issue until I updated Coq Platform - otherwise I might forget to do so.

The opam PR failed CI and probably won't get merged unless you take care of it.

[ejgallego]

Sure; I will keep this open.

It seems a bit strange to me tho to track a todo in coq-platform as an issue on the upstream. I have quite a few thoughts on the process (pity we didn't manage to talk more at Nice), hopefully once I resolve quite urgent research we can discuss more.

[MSoegtropIMC]

Yeah, it is a bit strange. But otherwise I would have to create two issues for everything and the discussion will be partly here and partly there. It does have advantages to have one issue per package.

[ejgallego]

Mmm, yes, definitively there should be no two issues. Actually maybe the platform could be a bit more dynamic? I am worried about manual curation scaling properly to a large set of packages, but indeed we gotta discuss more about how to get the CI and platform model closer.

[ejgallego]

The Opam release was merged so this should be good for the platform I hope.

[palmskog]

We should ping @erikmd who (in a couple of hours when opam repo is deployed) finally has everything he needs to update the Docker with 8.16.0.

[erikmd]

Hi all, hi @palmskog, thanks a lot for the timely pings!

coq-serapi seems to be deployed now ( https://opam.ocaml.org/packages/coq-serapi/ )
so I've just pushed a commit ( coq-community/docker-coq@409bcd6 )
triggering this GitLab CI pipeline: https://gitlab.com/coq-community/docker-coq/-/pipelines/636283969

I'll look after the mathcomp/mathcomp update tomorrow. (done)

[erikmd]

BTW as soon as coqorg/coq:8.16.0 goes live, this badge will be updated:

[MSoegtropIMC]

The opam package works for me (in the sense that it compiles), so I will close this issue.

[ejgallego]

Thanks @MSoegtropIMC

[MSoegtropIMC]

Reopening this, so that I don't forget to update as discussed here Zulip

[MSoegtropIMC]

I update coq-serapi to version coq-serapi.8.16.0+0.16.1 in the 2022.09 prep branch as discussed.