Stream: Coq devs & plugin devs

Topic: no betas for 8.14 and later?


view this post on Zulip Karl Palmskog (Dec 15 2020 at 12:31):

A recent discussion on GitHub unveils that there will be no more betas for future Coq versions. Can someone give (or point to) the rationale/background here? This means we all will have to test compatibility against moving targets up until the release (e.g., v8.14 in the GitHub repo)

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 12:37):

When was that announced? I don't remember this being discussed.

view this post on Zulip Karl Palmskog (Dec 15 2020 at 12:39):

to me at least, "release candidate" is a form of beta, but apparently not to others

view this post on Zulip Karl Palmskog (Dec 15 2020 at 12:41):

it seems like a pointless renaming exercise to go from +beta1 to (something like) +rc1 just to not call it beta and have it live in the regular opam repository like a release, if that is the intention

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 12:47):

to stress that it won't change in breaking ways from there to the final

some people might take an rc more seriously than a beta

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 12:48):

e.g. if a package doesn't track master, porting to an rc might make more sense than porting to a beta? not sure

view this post on Zulip Enrico Tassi (Dec 15 2020 at 12:59):

Let me clarify that. I was referring to the discussion at the last Coq Call where I proposed a different release process. One of the things was that we usually don't break compatibility after a certain point in time, even if we don't say that. Renaming the beta into a release candidate seems a way to make it more clear. For example, since the v8.13+beta1 tag I think I merged in the v8.13 0 (zero) PRs touching .ml code! All PRs are about documentation, installer scripts, ...

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2020 at 13:02):

How are we supposed to perform bugfixes then?

view this post on Zulip Karl Palmskog (Dec 15 2020 at 13:02):

I mean, not touching the ML code doesn't in itself guarantee that (downstream) projects don't break, e.g., linking or scripts can cause that as well

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:03):

Pierre-Marie Pédrot said:

How are we supposed to perform bugfixes then?

8.13 seems an extreme case, but we do have CI for that.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:07):

Karl Palmskog said:

I mean, not touching the ML code doesn't in itself guarantee that (downstream) projects don't break, e.g., linking or scripts can cause that as well

Once more, we do test on our side. But more importantly the process I described passes the ball to the platform, which will start to build packages on top of the RC tag, and signal to the upstreams how things are (this time I did it myself as part of the standard release).
If some "scripts" (I guess you mean the makefiles) are broken in Coq proper, then we can address that for the final.

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:09):

So, on one hand things are exactly like before (naming it beta or RC does not change things).
But we try harder to consider that tag, whatever we name it, a solid base for the platform (no breaking changes allowed).

view this post on Zulip Enrico Tassi (Dec 15 2020 at 13:10):

This is only a little detail of what I proposed, when I'll have some time I'll write it down so that discussions can happen on the full picture.

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:26):

IIUC, the core point is that porting to an -rc is not pointless because most breaking changes are in

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:26):

"all breaking changes" is the goal, but not an actual guarantee

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:28):

the promise is that porting to -rc and then porting to the release should _not_ be double the work but more like ~101% of the work :-)

view this post on Zulip Karl Palmskog (Dec 15 2020 at 15:26):

@Enrico Tassi so these release candidates would not be pre-releases on GitHub, but actual releases? And they would be packaged by everyone downstream (including the regular opam repository) as releases?

view this post on Zulip Karl Palmskog (Dec 15 2020 at 15:30):

given that we have working and tested conventions for naming and handling of betas and actual releases (especially in CI, which is what I care about most), this seems wasteful to throw away for what is essentially a nominal change ("beta1" becomes "rc"?)

view this post on Zulip Enrico Tassi (Dec 15 2020 at 15:51):

I did not know there was special handling for +betaX in scripts (pointers please). If it is too much we can take back the "renaming".

view this post on Zulip Karl Palmskog (Dec 15 2020 at 16:49):

what I meant was that, for example, it is known that 8.13+beta1 sorts in opam before 8.13.0 and 8.13.dev, and that version number convention also works the same in Nix, and on GitHub

view this post on Zulip Karl Palmskog (Dec 15 2020 at 16:52):

if the X.Y+betaZ is going to change to something completely different for release candidates, the discussion on version numbering might have to be repeated, to ensure it sorts the same everywhere

view this post on Zulip Karl Palmskog (Dec 15 2020 at 16:56):

some of the woes that we had in the opam archive for MetaCoq might be relevant: https://github.com/MetaCoq/metacoq/issues/454

view this post on Zulip Enrico Tassi (Dec 15 2020 at 18:18):

I had in mind something like 8.13+rcwhich has the same properties of 8.13+beta as far as I can tell.

view this post on Zulip Karl Palmskog (Dec 15 2020 at 18:19):

so you know there will always be exactly one rc? (This was the assumption that caused problems for MetaCoq)

view this post on Zulip Enrico Tassi (Dec 15 2020 at 18:28):

The way I read it is that they screwed up the versions (and didn't test it): beta2 and beta are not compared how they thought.

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 09:09):

So it has to be named08 813+rc1 in order to sort nicely with 8.13+rc2?

view this post on Zulip Karl Palmskog (Dec 16 2020 at 09:13):

yes, my point is that if you name the first one 8.13+rc+X, but then decide to release another rc, 8.13+rc2+X will be sorted before the first

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:02):

ban rc and only allow rc1? even if you plan to never rc2, you get the option to change your mind

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:02):

don't let opam restrict your release policies

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:04):

_however_, I'd vote for as many RCs as needed, since tags are free and opam releases cheap

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:07):

Hm, packaging should focus on the needs of packagers who test RCs. So no to a macOS packager (doesn't support opam install), yes to an opam release, and yes to a nix release? or does any packager actually need an installer — and if yes, does it need signing?

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 11:17):

So no to a macOS packager (doesn't support opam install), yes to an opam release, and yes to a nix release? or does any packager actually need an installer — and if yes, does it need signing?

The plan is to sign the installers with all packages as one entity.

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:22):

hmm, since there is no Linux installer, what kind of signature or certification is provided in a form a Linux user can consume?

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:22):

(according to the OCaml user survey, 90%+ of OCaml users are running Linux)

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:29):

Paolo Giarrusso said:

_however_, I'd vote for as many RCs as needed, since tags are free and opam releases cheap

:+1:

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:30):

If RCs (by opposition to betas) are about letting project maintainers know it's time to release a compatible version and not about having lots of users start testing the release, then we really don't need Win + macOS installers at that point and definitely do not need any signature at that point.

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:30):

Paolo Giarrusso said:

don't let opam restrict your release policies

can you clarify here? Are you saying it's OK to have broken version sorting, as long as it's (only) on opam?

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:31):

@Karl Palmskog no, I'm saying "let's use rc1 instead of rc"

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:31):

as above > ban rc and only allow rc1? even if you plan to never rc2, you get the option to change your mind

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:32):

OK sure, that is basically what I'm for as well. (basically just replace beta with rc in the current scheme with beta1, beta2)

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:33):

on > hmm, since there is no Linux installer, what kind of signature or certification is provided in a form a Linux user can consume?

IIUC, that should not affect betas since we wouldn't sign them anywhere, but it might affect releases

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:34):

we already have signing of the Coq tag itself, but Michael was talking about signing Coq + packages (presumably the platform)

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:35):

Karl Palmskog said:

OK sure, that is basically what I'm for as well. (basically just replace beta with rc in the current scheme with beta1, beta2)

Just to insist on this point, this is also my preference. When we started with the +beta scheme with Maxime, we almost made the mistake of not putting a number, but then considered that even if we were only planning one beta, there could be a second unexpected one. It has turned out quite useful since this first release (8.7) happened to have several betas.

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:36):

@Michael Soegtrop and @Karl Palmskog: I assume those are about the platform, and I thought RCs might not get platform releases (but the goal is only to allow cheap RCs)

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:38):

I guess I'm a bit surprised that the beta approach is planned to go away. I thought at least it was useful to switch a bunch of coq-community project CI to 8.XY+betaZ and see what happens. I think we at least found one quite serious regression this way: https://github.com/coq-community/atbr/issues/23

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:39):

with improvements to the Docker image generation process, it's very cheap to mass-switch CI for coq-community projects to a beta and see what happens, but with a release candidate process that doesn't aim for testing, I think there's basically no reason to do this, we might as well only do full releases

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:40):

I thought the idea was the opposite?

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:41):

maybe this discussion is too confusing and I should bow out, but I thought the point was (1) s/beta/rc to clarify that betas are already functionally RCs

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:41):

I mean, have you heard of "release candidate testing"?

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:41):

(2) encourage more testing

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:41):

uh? of course

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:41):

it's not a set phrase, but that's the point

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:41):

a release candidate is something that is already in such a good shape there's little point in testing it

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:42):

that might be the correct meaning, but I'm not sure that's the actual usage

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:42):

also, that sounds like "release"

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:43):

but I was anyway referring implicitly to Théo's comment here that the main point of rc is to signal to packagers to package, which indeed is something quite different from testing

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:44):

So let me clarify things.

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:45):

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:46):

The naming is really secondary. The most important idea is a change in process.

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:46):

so I think it's fair to say that using "release candidate" is something that doesn't signal any form of testing is needed

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:48):

Enrico has noticed that we spend a lot of time / efforts between the branching point and the actual beta release to put the release in good shape at a level that has nothing to do with its actual content (release notes, packaging)...

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:48):

And further, this would be for little point because the beta would be insufficiently tested by end-users.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:49):

Which is something we noticed because users actually start reporting regressions when the final release is out.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:49):

So the idea is not to discourage testing (of course), but to change the release process for more efficiency:

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:50):

  1. reduce the time between branching and releasing the beta / RC (whatever we call it) with the idea that the RC will be just a tag without efforts spent yet on packages / release notes.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:50):

  1. ask maintainers of Coq libraries to test (yes) and release (when sufficiently tested) a compatible version.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:51):

  1. do the work on polishing the release notes, packaging (through the platform) during this period and not before.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:52):

  1. expect that the final release will still contain regressions and that users will report them only at this point, so be ready to publish patch-level releases as frequently as needed so that users can benefit from hotfixes (instead of waiting to have all the bug fixes in like what happened in 8.12.1, which was pretty terrible).

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:53):

The naming change could be discussed separately (and in second instance). First, we need to make sure the new process is right.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:54):

(I'm done)

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:57):

that sounds great, with only one caveat: people porting code might benefit from some release notes/changelog

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:57):

so what will be the time lag between rc and the real release? and will rcs be considered "real releases" and end up on regular opam, as has been suggested?

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:57):

maybe a separate opam repo, since they're more aimed at expert users

view this post on Zulip Karl Palmskog (Dec 16 2020 at 11:58):

for example, if the time is short both between the branch and the rc, and the rc and the real release, then the best course of action for project maintainers is probably to keep testing with dev/master until the real release

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:59):

Paolo Giarrusso said:

that sounds great, with only one caveat: people porting code might benefit from some release notes/changelog

The detailed changelog will be provided but not the release summary with the release highlights.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:59):

Karl Palmskog said:

so what will be the time lag between rc and the real release? and will rcs be considered "real releases" and end up on regular opam, as has been suggested?

This hasn't actually been discussed.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 12:00):

Karl Palmskog said:

so what will be the time lag between rc and the real release? and will rcs be considered "real releases" and end up on regular opam, as has been suggested?

I don't think the time will be made shorter. On the contrary, I think the expectation is to let sufficient time to maintainers to produce new releases so that the final Coq platform only include released code.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 12:01):

Anyway, all this discussion makes me think this change would deserve a CEP, so that it is sufficiently clear what is happening and that everyone has the opportunity to voice concern.

view this post on Zulip Karl Palmskog (Dec 16 2020 at 12:02):

I also think something like CEP would be nice with some more details. It's a bit abrupt to go from "we have branch, betas, release" to "no betas, shorten time to release" (and what to me sounded like "no testing")

view this post on Zulip Karl Palmskog (Dec 16 2020 at 12:09):

as for timing, I think the timeline suggested in this issue for AAC Tactics is very compressed:

This gives a time window of around 14 days (10 working days) to test your project against a non-moving target and take care of issues and tag a release

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 12:10):

Yeah, so it's precisely my understanding that we should extend this time with a non-moving target, not shorten it.

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 16:09):

Paolo Giarrusso said:

I assume those are about the platform, and I thought RCs might not get platform releases (but the goal is only to allow cheap RCs)

I think it is likely that we do platform RC releases with packages as they come in. This should be a cheap process.


Last updated: Dec 07 2023 at 09:01 UTC