I was going to say in a README that the project was compatible with "Coq Platform 2021.09.0". But then I realized this isn't true or at least is ambiguous, since a platform release has multiple Coq versions. How should one unambiguously refer to a Coq version+packages in a Platform release? Ideas:
Releases propose several variants. I think what matters is what variant you are using, since subsequent releases will continue to provide past variants (except preview / beta variants).
OK, but how do I refer to "variants" then? (The term "variant" is only used in one place in the Platform release README)
So to shorten a bit the long titles available in the platform repo, I would say "Coq 8.13.2 with the 2021.09 package collection".
I mean, then how would I say, Coq 8.13.2 with the 2021.02 package collection, but please use the 2021.09 release of the platform, which has fixes
Oh! I hadn't considered that you would need to be that explicit.
well, if one wants to be "Platform compatible" in a verifiable way, I think one has to be that precise. For example, there could be a bug that breaks my project in the 2021.02 release of the platform, which was fixed in the 2021.09 release, but I still want the same exact package collection as 2021.02
also, I think this kind of specification is necessary if we want to do Docker images
I think Erik's docker-keeper is up for a challenge for sure, if that's the route we take
very concrete example of what I ended up saying for now: https://github.com/runtimeverification/casper-cbc-proofs/tree/326ce19dcc1ab9d3631c50767309e6aaa6d17f20#building-instructions
unless we quickly reach consensus here, I think this is worth opening a GitHub issue about, but probably I will do that tonight
My impression is that Docker images should only have "variants" / "package sets" available in the latest Platform release. The Platform is a distribution. Similarly to the fact that we update the Docker images for Coq 8.5 when Debian is updated, we should update the Docker images for any package set when the Platform is updated (and there is no point in keeping images based on previous Platform releases).
That's why there was a switch to a multi-version "main" branch.
well, even if you only have the "latest" variants, those variants should have consistent, predictable names (tags in Docker Hub)
Erik already has conventions for how he handles OCaml versions in Coq Docker images (there are always three of them, I believe)
for anyone following this topic who didn't see it, I opened this issue: https://github.com/coq/platform/issues/179
@Karl Palmskog : indeed a good question. In general the combination of Coq version + pick date should be compatible between different releases of Coq Platform but might not be identical. E.g. things like the used OCaml compiler might change. Package version updates are only allowed for pure bug fixes, say an update from Coq 8.13.1 to 8.13.2. So Coq 8.13.2 pick 2021.02 release 2021.09 should be 100% compatible to Coq 8.13.3 pick 2021.02 release 2021.09.
Some day we need to find official names for this. I am sometimes switching between "version" and "pick". I am not sure which is clearer. I guess "pick" is less ambiguous.
So in total we have 3 parameters: the Coq version, the package pick or version (a date) and the Coq Platform release (also a date). The latter should never matter and it is always recommended to use the latest release, but to be 100% sure one should use Coq version + pick/version date + release date.
Btw.: From 2021.11 on the switch name will contain all 3, e.g.
__coq-platform.2021.11.0~8.14~2021.11. This is
release~coq-version~pick. Before I left away the "pick" for the default pick, but I decided to always include the pick. So I would use the postfix of the switch name or the complete switch name as official full version name.
OK, so then I can/should say(?):
This project is compatible with the 2021.09.0 release of the Coq Platform with Coq 8.13.2 and the 2021.09 package pick.
That's not super long but still quite a mouthful...
I would probably just say "This project is compatible with the Coq Platform package pick 2021.09 for Coq 8.13.2" and maybe put into a foot note "Tested with Coq Platform release 2021.09 but any later release or installation method of this package pick should be compatible".
The point is that if the package pick and the release is the same people will most likely automatically take the release from the package pick and if not it should still be compatible.
Any votes on the final terminology "version" vs "package pick"?
"version" is so overloaded already, so "pick" is fine by me
OK, I will adjust the readme files accordingly.
@Karl Palmskog : I did a bit of rework to make the naming more consistent (not just in the readme files but also in scripts, variable names, folder / file names, ...)
I now (hopefully consistently) use this naming:
This sounds great to me, I will update my issue and close it.
it sounds like the most obvious thing to do is to have one Docker image per Platform release switch, so one attempt at tentative Docker tags that would be nice for me as a user for 2021.09.0 is
cc: @Erik Martin-Dorel who might have opinions and might be able to tell if this is doable directly with Docker-keeper.
I'm not convinced that the
-compatibility name makes a lot of sense because as new platform releases get out, there will be more and more compatibility picks.
fine, the left-most suggestions were the "official" ones, the others were just nice-to-haves
I think besides the concrete picks, we should have only 2 "meta" labels: stable and beta. dev is already a "concrete" pick (not well supported as yet, though).
Thanks @Karl Palmskog for pinging me. This naming convention is definitely a question I wanted to suggest BTW, about the Docker packaging of Coq Platform.
Sorry though, I have very little time this week to be able to come up with some answer/feedback; feel free to ping me anew next week anyway.
OK so unless I'm mistaken here are the tags we end up with based on the recent discussion:
2021.11.0 is out we instead get:
Yes, that's what it is. There is not beta as yet. The plan is to do a 2021.11.X release adding a new package pick for 8.15 beta, but keeping all other picks (except for compatible bug fixes like Coq 8.14.2).
Last updated: Jan 29 2023 at 19:02 UTC