Ali Caglayan (Oct 20 2021 at 12:15): Ali Caglayan (Oct 20 2021 at 12:15):I am a bit confused. This time we are delaying the Platform release till a bit after 8.14's release. This makes sense. But I see that there is mention of doing them both at the same time. How are libraries in the Platform supposed to release tags for a version of Coq that will not be out yet?
Théo Zimmermann (Oct 20 2021 at 12:19):There is no mention of doing both at the same time. Where do you see this?
Théo Zimmermann (Oct 20 2021 at 12:20):We could have a tighter schedule though, relying on the fact that when the release candidate is out, the platform package maintainers can start tagging a compatible release.
Ali Caglayan (Oct 20 2021 at 12:44):Guillaume Melquiond said:
To be clear (and to reiterate what Theo already said), releases of Coq are meant to be announced at the same time as the Platform. For previous releases of Coq, we were delaying the release so that the Platform would be ready. This time, we have decided to release early, before the Platform is actually ready. But as before, we wait for the Platform to be ready before we officially announce the release.
Théo Zimmermann (Oct 20 2021 at 12:48):"This time" should be understood as "From now on".
Ali Caglayan (Oct 20 2021 at 12:50):OK my misunderstanding then
Ali Caglayan (Oct 20 2021 at 12:50):I am in favour of a tighter release schedule. However sometimes we have teething issues when doing releases, so perhaps it should be possible to delay if need be.
Ali Caglayan (Oct 20 2021 at 12:50):For example, it turned out that the HoTT library had some issues being installed using opam on MacOS
Ali Caglayan (Oct 20 2021 at 12:51):but we managed to resolve this quickly enough
Michael Soegtrop (Oct 20 2021 at 13:06):@Ali Caglayan : it is more of a coincidence that 8.14.0 became ready. The 2021.09 release was a bit delayed cause of the many newly added packages. The plan was to release Coq Platform 2021.09 with 8.14+beta1 based on 8.14+rc1. But then 8.14.0 was released, and I created a Coq Platform +beta2. The final release is planned for November.
Coq 8.14+rc1 was released about a month ago and many packages are already final - about half. coq-hott just made it. But it is no issue if you don't. The 2021.09 release of Coq Platform contains Coq Platform 8.14+beta2 (based on Coq 8.14.0). Whatever is ready is ready - what is not ready comes with the final release. Currently about half of the Coq Platform packages are in the (supposedly) final state in Coq Platform 2021.09 8.14+beta2.
Michael Soegtrop (Oct 20 2021 at 13:08):So the plan is to create a Coq Platform beta 4 weeks after Coq rc1 and the release 4 weeks after Coq .0. The time can be stretched in case there are substantial changes.
Ali Caglayan (Oct 20 2021 at 13:11):What am I supposed to do with a release candidate before the release? I knew for a while that the release candidate was out, but I cannot make a HoTT library release tagging 8.14 until 8.14 has actually been released. In our case, this is because we have documentation/submodules/ci all relying on a the 8.14 version of coq.
Ali Caglayan (Oct 20 2021 at 13:13):Or am I misunderstanding? Are you saying that there is always a 4 week window after a coq release (candidate or not).
Ali Caglayan (Oct 20 2021 at 13:13):We typically tag on the release not the candidate, is that something we should do in the future?
Michael Soegtrop (Oct 20 2021 at 13:23):There will definitely always be a >=4 weeks delays between a Coq .0 release and a Coq Platform .0 release.
What the time Window for the betas of Coq Platform is I can't tell as yet. It might be that this is usually also 4 weeks, it might also be that I do beta releases relatively quickly after Coq .rc1 with whatever works then. This should make it easier for package maintainers to do their work, because dependencies might already be there.
I am not sure I understand in which way you depend on Coq being 8.14.0 and not 8.14+rc1. This sounds like the issue is string manipulation in your make / CI files which should be solvable. E.g. if you use opam, all you have to do is to add the extra-dev repo and say you need at least Coq>=8.14 (8.14<=8.14+rc1<=8.14.0 in opam).
Guillaume Melquiond (Oct 20 2021 at 13:27):Ali Caglayan said:
What am I supposed to do with a release candidate before the release? I knew for a while that the release candidate was out, but I cannot make a HoTT library release tagging 8.14 until 8.14 has actually been released. In our case, this is because we have documentation/submodules/ci all relying on a the 8.14 version of coq.
What is wrong with relying on 8.14+rc1? It is called a "release candidate" for a reason. The only difference between 8.14+rc1 and 8.14.0 is a fix for https://github.com/coq/coq/issues/14915
Ali Caglayan (Oct 20 2021 at 13:29):Coq>=8.14 (8.14<=8.14+rc1<=8.14.0 in opam
I did not know this
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:32):The whole point of a platform is to decouple the release of the software from the release of the wider ecosystem
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:33):I can't find the original post where we first coined the "Coq Platform" term, but certainly that was not the idea we had in mind
Michael Soegtrop (Oct 20 2021 at 13:35):@Ali Caglayan : but please note that the +rc packages live in a separate opam repo called "core-dev" for coq and coqide and "extra-dev" for coq-* packages. You need to add these to your opam switch. If you use a Coq Platform beta created switch this is automatic.
Théo Zimmermann (Oct 20 2021 at 13:40):Emilio Jesús Gallego Arias said:
I can't find the original post where we first coined the "Coq Platform" term, but certainly that was not the idea we had in mind
Maybe not what you had in mind, but definitely something Michael and I had in mind for a long time. Managing the add-ons in the Windows installer had become a big pain and a big hurdle for the Coq release process. This was what started the platform plan.
Théo Zimmermann (Oct 20 2021 at 13:41):And indeed @Ali Caglayan, the point of switching from +beta to +rc was precisely to encourage users to start tagging as soon as the candidate is out (without fear of compatibility issues with the final release).
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:44):Théo Zimmermann said:
Emilio Jesús Gallego Arias said:
I can't find the original post where we first coined the "Coq Platform" term, but certainly that was not the idea we had in mind
Maybe not what you had in mind, but definitely something Michael and I had in mind for a long time. Managing the add-ons in the Windows installer had become a big pain and a big hurdle for the Coq release process. This was what started the platform plan.
What I mean is that in the discussion where the therm "Platform" was suggested (indeed in response to a prior discussion about the distributions of the addons) both the Haskell and OCaml platforms were used as a reference point. Neither of them couple the release of Coq with the release of the platform, and indeed, this view doesn't make a lot of sense, as long as the platform is _opt in_.
If you are gonna make the platform mandatory, that's a whole different setup.
Ali Caglayan (Oct 20 2021 at 13:45):There are two issues with tagging the HoTT library early:
Théo Zimmermann (Oct 20 2021 at 13:47):We use a submodule for Coq (which we intend to get rid of soon). When making a 8.14 release, are we recommending we point this to 8.14+rc1?
Getting rid of the submodule is definitely the solution here.
Théo Zimmermann (Oct 20 2021 at 13:48):coq-docker only gets released when the main release is done
That's wrong. coq-docker for 8.14 has been available for many weeks.
Enrico Tassi (Oct 20 2021 at 13:48):The docker images with 8.14 are there already.
Enrico Tassi (Oct 20 2021 at 13:48):Indeed they are made available as soon as the rc1 tag is in place to let people test in their CI
Ali Caglayan (Oct 20 2021 at 13:50):Alright, so it looks like I delayed the release of the HoTT tag for nothing. I will try to do it correctly for 8.15+rc1
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:52):Théo Zimmermann said:
coq-docker only gets released when the main release is done
That's wrong. coq-docker for 8.14 has been available for many weeks.
But if 8.14 is not announced, how are users gonna notice?
Enrico Tassi (Oct 20 2021 at 13:53):The users which have packages in the platform are notified. The others will be. It is all documented in the CEP https://github.com/coq/ceps/pull/52 if I'm not mistaken.
Théo Zimmermann (Oct 20 2021 at 13:54):But if 8.14 is not announced, how are users gonna notice?
That's a good point, because we may not be sufficiently distinguishing different types of users: end-users vs package maintainers.
Enrico Tassi (Oct 20 2021 at 13:55):https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md#announces
Théo Zimmermann (Oct 20 2021 at 13:55):We could definitely improve the communication to the latter group. What we have decided to delay to the platform release is communication to the former.
Yannick Forster (Oct 20 2021 at 13:55):It sounds a bit like there is an implicit assumption seems that 8.14 is relevant for you if and only if you are a developer of a package in the platform. Is that the case?
Théo Zimmermann (Oct 20 2021 at 13:55):Yes, that's the idea of the CEP linked above.
Théo Zimmermann (Oct 20 2021 at 13:56):If you are an end-user, you should only care about platform releases (like the upcoming 2021.09 or 2021.11).
Théo Zimmermann (Oct 20 2021 at 13:57):Maybe the "if and only if" is a bit strong of course :wink:
Enrico Tassi (Oct 20 2021 at 13:58):The hidden assumption is that today users don't need "just coq" but typically a few other "standard" packages, eg stdpp, mathcomp, bignum...
It may not be the case for metacoq folks (yet) ;-)
Emilio Jesús Gallego Arias (Oct 20 2021 at 14:00):Théo Zimmermann said:
If you are an end-user, you should only care about platform releases (like the upcoming
2021.09or2021.11).
That's effectively making the platform mandatory for all end-users, that's way too strong and leaving many people behind.
Moreover, if that were true, then indeed it makes no sense to release Coq standalone at all then, does it?
Théo Zimmermann (Oct 20 2021 at 14:02):Mandatory, no. That's just a recommendation. And who do you mean we are leaving behind?
Théo Zimmermann (Oct 20 2021 at 14:03):Moreover, if that were true, then indeed it makes no sense to release Coq standalone at all then, does it?
The whole point of the platform is to decouple the two releases processes, so yes...
Karl Palmskog (Oct 20 2021 at 15:51):as a maintainer of many projects in coq-community, some of which are in the Coq platform, the new process going from
is great for predictability and testing in CI, since one can switch to using the branch in CI, then fix all bugs during RC and tag, and then rely on that release is consistent with RC. And this time, we had the Docker images almost the whole way.
In this way, X.0 release is basically mostly an event of interest to packagers of serious library projects to fill up the released opam repo with compatible packages. When the platform for X.0 then comes out, there should normally be a huge selection of packages available, so one can switch for real to X.0 in downstream projects with many dependencies.
Emilio Jesús Gallego Arias (Oct 20 2021 at 16:03):Umm, maybe the problem is the released repos setup? In the sense that the step moving packages to released is mostly a boring one?
Karl Palmskog (Oct 20 2021 at 16:07):the problem we have generally is that people do not synchronize their package releases (into released) with the releases of Coq. Now we curate the important packages in the Platform so they are mostly on track with a new Coq, and we expect most other people to follow. The fact that we have the boring work of moving stuff from extra-dev to released is a good sign, it means we have had stuff working and now we're rolling it out.
The whole staggering between RC, X.0 and platform.X.0 makes perfect sense to me, the debate should in my view be more about details on the notifications and time bounds for staggering, not if this is a good idea at all (i.e., I think it's a great idea).
Paolo Giarrusso (Oct 21 2021 at 01:30):The hidden assumption is that today users don't need "just coq" but typically a few other "standard" packages, eg stdpp, mathcomp, bignum...
It may not be the case for metacoq folks (yet) ;-)
@Enrico Tassi I suspect most Coq users today need Logical Foundations (SF Vol. 1), a smaller tail needs later volumes, and an even smaller one uses any package.
Théo Zimmermann (Oct 21 2021 at 05:59):I would reformulate the claim by @Enrico Tassi to: today, some users are frightened of depending on packages external to the stdlib, that's a shame and the platform is providing a solution to this by making a bunch of packages as accessible as the stdlib.
Théo Zimmermann (Oct 21 2021 at 06:00):That was already the idea with including some plugins like Equations in the Windows add-ons of previous releases, now the package set is extended much beyond.
Théo Zimmermann (Oct 21 2021 at 06:00):That being said, the platform scripts make it just as easy to install just Coq (and possibly CoqIDE) without knowing how to install / use opam, so it's still useful to the users who do not need the extra packages.
Théo Zimmermann (Oct 21 2021 at 06:02):As for the binary installers, the macOS and Snap one do install all the packages, but it's not really a problem for users who don't need them, except in terms of disk space, and the Windows installer asks the user what they want to install.
Karl Palmskog (Oct 21 2021 at 12:12):it might be useful to track the disk space taken by different packages when installed. My intuition is that almost all medium-sized Coq plugins/libraries take at most 10 MB each, and then we have outliers such as VST and CompCert, which may take upwards of 100MB
Michael Soegtrop (Oct 21 2021 at 13:08):Théo Zimmermann said:
I would reformulate the claim by Enrico Tassi to: today, some users are frightened of depending on packages external to the stdlib, that's a shame and the platform is providing a solution to this by making a bunch of packages as accessible as the stdlib.
yes - the Coq Platform essentially came from the difficulties in managing my own Coq developments, which depend on about 10..15 Coq Platform packages. Without an organized release process it was hard to find a point in time and a combination of versions which compiles - that opam couldn't find a solution for my combined package request (with specifying just the Coq version and keeping all other versions open) was quite common and more the rule than an exception. Also it was common that package combinations which should work according to opam did not compile. Part of this issue was that different packages I needed required different versions of basic dependencies like Flocq. After such an experience you think twice before you depend your projects on any additional packages, because the likelihood of ending up in a mess increases exponentially with the number of packages. I hope that Coq Platform is now large enough so that at least common prerequisites of not included packages one might need are in Coq Platform, so that such packages likely agree on the version of dependencies they require - that is the version in Coq Platform. So even if someone needs a few extra packages, it is highly likely that this will work a short time after a Coq Platform release.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:23):Théo Zimmermann said:
I would reformulate the claim by Enrico Tassi to: today, some users are frightened of depending on packages external to the stdlib, that's a shame and the platform is providing a solution to this by making a bunch of packages as accessible as the stdlib.
Actually I'd like to solve that in a very different manner, namely integrating Coq with the package manager, we should chat some day!
Paolo Giarrusso (Oct 21 2021 at 13:52):Actually I'd like to solve that in a very different manner, namely integrating Coq with the package manager, we should chat some day!
FWIW, this argument for the platform seems to require at least something like Haskell’s stackage to coordinate versions; the Scala ecosystem also does some release coordination.
Paolo Giarrusso (Oct 21 2021 at 13:55):actually releasing binaries also has some upsides, but it doesn’t work for expert users unless it integrates well with the package manager — that’s a challenge for both Coq and Haskell, but at least the Coq Platform has an expert mode where it _does_ integrate with opam :-)
Last updated: Apr 19 2024 at 04:02 UTC