Stream: math-comp devs

Topic: 1.11 beta versioning

Karl Palmskog (May 26 2020 at 19:19):

@affeldt-aist one thing that worries me a bit about the 1.11 beta and 1.11.0 is that the versioning system used by OPAM (Debian's) makes the following true:

1.11.0 < 1.11.0+beta1

So people who are using extra-dev need to be aware of this when 1.11.0 is released.

However, if one followed Coq's system, you would have:

1.11+beta1 < 1.11.0

Cyril Cohen (May 26 2020 at 19:20):

Karl Palmskog said:

affeldt-aist one thing that worries me a bit about the 1.11 beta and 1.11.0 is that the versioning system used by OPAM (Debian's) makes the following true:

1.11.0 < 1.11.0+beta1

However, if one followed Coq's system, you would have:

1.11+beta1 < 1.11.0

Yep, I realised that a bit too late :crying_cat:
Maybe it means the next tag should be 1.11.1?

Cyril Cohen (May 26 2020 at 19:22):

Or maybe we can retag everythin 1.11+beta1 instead? (as a tag, and in the opam repos) @Karl Palmskog would that be doable?

Karl Palmskog (May 26 2020 at 19:22):

1.11.1 would work, the following gives no output:

dpkg --compare-versions 1.11.1 lt 1.11.0+beta1 && echo true

Karl Palmskog (May 26 2020 at 19:23):

@Cyril Cohen we can always change the version names in the OPAM extra-dev repo, yes (and also change GitHub tags for consistency)

Karl Palmskog (May 26 2020 at 19:23):

this is a bit rude to extra-dev users, but there are not that many of us, so I personally think it's fine, and will solve problems later on

Karl Palmskog (May 26 2020 at 19:29):

in any case, let me know (e.g., ping here) if you want any help with re-packaging and so on

Reynald Affeldt (May 26 2020 at 19:32):

@Karl Palmskog Thanks for your insights.

Reynald Affeldt (May 26 2020 at 19:34):

We need to communicate the issue to @Yves Bertot as well.

Christian Doczkal (May 26 2020 at 19:53):

Am I understanding that right that we have: 1.10~beta1 < 1.10 < 1.10+beta1 < 1.10.0 (i.e, ~ inserts before, + inserts after, point releases come last - even .0)? :thinking:

Karl Palmskog (May 26 2020 at 20:04):

@Christian Doczkal this is how Debian version naming works, yes. Coq settled on using 8.XY+betaY because other package managers/systems don't like the tilde (at least that's what I remember, there is a long Coq issue explaining the ins and outs). There is nothing much special about the plus, the special one is the tilde.

Christian Doczkal (May 26 2020 at 20:18):

Indeed, assuming that opam lists things in increasing order, there have been some "wild times" 8.5.0~camlp4 8.5.0 8.5.1 8.5.2~camlp4 8.5.2 8.5.3 8.5.dev. Still, I don't see why Coq would opt for this weird scheme rather than let every distro/package manager flag beta releases using their native method. What's the issue you're referring to?

Enrico Tassi (May 26 2020 at 20:48):

I don't recall exactly, but there was a discussion on coq-dev a long ago.

Enrico Tassi (May 26 2020 at 20:53):

My memory stops here: https://sympa.inria.fr/sympa/arc/coqdev/2015-07/msg00129.html but apparently something happened after this ;-)

Karl Palmskog (May 27 2020 at 13:52):

@Théo Zimmermann can you refresh our memory where and why it was decided that Coq betas would follow the naming 8.12+beta1, 8.12+beta2 (instead of 8.12~beta1, etc.). I've tried to search for it but to no avail.

Karl Palmskog (May 27 2020 at 13:53):

from the fragments I remember, it's very likely that having MathComp adopt the same versioning scheme will make sense

Théo Zimmermann (May 27 2020 at 13:54):

The standard opam practice would indeed have rather been 8.12.0~beta1 or something like this, which, by Debian's convention, comes before 8.12.0. However, the Nix version comparison function does not follow Debian's practice and the choice of 8.12+beta1 came up as something reasonable since it would come before 8.12.0 both in opam and Nix.

Théo Zimmermann (May 27 2020 at 13:55):

Coq settled on using 8.XY+betaY because other package managers/systems don't like the tilde (at least that's what I remember, there is a long Coq issue explaining the ins and outs). There is nothing much special about the plus, the special one is the tilde.

So this recollection is indeed correct.

Karl Palmskog (May 27 2020 at 13:56):

thanks! Since most of the MathComp team seems to be leaning towards Nix these days (while there are tons of installs of MC via OPAM), I think it would be good if MC simply follows Coq here, and use 1.11+beta1 and not 1.11.0+beta1

Enrico Tassi (May 27 2020 at 14:21):

What still stinks to me is that if tomorrow we find another relevant package manager that does not like + what do we do? I Think @Christian Doczkal is right in saying that each package manager should mangle the upstream version according to its "version language". We were lucky to find an intersection between opam and nix, but conforming to that policy does not seem a silver bullet to me.

Anyway, I guess math comp should follow it, but we should also document the policy more clearly for the Coq community. Maybe you've already done that in coq-community?

Théo Zimmermann (May 27 2020 at 14:24):

This is a choice which I've never been entirely comfortable with, in part because of the reason you give, and which I never really thought should apply as well to Coq projects, but of course, it was bound to happen.

Théo Zimmermann (May 27 2020 at 14:25):

So you're right. It seems like it is time to document the why of this convention.

Karl Palmskog (May 27 2020 at 14:25):

@Enrico Tassi no, we haven't documented it in coq-community, I would only expect really large projects like Coq and MathComp to follow it, we generally use 8.10.0, 8.10.1, etc., following Coq's version numbers for coq-community

Théo Zimmermann (May 27 2020 at 14:25):

we generally use 8.10.0, 8.10.1, etc., following Coq's version numbers for coq-community

Well...

Théo Zimmermann (May 27 2020 at 14:25):

This is something else that I'm not clear with.

Enrico Tassi (May 27 2020 at 14:25):

I've seen beta releases of Equations, MetaCoq...

Théo Zimmermann (May 27 2020 at 14:26):

It seems like it would have its place on this page: https://github.com/coq-community/manifesto/wiki/Commit,-branch-and-release-policies

Karl Palmskog (May 27 2020 at 14:26):

at least I use 8.11.0, etc., for chapar, Huffman, Buchberger, ..., since this was what was used in coq-contrib

Théo Zimmermann (May 27 2020 at 14:26):

Yep, this is a coq-contrib heritage.

Théo Zimmermann (May 27 2020 at 14:27):

As mentioned in the page mentioned above.

Théo Zimmermann (May 27 2020 at 14:28):

But note that, as mentioned on this page, there also exists another meaning regarding the +.

Théo Zimmermann (May 27 2020 at 14:28):

Like the coq version this is compatible with (as in v1.2+coq8.11)

Karl Palmskog (May 27 2020 at 14:29):

to me, there is a large divide between Coq, MathComp, and possibly std++/Iris/CompCert/VST on the one hand, and most others on the other hand, with respect to versioning, since others are not likely to build much on the latter

Enrico Tassi (May 27 2020 at 14:34):

I don't get exactly what your position is. I just wanted something like "if you make a beta, you are encouraged to use + as a separator since it works in both opam and nix". You seem to talk about versions of packages that mention the version of Coq. I've my opinion on this, but it is not what I'm talking about.

Théo Zimmermann (May 27 2020 at 14:36):

My position is unclear but I've been reluctant to encourage anything until now.

Cyril Cohen (May 27 2020 at 14:41):

I think I vaguely remembered this when we decided to release the last beta of mathcomp, but did not remember exactly why and I could not spot the mistake in 1.11.0+beta even though I felt something was off

Enrico Tassi (May 27 2020 at 15:24):

I guess it makes sense to document this thing somewhere, if coq-community is not the right place it's fine, but the howto-release of mathcomp seems also the wrong place to me. It would work for MC upstream, but others may do the same mistake

Enrico Tassi (May 27 2020 at 15:24):

@affeldt-aist another way to fix things is to name the final 1.11.0.0 (I see your PR, I guess it is fine, but this is another fix to consider)

Théo Zimmermann (May 27 2020 at 15:26):

I actually agree with you that it needs to be documented. But I wouldn't go as far as saying this is the recommended way. Just this is a way of being compatible with opam and Nix.

Reynald Affeldt (May 27 2020 at 15:29):

I guess it makes sense to document this thing somewhere

We decided to go through the burden of renaming the opam packages in order to make the error disappear so that it is less likely to be reproduced in the future (even though as @Karl Palmskog pointed at this is not nice to extra-dev users to whom we apologize).

Cyril Cohen (May 27 2020 at 15:31):

Théo Zimmermann said:

I actually agree with you that it needs to be documented. But I wouldn't go as far as saying this is the recommended way. Just this is a way of being compatible with opam and Nix.

And we recommend to be compatible with both :wink:

Cyril Cohen (May 27 2020 at 15:32):

@affeldt-aist please do not remove the 1.11.0+beta1 tag (not yet at least) while removing the associated release is ok and should be done

Cyril Cohen (May 27 2020 at 15:32):

(that way, unupdaded opam and nix will keep working)

Cyril Cohen (May 27 2020 at 15:35):

I also bet that this naming policy is compatible with github (given the order in which releases appear on https://github.com/math-comp/math-comp/releases)

Reynald Affeldt (May 27 2020 at 15:38):

Cyril Cohen said:

affeldt-aist please do not remove the 1.11.0+beta1 tag (not yet at least) while removing the associated release is ok and should be done

The plan was to remove it but not right away. If you have a precise timeline, please let us know. @Yves Bertot

Cyril Cohen (May 27 2020 at 15:51):

Indeed removing the 1.11.0+beta1 release should be done right before release 1.11.0 (and must be done before).
Removing the tag should never be done.

Théo Zimmermann (Jun 02 2020 at 17:44):

Even if you don't remove the tag just yet, you can already remove the "release" on GitHub. The current situation with two releases is very confusing (there is no way for a user to know which tag will be kept).

Last updated: Dec 05 2023 at 11:01 UTC