[RFC] release cycle

[gares]

Here a draft of what I presented at the Coq call, comments welcome.

Rendered here

CC @Zimmi48 @erikmd @MSoegtropIMC

[ejgallego]

Thanks @gares for the writeup, I think this evolution is on the right path and in line with many of the thoughts that have been discussed over the years.

Indeed the beta should be pretty conservative IMO as you propose, I think this was not so possible before due to actually many regressions happening, but our large (even if expensive) CI has helped a lot to actually produce something that almost works out of the box in most cases.

I'll add some other thoughts inline.

[silene]

There are a few points that are not clear to me:

• At which point does pinning happen on the branch? Given the description of stage 4, it seems to have completed at the end of stage 1, but since stage 1 is only 10 days long, that seems unlikely.
• The timeline confuses me a bit. It seems like version X.0 of the platform could be released after version X.1 of Coq. It would seem better to directly skip to platform X.1 in that case, so as to not confuse users.

[MSoegtropIMC]

@silene :

A release of a package is mostly there to add features to this package, not to ensure compatibility to core Coq. This made the picking in the past very difficult, because one needed something which does build with latest Coq but does not contain unfinished features of the package. I would say finding a reasonable compromise here was at least 90% of the picking effort in the past - frequently involving putting together cherry picked patches. Since the "rounded up feature set" aspect can now be moved to the Coq platform, I would expect that from now on the picking effort for Coq's CI is much less. For Coq's own CI it doesn't matter if the version tested in CI is something with a reasonably closed feature set one would like to release to the users. All what matters is that whatever is there builds with current Coq. So I think it would be OK to simply pick something which compiles.

Regarding versioning: my plan is that a Coq platform version has always one digit/component more than the Coq release. E.g. there is something like 8.13.0+beta and 8.13.0.0 and likely also a 8.13.0.1. And there might even be something like 8.13+beta.0 or 8.13+beta+beta. Increasing releases of the Coq platform with constant Coq version are e.g. useful to add new packages.

[silene]

So I think it would be OK to simply pick something which compiles.

If I understand you correctly, pinning CI on the Coq branch should not be made using tags (contrarily to what was done on the current release branch) but using random commits. If so, this should certainly be made clearer in the CEP.

[gares]

If so, this should certainly be made clearer in the CEP.

I will, and mention the (new I guess) script that does this automatically.
FTR there is also another script that opens almost automatically issues on the upstream repo saying "we are testing commit $sha would you mind tagging it"? (you saw a couple of those on your projects)

[gares]

The timeline confuses me a bit. It seems like version X.0 of the platform could be released after version X.1 of Coq. It would seem better to directly skip to platform X.1 in that case, so as to not confuse users.

Regarding versioning: my plan is that a Coq platform version has always one digit/component more than the Coq release. E.g. there is something like 8.13.0+beta and 8.13.0.0 and likely also a 8.13.0.1. And there might even be something like 8.13+beta.0 or 8.13+beta+beta. Increasing releases of the Coq platform with constant Coq version are e.g. useful to add new packages.

I don't have a clear idea here, nor strong opinions, but I'm not in love with the idea that the platform version mentions the minor version of Coq, especially if we produce many hotfixes. Maybe it's a dream, but it would be nicer if Coq users could say "Coq 8.13 platform 7" to mean the platform version 7 for Coq 8.13 which includes some Coq 8.13.x which the platform devs see fit. After all the plan in this CEP is to hide "bare bone Coq" from users and expose only the platform.

[ejgallego]

I don't have a clear idea here, nor strong opinions, but I'm not in love with the idea that the platform version mentions the minor version of Coq, especially if we produce many hotfixes. Maybe it's a dream, but it would be nicer if Coq users could say "Coq 8.13 platform 7" to mean the platform version 7 for Coq 8.13 which includes some Coq 8.13.x which the platform devs see fit. After all the plan in this CEP is to hide "bare bone Coq" from users and expose only the platform.

A common naming scheme with platforms is to use a YYYY-MM data format, so you have Coq Platform 2020-12 , etc...

[Zimmi48]

LGTM though I haven't yet read comments from other people.

[MSoegtropIMC]

If I understand you correctly, pinning CI on the Coq branch should not be made using tags (contrarily to what was done on the current release branch) but using random commits. If so, this should certainly be made clearer in the CEP.

Yes, this is the idea as soon as the Windows installer in Coq CI is stripped down to building just Coq and CoqIDE (and maybe Ltac2 and Equations). Up to now using tags was required cause of the Windows installer. But the past experience showed that this approach is hard to maintain and definitely not scalable.

I would say in 8.13 the goal is to make a sort of hybrid approach to have a smooth transition, that is ensure that a Coq Platform with full Windows installer can be build shortly after the release. After that Coq's CI can concentrate on its original purpose.

[MSoegtropIMC]

It might make sense to bind the packages to a release branch of the package during the beta phase, rather than to a commit. At the end of the beta phase, this branch is tagged then. Both approaches have their advantages and disadvantages. Using branches is likely more agile and less work for the platform maintainers since changes in the release branches of the packages are immediately visible. The downside is that platform CI does not run automatically on changes, so during the beta phase one would need at least one build a day to find breaking changes. Also with commits the platform maintainers would have more control. I think it depends on the discipline of the package maintainers what works better. My guess is that we will use branches where it works well and fall back to commits for specific projects where things go wild.

[Zimmi48]

It might make sense to bind the packages to a release branch of the package during the beta phase, rather than to a commit.

Yes, but for most non-plugin projects there are no release branches (releases are created from master). So my conclusion is the same as yours.

[Zimmi48]

One thing that is really important IMHO is that this CEP says explicitly what policy it sets and what it leaves up to maintainers / to be decided later. E.g., I wouldn't like the CEP to propose a versioning scheme for the platform to see that it is immediately deviated from, unless the CEP explicitly says that the proposed scheme is just a non-binding example. So, either we explicitly agree on a scheme, details of the release steps, etc., or we explicitly leave some of these items unbound.

My opinion is that it would make sense to have a discussion on the versioning scheme of both Coq and the platform as part of this CEP, but I wouldn't want this to become the whole discussion and to mask other aspects that would deserve to be discussed.

[Zimmi48]

as soon as the Windows installer in Coq CI is stripped down to building just Coq and CoqIDE (and maybe Ltac2 and Equations)

I've already expressed this before and this also seems to be the opinion of Enrico from what I read in this CEP, but I think there should be no left-over code for the Windows installer in Coq's repository and in particular that we should stop producing any kind of installers as assets with Coq's own releases. Of course, keeping a CI job that tests the (external) Coq platform installer scripts makes complete sense.

[MSoegtropIMC]

but I think there should be no left-over code for the Windows installer in Coq's repository and in particular that we should stop producing any kind of installers as assets with Coq's own releases.

I agree. I mentioned the installer just to explain why we did need proper tags before in Coq CI for releases and why this changed now. If one wants to have a small platform build (just Coq and CoqIDE) in Coq CI or not remains to be seen, depending on how frequently it happens that something breaks here. My guess is that it won't be needed. Running a daily master build on Coq platform and manually creating an issue if this breaks should be sufficient.

[erikmd]

Thanks @gares for opening the CEP and pinging me (and sorry for the delay, I've been swamped by teaching, and on-going grading…)
the proposed workflow looks nice; and I strongly agree with this comment of yours where you suggest that within the version X.0 of the platform, the X will just be of the form 8.14 (without making explicit the chosen patchlevel version of coq; even if obviously, the exact version of Coq will be specified and documented using an opam constraint or so).

Indeed, this would be similar to the choice that had been done when I had discussed the versioning strategy of coqorg/coq with @Zimmi48 and @ejgallego: we can expect most users of, say, Coq 8.14, to be especially interested in installing Coq 8.14.x with x = the latest released patchlevel, or more generally (in the socpe of this CEP), an appropriate version chosen by the PRM.

Some extra questions:

1. what should happen when Coq V8.14.1 is released and Coq-Platform 8.14.0 already exist? → should we just substitute in the Coq-Platform 8.14.0 spec and docker image, the version of Coq V8.14.0 with Coq V8.14.1? or should we necessarily release a new Coq-Platform 8.14.1, etc., for each change of any version in the spec? (FTR: in coqorg/coq, with the current workflow, coqorg/coq:8.x is an alias for coqorg/coq:8.x.0, and when Coq V8.x.1 is released, coqorg/coq:8.x.0 is removed and replaced with coqorg/coq:8.x.1 but the short alias coqorg/coq:8.x is still available and is remapped to the latest patchlevel).
   Actually I guess that for this first question, the answer could be a trade-off: if you think all versions of the libraries should be "immutable" in a given platform version, we might want to have an "exception" for this rule just for the coq compiler patchlevel version itself.

2. as the CEP text proposes to rely on Docker images for packaging the platform, do you think we could directly rely on Docker-Coq images to this aim? (currently, the release of these images follow the opam releases of coq… with the above strategy for packaging the latest patchlevel). In this case, the build of the Coq-Platform images could be similar to building the mathcomp/mathcomp images. But on second thought, this can be viewed as an "implementation detail" so I guess it doesn't need to be documented in the CEP text, maybe.

3. Currently, there is a difficulty (vicious circle) that just occurs in one place (the CI of Bignums): for backward compatibility reasons, Docker-Coq integrates coq+bignums. But this cause some pain if there is a breaking change in Coq master that breaks Bignums. Because the coq and bignums repository are separate but bundled in the image… which is also used in the Docker-based CI of Bignums, for simplicity. So…
   Maybe a specific strategy could be devised to have two overlays (in Bigums and in Docker-Coq) or, to have a simpler solution, later on, Bignums could just be reintegrated in Coq? (see also [released] Add coq-bignums.8.13.0 opam#1512 (comment); maybe that discussion could be resumed at some point)

[gares]

But on second thought, this can be viewed as an "implementation detail" so I guess it doesn't need to be documented in the CEP text, maybe.

I think you are right, but before saying that "we officially generate dockers" I wanted a docker expert (eg you) to agree on the plan and eventually help implementing something like the snap job for the platform (so that a PRM does not need to know the details of docker, just how to invoke a job which builds and deploys the image).

[gares]

for backward compatibility reasons, Docker-Coq integrates coq+bignums

I see what you mean. Let me clarify. We have 2 docker images in this CEP:

• one with just coq vX, so that platform packages can test/release (core)
• one with the entire platform, so that all non-platform users can test their stuff against the platform (platform)

To me the core image roughly corresponds to the actual images but exists just for technical reasons. In the sense that I would not advertise it to the public in the large, and we may even put in there all we have in Coq's CI (all the plugins, pinned to a commit hash). So yes, also bignums would be there, but not a released version.

The platform image should be the one used for CI in the wild (if you want to CI a project already in there you can start by opam remove it). But for a few projects, I believe testing against a stable platform release (as a single entity) should be the preferred solution.

Maybe there is still some need for the current images for both stable and dev Coq, and/or derived images (like the ones with mathcomp.dev).

I start to think docker+CI+platform should be a separate CEP/discussion. Maybe I can just mention the possibility of making a docker images in this CEP, without making it mandatory.

[gares]

I believe I've integrated all remarks and improved the text a little here and there.
I did pick the 8.13.0.0 versioning schema for the sake of the examples, and declared out of the scope of this CEP the discussion about (even if I don't like it, but it is there already, so...).
I did make docker recommended but not mandatory.

I think this text should be validated one last time by @silene as the nex RM and by @MSoegtropIMC as the main platform dev.
Once this is done we can try to adjust the release checklist on the Coq side (and maybe craft one on the platform side).

[silene]

I am fine with it. Here are a few editorial suggestions. First, since you are counting days using multiple of 5 working days, just write "weeks" instead (e.g., 2 weeks instead of 10 days, 1 month instead of 20 days). Second, I would move all the negated sentences from stage 1 to stage 2; it seems more important to say that stage 2 delivers a binary release rather than stage 1 does not deliver a binary release.

[gares]

Thanks I did push some corrections.
I did leave a side note that no binary installers are expected, because it stresses the difference with the current process, and a pointer to the platform release for them. There there was already a positive sentence I guess.

[Zimmi48]

It seems that we have converged on the YYYY.MM.X scheme for the platform versions (see https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/Version.20naming). I guess that since we have arrived to this conclusion, it would make sense to update the CEP accordingly. Then, it seems to me that it is time to merge.

Note that I've updated the release checklist accordingly in coq/coq#13823.

[gares]

I'll try to update the CEP tomorrow, thanks everybody for contributing to the discussion

[gares]

I hope my changes are OK w.r.t. the version of the platform.

[Zimmi48]

These are only typos.

[Zimmi48]

I propose to merge this CEP and the related coq/coq#13823 PR at the next Coq Call.

[gares]

Thanks! and agreed.

[gares]

we can merge now

[Zimmi48]

Approved in the Coq Call 😉

[Zimmi48]

I've renamed the two impacted milestones in the Coq repository.

[erikmd]

@gares, I've just noticed that given the underlying feature branch of this PR does not exist anymore, the URL
https://github.com/gares/ceps/blob/platform-release-cycle/text/052-platform-release-cycle.md in #52 (comment) is broken… so you may want to edit the initial post to put https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md