Karl Palmskog (Nov 18 2021 at 10:51): Karl Palmskog (Nov 18 2021 at 10:51):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:
Théo Zimmermann (Nov 18 2021 at 10:54):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).
Karl Palmskog (Nov 18 2021 at 10:56):OK, but how do I refer to "variants" then? (The term "variant" is only used in one place in the Platform release README)
Théo Zimmermann (Nov 18 2021 at 10:56):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".
Karl Palmskog (Nov 18 2021 at 10:58):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
Théo Zimmermann (Nov 18 2021 at 10:59):Oh! I hadn't considered that you would need to be that explicit.
Karl Palmskog (Nov 18 2021 at 11:00):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
Karl Palmskog (Nov 18 2021 at 11:00):also, I think this kind of specification is necessary if we want to do Docker images
Karl Palmskog (Nov 18 2021 at 11:01):I think Erik's docker-keeper is up for a challenge for sure, if that's the route we take
Karl Palmskog (Nov 18 2021 at 11:03):very concrete example of what I ended up saying for now: https://github.com/runtimeverification/casper-cbc-proofs/tree/326ce19dcc1ab9d3631c50767309e6aaa6d17f20#building-instructions
Karl Palmskog (Nov 18 2021 at 11:07):unless we quickly reach consensus here, I think this is worth opening a GitHub issue about, but probably I will do that tonight
Théo Zimmermann (Nov 18 2021 at 13:31):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).
Théo Zimmermann (Nov 18 2021 at 13:31):That's why there was a switch to a multi-version "main" branch.
Karl Palmskog (Nov 18 2021 at 13:33):well, even if you only have the "latest" variants, those variants should have consistent, predictable names (tags in Docker Hub)
Karl Palmskog (Nov 18 2021 at 13:34):Erik already has conventions for how he handles OCaml versions in Coq Docker images (there are always three of them, I believe)
Karl Palmskog (Nov 18 2021 at 16:39):for anyone following this topic who didn't see it, I opened this issue: https://github.com/coq/platform/issues/179
Michael Soegtrop (Nov 19 2021 at 08:30):@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.
Michael Soegtrop (Nov 19 2021 at 08:34):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.
Karl Palmskog (Nov 19 2021 at 08:44):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...
Michael Soegtrop (Nov 19 2021 at 11:08):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"?
Karl Palmskog (Nov 19 2021 at 11:08):"version" is so overloaded already, so "pick" is fine by me
Michael Soegtrop (Nov 19 2021 at 12:21):OK, I will adjust the readme files accordingly.
Michael Soegtrop (Nov 20 2021 at 17:16):@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:
Karl Palmskog (Nov 21 2021 at 13:56):This sounds great to me, I will update my issue and close it.
Karl Palmskog (Nov 21 2021 at 14:41):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 <release>-<coq-version>-<pick>:
2021.09.0-8.13-2021.09 / 2021.09.0-recommended / latest-recommended2021.09.0-8.13-2021.02 / 2021.09.0-compatibility / latest-compatibility2021.09-0-8.14-2021.09 / 2021.09.0-beta / latest-betacc: @Erik Martin-Dorel who might have opinions and might be able to tell if this is doable directly with Docker-keeper.
Théo Zimmermann (Nov 21 2021 at 18:46):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.
Karl Palmskog (Nov 21 2021 at 19:40):fine, the left-most suggestions were the "official" ones, the others were just nice-to-haves
Michael Soegtrop (Nov 22 2021 at 09:40):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).
Erik Martin-Dorel (Nov 22 2021 at 23:44):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.
Karl Palmskog (Nov 25 2021 at 13:54):OK so unless I'm mistaken here are the tags we end up with based on the recent discussion:
2021.09.0-8.13-2021.09 / latest-stable2021.09.0-8.13-2021.022021.09.0-8.14-2021.09 / latest-betaThen once 2021.11.0 is out we instead get:
2021.11.0-8.14-2021.11 / latest-stable2021.11.0-8.13-2021.092021.11.0-8.13-2021.02 Michael Soegtrop (Nov 26 2021 at 09:05):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: Jun 03 2023 at 04:30 UTC