I'm a bit surprised to see their version in the platform is 1.1.1, while upstream is using v8.15 as latest tag. How come their is a difference of version numbering?
The Coq Platform uses the version number from the opam archive. I do not know why @Laurent Théry uses a different scheme for the git tag and the opam version number, nor where the correspondence can be found (I would recommend putting it in the release title on GitHub at the very least).
Should I do something?
@Laurent Théry I think it's more forward-looking in this case. We would like the version names of CoqPrime to be consistent with the CoqPrime repo tags. Right now, the best way to do this might be to call the next CoqPrime version
8.16 and the tag
since there may be bugfixes, maybe even use
v8.16.0 (tag) and
8.16.0 (version number in opam)?
I suggest to do the opposite and just retag the repository accordingly, e.g.,
git tag 1.2.0 v8.15.
Guillaume's suggestion is reasonable. And by not reusing the
v prefix, you are clearly marking that you are in a different namespace.
You should even be able to reassociate past releases with a different tag on the GitHub interface (but do not delete the old tags since they are used by opam).
FWIW, Coq-Equations versions _both_ Equations and the underlying Coq version. That seems more robust, unless you know you'll never release two coq-coqprime versions for the same Coq version?
but Equations is a plugin, and I don't think CoqPrime uses any OCaml? Hence, it should usually be compatible with at least two adjacent Coq versions
Indeed, the reason that Equations does this is to be able to release the same "version" of Equations for several Coq versions (using different branches).
Sorry I had misread: this library _is_ compatible with older Coq releases (down to 8.11? https://github.com/thery/coqprime/blob/master/opam/opam), so you suggest 1.1.1/1.2 instead of 8.15/8.16. I agree!
I am a bit lost, I should change the tag in coqprime but this will not break the link to the download in opam?
What Guillaume suggests is to add synonym tags. This will not break opam as long as you keep the existing tags as well.
sorry I didn't understand the difference between tag and release (with Coqprime I've been doing only release so far). Anyway I have added the tags.
I think "Releases" on GitHub can be viewed as a shallow layer on top of Git tags. Basically, some extra information is added about a tag to the GitHub backend, and this makes the tag treated a bit differently than otherwise in the web interface, e.g., the tag/release shows up under
Next time you create a release, when GitHub asks you for a tag name, you can use something like 1.2.1 / 1.3 / etc. instead of v8.X.
You can even modify past release to point to your tag synonyms instead of the ones that they are currently pointing to.
Laurent Théry has marked this topic as resolved.
I am a bit late to the discussion, but I agree with @Guillaume Melquiond that the CoqPrime versioning should be independent of the Coq versioning, since it is not a plugin and doesn't seem to depend a lot on other details. The witness generator is an independent executable.
Laurent Théry has marked this topic as unresolved.
just realised that there is also an opam for coqprime-generator. So its version number should sync coq-coqprime?
@Laurent Théry : not necessarily. E.g. the version numbers for the Coq part and the C++ part of Gappa also don't (always) have the same version:
coq-gappa 1.5.2 A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover gappa 1.4.0 Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic
It might happen that you need to update the Coq part more frequently. If you use the same version number in case you do a synced update depends on how frequent synced updates are. Afaik for Gappa @Guillaume Melquiond syncs the version numbers when he does a synced update.
but then how I manage with tag, should I prefix them with coqprime and coqprime-generator?
I think what Michael is saying is that it's fine to have a tag of a repo called
X.Y, and that the "main" package in the repo has version
X.Y, but then you also have another package generated from the same tag/repo that has version
I think most multi-package projects have similar dilemmas, and it should be fine to choose either to use a single version for all packages, or different versions for different packages.
so I leave the tag as it is (I was not the one that created the opam coqprime-generator) but we assume that it is using the same X.Y than opam coqprime.
I sometimes synchronize the releases of
coq-gappa, but I never synchronize their version numbers. They have been in the past and they might again be in the future, but this is purely an accident.
Last updated: Jan 30 2023 at 10:03 UTC