Versioning policy
ejgallego opened this issue · 14 comments
Hi folks,
allow me to open a follow up of aa755#12 here, as I am a bit surprised of the solution adopted there to have a N-copies of the plugin in the repository.
This is IMHO inconvenient as one cannot easily use version control to understand changes among versions, and introduces complexity in the build script which has to understand the Coq version too.
I would indeed suggest that paramcoq follows the policy suggested in coq/coq#8750 , that is to say, have a single copy of the plugin in the repository and one branch for each supported Coq version.
Indeed, let's do this.
Someone can do it or I will look at this in the next days.
Documentation here: coq/coq@b337945
Another inconvenience of the current setup is that even if we change the code for the 8.10 version only, the CI will have to run for all of them.
@ejgallego: I do agree that branches would be more convenient. So I'll merge your related PRs/fix that.
If I remember correctly, the main purpose of this directory structure was to get an OPAM package compiling with multiple versions of Coq. I should add a diff rule in the Makefile to build this package in the new branches based structure. I'm thus keeping this issue open to remind me I have to do it.
Indeed OPAM is a problem and key versioning infrastructure regarding OPAM/Dune are still open.
Usually, once the opam versioning issues are solved git tags should from the base for the OPAM version, thus paramcoq would be versioned v8.10+1.8.2, etc... with the proper version constraints.
This is just one way to do it and not everybody likes it; I consider it the lesser of the available evils so I stick to it for my projects, i.e: https://github.com/ocaml/opam-repository/tree/master/packages/coq-serapi
With this way of versioning, how should the tagging of version numbers for paramcoq be managed?
Before aa755#12, it used to be messy: successive version numbers were attributed to the plugin but for different Coq versions, which was very confusing.
Now, as you suggest in coq/coq#8750, having a 8.x (.y?) tag for each Coq version does not allow to track the global progression of the plugin: if a new feature is implemented, what number should we bump up?
Versioning can still be linear, that is to say, 1.8.2, however, what changes is the release tag, you have to release v8.9+1.8.2 and v8.8+1.8.2 for example.
But indeed, in general it does not make a lot of sense to develop in several Coq versions given how fast is Coq moving these days, so once you move from _v8.8+x_ to _v8.9+x_ usually you wouldn't see too many v8.8 releases.
Anyways this is just a proposal, all that I can say is that at last with this release schema you won't get confused about the Coq version the plugin is supposed to support.
I personally tend to prefer the other way around: 1.8.2+coq8.9 or something like it. This is more in the spirit of semver (which says you can put anything after a + (https://semver.org/#spec-item-10). IIRC there were some OCaml packages using a similar convention as well. And Coq-Equations is following a somewhat similar scheme.
Indeed that's also widely used, to denote "binary" builds; I prefer the other order as indeed for plugins is rare that one plugin works in two coq versions; however for a lib is very common that a branch could work on several versions; but then you wouldn't tag the release, only the build "Debian-style" I think.
@Zimmi48 thanks for the suggestion. OPAM does not follow semver but Debian ordering (https://www.debian.org/doc/debian-policy/ch-controlfields.html#s-f-version) so it will consider 1.8.2+coq8.9 as newer than 1.8.2+coq8.8. I guess this is acceptable as it will anyway consider Coq 8.9 newer than 8.8.
Summing up, we could have
- coq-paramcoq.1.1.1+coq8.7 depending on coq {>= 8.7 & < 8.8}
- coq-paramcoq.1.1.1+coq8.8 depending on coq {>= 8.8 & < 8.9}
- coq-paramcoq.1.1.1+coq8.9 depending on coq {>= 8.9 & < 8.10}
- any package, such as CoqEAL, depending on paramcoq could ask for {>= 1.1 & < 2}
Does that sound a reasonable solution to everyone ?
Sounds good, but note that you will rarely have so many versions of 1.1.1 for example as usually you will move to a newer branch when a new Coq version is released ~6 months.
Indeed that's unfortunate but the current Coq's policy is no ML API compatibility for plugins.
That sounds pretty reasonable. Even if the API provided by Coq is not stable, as long as the user facing features of the plugins are stable, it makes sense to use this versioning scheme so that packages such as CoqEAL can depend on a range of versions indeed.
BTW, this recommended versioning policy is now documented as well in https://github.com/coq-community/manifesto/wiki/Commit,-branch-and-release-policies.
This seems settled then.