Comments (15)
Thinking about it, also taking your proposed release process into account, I think using just 8.14+X or 8.14.X is the better option. If the platform becomes the publicly announced "product", people will become less aware of the Coq patch releases and probably don't care how Coq platform X.Y.Z relates to Coq release X.Y.
So we take this as agreed?
from platform.
Totally.
I prefer the +
because it does not risk of being confused with the Coq version, which stays X.Y.Z
from platform.
About Y=beta
, I suggest Y=beta1
to make sure that we account for the (hopefully infrequent) case where we need to release a second beta of the platform (beta
and beta2
are not ordered as we would like in all packaging systems).
from platform.
For the record, the current policy set by @MSoegtropIMC is to have the complete Coq version name, followed by a further number. E.g., 8.13+beta1.0, 8.13.0.1, etc. However, @gares expressed concern about the last digit being important, e.g., if we can add new packages in such a release. I agree with this concern. My proposal would be to separate the platform versioning scheme from the Coq versioning scheme. Since it seems important to highlight the Coq version, it could be done in a later component. E.g., 1.0.0+8.13. Another option which was proposed by @ejgallego is to use date-based version numbers, like in many distributions.
from platform.
I still prefer the Coq version + extra digit variant because:
- the Coq platform should be tightly coupled to the Coq releases
- it is an exceptional startup situation that we might add many packages from one minor version to the next
- I don't see why we should pick a version scheme which is optimized for this startup situation
from platform.
it is an exceptional startup situation that we might add many packages from one minor version to the next
If this becomes a rule, then I'm fine with your reasoning. It was not clear to me that packages were supposed to enter/exit the platform only at major release time (and 8.13 would be an exception to that rule)
from platform.
It was not clear to me that packages were supposed to enter/exit the platform only at major release time
this is not what I meant. I was referring to the fact that if we make a 8.13.0.0 now, the difference between 8.13.0.0 and 8.13.0.1 might be quite massive and this should be an exception. I wouldn't mind adding a few packages on minor versions in the future.
But please keep in mind that it is a documented rule that it should be a rare exception to remove a package from one version to the next.
Btw.: I do get requests for a soon official 8.13.0.0 release with the current feature set, so I think we should really do it.
from platform.
the Coq platform should be tightly coupled to the Coq releases
IIUC, that's not entirely true since the platform may be released a few weeks after a Coq release. Also, as we just discussed, new packages can be added in between major Coq releases.
OTOH, it seems important to everyone here to clearly highlight what is the major version of Coq that's shipped in a given platform version. However, where we disagree (both @gares and me) with you is with the claim that the patch-level number of Coq is important enough to be shown in the version of the platform. We think it doesn't deserve to be shown more than any other relevant piece of data like the patch-level number of the math-comp version that is shipped.
That being said, it could be confusing to have Coq platform's 8.13.1 version to actually include Coq 8.13.0. So a solution to this issue would be to have another component separator. I understand that one would want to put the Coq version first, but then the platform version could be 8.13-1.0. And then, you would go on to 8.13-1.1, 8.13-1.2, etc., every time you update any package (Coq, math-comp, etc.) to a new patch-level (bugfix) release (this could happen every time such a package gets a new bugfix release). And when you add a new package that was not included before you would go to 8.13-2.0. And when you bump to a new major Coq release, you could reset the platform version component: 8.14-1.0.
from platform.
Another suggestion, in line with what I was proposing above, as been made independently by @erikmd in coq/ceps#52 (comment):
Hi all, I know that it has been mentioned above that the precise naming convention could be discussed in a later thread.
However I just wanted to raise a suggestion on a detail (that might impact the suffix that is mentioned in the CEP):
as the Coq platform can be seen as a Coq distribution (core + contributions), would it make sense to always append the suffix with a
+
instead of just a.
? a bit like how some GNU/Linux distributions such as Debian tag the packaged versions… I mean, that would amount to release for Coq 8.14.0:
either coq-platform 8.14.0+beta; coq-platform 8.14.0+0; coq-platform 8.14.0+1 (assuming we keep Coq's whole 3-place version)
or coq-platform 8.14+beta; coq-platform 8.14+0; coq-platform 8.14+1 (assuming we want to "hide" Coq's point release to users, while avoiding any ambiguity w.r.t. what "8.14.1" could mean).
WDYT? (anyway, if you agree with this
+
-suffix idea, the precise naming convention, e.g., the choice between the two items above, could still be discussed apart, obviously)
Both @gares and me prefer the second bullet point.
from platform.
I think this depends a bit on the timing we will see. In case a patch release of Coq comes after a platform release, it is likely we will do a patch release of the platform pretty immediately. Say we are at Coq platform 8.14+1 with Coq 8.14.0 and then comes a patch to 8.14.1 and we would release Coq platform 8.14+2 immediately. Then this relation is not obvious from the version numbers - one would have to read the release notes.
But I don't have a very strong opinion here. I agree that running out of letters is not the only downside of X.Y.Z.W version numbers.
from platform.
have to read the release notes.
That is the crux IMO.
I see the platform as a distribution, its version can hardly provide all the info about what it contains.
Sure, Coq is a key component, but I expect users to care more about the rest. E.g. I care more about the version of my browser or mail client than the version of my Linux kernel. I'm stretching it a little, I admit it, but being able to remove even the Coq version from the platform version would be a sign of success IMO.
from platform.
Fine, so the bottom line is that Coq platform will be named 8.X+Y, where the 8.X matches the Coq version and Y is either "beta" or an increasing number.
from platform.
Yes, I'll update the CEP about the new release cycle with this info ASAP!
from platform.
Thanks for noting this. Yes we should use +beta1.
from platform.
This discussion was concluded on Zulip and the related CEP. In the end, we will use the YYYY.MM.X
scheme where X
is an increasing number starting at 0, beta versions take the version number YYYY.MM+beta1
and YYYY.MM
is only increased for major updates, mostly of Coq, but possibly also of an included package, and in case of removal of a package. Minor updates will only require an increase of X
and may include new packages or updates of packages with only bug fixes.
from platform.
Related Issues (20)
- "Argument list too long" error when installing coq-unimath HOT 8
- Add path length check on root path on Windows (for serapi).
- CI: update Github actions HOT 2
- snap-installed Coq Platform does not work in emacs/ProofGeneral HOT 3
- coq-platform snap: missing icons in coqide HOT 2
- changed code signature in macOS release 8.17.1~2023.08? HOT 2
- coq_makefile broken
- Tracker issue for 8.18 pick creation
- Scripts: opam update is done to late - it must be done before switch creation
- Add coq-tools / coq-bug-minimizer to the platform? HOT 2
- Add coinduction to the Coq Platform
- Add the libraries for undecidability and first-order logic to the Platform HOT 4
- Coq Platform & OCaml 5 HOT 1
- CI: auto cancel workflow runs on new push to PR branch
- Snap release 8.18 / 2023.11.0 HOT 1
- Missing Windows 32bit binaries in 2023.11.0 release HOT 3
- 2023.11.0 on Mac M2: coq-unicoq, coq-relation-algebra fail with seg fault HOT 14
- README incorrectly says there's no binary release for Apple Silicon HOT 1
- Tracker issue for 8.19 package tag creation
- Please avoid Dune 3.13-3.15 HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from platform.