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)
When was that announced? I don't remember this being discussed.
to me at least, "release candidate" is a form of beta, but apparently not to others
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
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
e.g. if a package doesn't track master, porting to an rc might make more sense than porting to a beta? not sure
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, ...
How are we supposed to perform bugfixes then?
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
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.
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.
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).
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.
IIUC, the core point is that porting to an -rc
is not pointless because most breaking changes are in
"all breaking changes" is the goal, but not an actual guarantee
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 :-)
@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?
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"?)
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".
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
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
some of the woes that we had in the opam archive for MetaCoq might be relevant: https://github.com/MetaCoq/metacoq/issues/454
I had in mind something like 8.13+rc
which has the same properties of 8.13+beta
as far as I can tell.
so you know there will always be exactly one rc
? (This was the assumption that caused problems for MetaCoq)
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.
So it has to be named08 813+rc1
in order to sort nicely with 8.13+rc2
?
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
ban rc
and only allow rc1
? even if you plan to never rc2
, you get the option to change your mind
don't let opam restrict your release policies
_however_, I'd vote for as many RCs as needed, since tags are free and opam releases cheap
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?
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.
hmm, since there is no Linux installer, what kind of signature or certification is provided in a form a Linux user can consume?
(according to the OCaml user survey, 90%+ of OCaml users are running Linux)
Paolo Giarrusso said:
_however_, I'd vote for as many RCs as needed, since tags are free and opam releases cheap
:+1:
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.
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?
@Karl Palmskog no, I'm saying "let's use rc1 instead of rc"
as above > ban rc and only allow rc1? even if you plan to never rc2, you get the option to change your mind
OK sure, that is basically what I'm for as well. (basically just replace beta
with rc
in the current scheme with beta1
, beta2
)
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
we already have signing of the Coq tag itself, but Michael was talking about signing Coq + packages (presumably the platform)
Karl Palmskog said:
OK sure, that is basically what I'm for as well. (basically just replace
beta
withrc
in 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.
@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)
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
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
I thought the idea was the opposite?
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
I mean, have you heard of "release candidate testing"?
(2) encourage more testing
uh? of course
it's not a set phrase, but that's the point
a release candidate is something that is already in such a good shape there's little point in testing it
that might be the correct meaning, but I'm not sure that's the actual usage
also, that sounds like "release"
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
So let me clarify things.
The naming is really secondary. The most important idea is a change in process.
so I think it's fair to say that using "release candidate" is something that doesn't signal any form of testing is needed
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)...
And further, this would be for little point because the beta would be insufficiently tested by end-users.
Which is something we noticed because users actually start reporting regressions when the final release is out.
So the idea is not to discourage testing (of course), but to change the release process for more efficiency:
The naming change could be discussed separately (and in second instance). First, we need to make sure the new process is right.
(I'm done)
that sounds great, with only one caveat: people porting code might benefit from some release notes/changelog
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?
maybe a separate opam repo, since they're more aimed at expert users
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
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.
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.
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.
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.
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")
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
Yeah, so it's precisely my understanding that we should extend this time with a non-moving target, not shorten it.
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