search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

Repo contains strange versions of coq-iris #191

Closed RalfJung closed 7 years ago

RalfJung commented 7 years ago

I just saw via opam show that opam knows about some very strange versions of Iris that we never published: 8.7.dev and dev. It took me a while to realize that this repository is where they are coming from. It seems these strange versions were added by @matejkosik a month ago.

What is the rationale for this? I would prefer for these versions to be removed. First of all, there is no "Iris 8.7", so having a version 8.7.dev of Iris available in opam is at beast misleading. Second, all of these versions are actually just aliases for Iris 3.0.0. This is pretty bad; it means that if we release an Iris 3.1.0, opam upgrade will actually replace that version of Iris with 8.7.dev, effectively downgrading Iris to 3.0.0. And finally, the dev version also is not really the dev version but instead yet another alias for Iris 3.0.0.

My current guess is that you are using these versions in your CI, but then you should really use a dedicated opam archive for that purpose. I have extra-dev added to all my opam instances to obtain the latest version of ssreflect, that should not automatically inflict version numbers that only make sense internally to your CI on coq-iris in my opam installations.

ghost commented 7 years ago

Done. (packages coq-iris.8.7.dev and coq-iris.dev were removed)