Stream: MetaCoq

Topic: OPAM version ordering fixes


view this post on Zulip Karl Palmskog (Aug 11 2020 at 09:30):

We have coq-metacoq.1.0~alpha+8.9 and coq-metacoq.1.0~alpha2+8.11. When someone who hasn't pinned Coq and uses Coq 8.11 runs opam install coq-metacoq, he is prompted to downgrade Coq to 8.9.1. This is due to the following:

$ dpkg --compare-versions 1.0~alpha2+8.11 lt 1.0~alpha+8.9 && echo true
true

MetaCoq devs, are there any plans to fix this? For example, you could rename coq-metacoq.1.0~alpha+X.Y to coq-metacoq.1.0~alpha1+X.Y, as discussed elsewhere.

view this post on Zulip Bas Spitters (Aug 31 2020 at 18:27):

Same question from our side. Is a 8.12 release planned?
http://coq.io/opam/coq-metacoq.1.0~alpha2+8.11.html

view this post on Zulip Karl Palmskog (Sep 04 2020 at 12:28):

@Matthieu Sozeau @Théo Winterhalter do you have any objections to if I simply change the opam package version names in the opam archive (alpha+8.X -> alpha1+8.X? I'd really like to see this problem solved.

view this post on Zulip Théo Winterhalter (Sep 04 2020 at 12:37):

I also don't mind (and would gladly welcome the change), but I've not been working on this side of MetaCoq.

view this post on Zulip Karl Palmskog (Sep 04 2020 at 12:38):

well, sometimes we all have to take on new roles when others are busy... OK then, I will just do the change

view this post on Zulip Théo Winterhalter (Sep 04 2020 at 12:46):

Go ahead. :)

view this post on Zulip Théo Winterhalter (Sep 04 2020 at 12:47):

Thanks for fixing that!

view this post on Zulip Matthieu Sozeau (Sep 07 2020 at 09:01):

No problem, go ahead!

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:07):

this is done now, for the record. Let me know if you need help with new packages, etc. - the Metacoq packages are some of the most complex ones we have.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:08):

in particular, are you sure you want to keep the (now-obsolete) dev packages for 8.8 in extra-dev?

view this post on Zulip Matthieu Sozeau (Sep 07 2020 at 09:43):

I think that one can be removed now.


Last updated: Aug 11 2022 at 02:03 UTC