✔ On the coq-coqprime and coq-coqprime-generator packages · Coq Platform devs & users

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?

Théo Zimmermann (Jul 15 2022 at 07:42):

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).

Laurent Théry (Jul 18 2022 at 09:05):

Karl Palmskog (Jul 18 2022 at 09:08):

@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 v8.16

Karl Palmskog (Jul 18 2022 at 09:10):

since there may be bugfixes, maybe even use v8.16.0 (tag) and 8.16.0 (version number in opam)?

Guillaume Melquiond (Jul 18 2022 at 09:15):

I suggest to do the opposite and just retag the repository accordingly, e.g., git tag 1.2.0 v8.15.

Théo Zimmermann (Jul 18 2022 at 09:30):

Guillaume's suggestion is reasonable. And by not reusing the v prefix, you are clearly marking that you are in a different namespace.

Théo Zimmermann (Jul 18 2022 at 09:32):

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).

Paolo Giarrusso (Jul 18 2022 at 09:44):

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?

Karl Palmskog (Jul 18 2022 at 09:48):

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

Théo Zimmermann (Jul 18 2022 at 09:49):

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).

Paolo Giarrusso (Jul 18 2022 at 09:58):

Laurent Théry (Jul 18 2022 at 15:17):

I am a bit lost, I should change the tag in coqprime but this will not break the link to the download in opam?

Théo Zimmermann (Jul 18 2022 at 15:52):

What Guillaume suggests is to add synonym tags. This will not break opam as long as you keep the existing tags as well.

Laurent Théry (Jul 19 2022 at 09:33):

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.
Thanks!

Karl Palmskog (Jul 19 2022 at 09:36):

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 <repo-url>/releases

Théo Zimmermann (Jul 19 2022 at 09:42):

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.

Théo Zimmermann (Jul 19 2022 at 09:43):

You can even modify past release to point to your tag synonyms instead of the ones that they are currently pointing to.

Notification Bot (Jul 20 2022 at 09:44):

Michael Soegtrop (Jul 20 2022 at 09:45):

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.

Notification Bot (Jul 20 2022 at 09:46):

Laurent Théry (Jul 20 2022 at 09:50):

just realised that there is also an opam for coqprime-generator. So its version number should sync coq-coqprime?

Michael Soegtrop (Jul 20 2022 at 09:54):

@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.

Laurent Théry (Jul 20 2022 at 11:13):

but then how I manage with tag, should I prefix them with coqprime and coqprime-generator?

Karl Palmskog (Jul 20 2022 at 11:14):

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 versionX.Z

Karl Palmskog (Jul 20 2022 at 11:16):

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.

Laurent Théry (Jul 20 2022 at 11:23):

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.

Guillaume Melquiond (Jul 20 2022 at 11:52):

I sometimes synchronize the releases of gappa and 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.

Stream: Coq Platform devs & users

Topic: ✔ On the coq-coqprime and coq-coqprime-generator packages

Julien Puydt (Jul 14 2022 at 22:43):