Karl Palmskog (Dec 15 2020 at 12:31): 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)
Pierre-Marie Pédrot (Dec 15 2020 at 12:37):When was that announced? I don't remember this being discussed.
Karl Palmskog (Dec 15 2020 at 12:39):to me at least, "release candidate" is a form of beta, but apparently not to others
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
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
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
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, ...
Pierre-Marie Pédrot (Dec 15 2020 at 13:02):How are we supposed to perform bugfixes then?
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
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.
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.
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).
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.
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
Paolo Giarrusso (Dec 15 2020 at 14:26):"all breaking changes" is the goal, but not an actual guarantee
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 :-)
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?
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"?)
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".
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
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
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
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.
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)
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.
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?
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
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
Paolo Giarrusso (Dec 16 2020 at 11:02):don't let opam restrict your release policies
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
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?
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.
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?
Karl Palmskog (Dec 16 2020 at 11:22):(according to the OCaml user survey, 90%+ of OCaml users are running Linux)
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:
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.
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?
Paolo Giarrusso (Dec 16 2020 at 11:31):@Karl Palmskog no, I'm saying "let's use rc1 instead of rc"
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
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)
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
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)
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
betawithrcin the current scheme withbeta1,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.
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)
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
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
Paolo Giarrusso (Dec 16 2020 at 11:40):I thought the idea was the opposite?
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
Karl Palmskog (Dec 16 2020 at 11:41):I mean, have you heard of "release candidate testing"?
Paolo Giarrusso (Dec 16 2020 at 11:41):(2) encourage more testing
Paolo Giarrusso (Dec 16 2020 at 11:41):uh? of course
Paolo Giarrusso (Dec 16 2020 at 11:41):it's not a set phrase, but that's the point
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
Paolo Giarrusso (Dec 16 2020 at 11:42):that might be the correct meaning, but I'm not sure that's the actual usage
Paolo Giarrusso (Dec 16 2020 at 11:42):also, that sounds like "release"
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
Théo Zimmermann (Dec 16 2020 at 11:44):So let me clarify things.
Karl Palmskog (Dec 16 2020 at 11:45): Théo Zimmermann (Dec 16 2020 at 11:46):The naming is really secondary. The most important idea is a change in process.
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
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)...
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.
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.
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:
Théo Zimmermann (Dec 16 2020 at 11:50): Théo Zimmermann (Dec 16 2020 at 11:50): Théo Zimmermann (Dec 16 2020 at 11:51): Théo Zimmermann (Dec 16 2020 at 11:52): 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.
Théo Zimmermann (Dec 16 2020 at 11:54):(I'm done)
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
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?
Paolo Giarrusso (Dec 16 2020 at 11:57):maybe a separate opam repo, since they're more aimed at expert users
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
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.
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.
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.
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.
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")
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
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.
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