coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Something wrong with the coq-released OPAM repo?

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Something wrong with the coq-released OPAM repo?
Date: Thu, 30 May 2019 14:56:59 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=Pass smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:7X6SURUBGgEGjcngI/eRhTxhAFnV8LGtZVwlr6E/grcLSJyIuqrYYxKHt8tkgFKBZ4jH8fUM07OQ7/m5HzVasN3Y6yhKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sBjdutMLjYd8Lqs9xQbFr3VUd+9L2W5mOFWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy243abpyVOvRgcK3Sf90aSnZPUcleWCJMGZ+8YogVAuYdIepVtYvwql0TphW+HwmsA+bvxydJiX/rx6I61f4hERzH3Ac9BNwOsWnfodL6NacLUOC50LTEwC7fYPNNwzv99JXIch49ofGXR75/b9feyVQ2Gg7Dk16ep4vlPzaP2eQMtWiW9+tgVeS1i24msQ59uDavxt0qh4LUhYwV0kjJ+Th3zYopP9G1SUF2bcS6HJZerS2XOYl7Tts8T210vCs20LwLtYS0cSUE0pgr2h/SZv6BfoOV+BzsTvyRLi19hH99eLKwmRKy8U+4x+3iU8m4yUtFoTRBktnNqHACyQbT68iaRvdn4EiuxyqA1xvJ5uFYPEA0m7bbK4U7zrEui5UTrFzPHi7wmErokK+bblgo9+a05+j9Y7jrqYWQO5F6hw3kPKkjmNSzAeEiPQgPW2ib9/681Lrm/UDhT7RKl/w2nrXEvJ3BOcsbvbS1AxNI0oYt9xa/FC2q38oFknkaNF5FYg6Ij5D1O1HSJ/D1Feuwg1O1kDty2//GOqDhDY7WI3jYkLbheK595FRGxAoyy9Bf/ZNUBasbLPL9QE+i/ODfWxQ+Kkm/x/vtINR7zIIXH2yVUYGDN6aHgUKB4PgyIqG1ZcdBqC/8c6EN7OWokWI3hURbcKW0i8hEIEukF+hrdh3KKUHnhc0MRD9T71gOCdfygVjHagZ9InO7XqYy/DY+Ud70BpyFWp2jnKfH0SumTMQPOjJ2T2uUGHKtTL2qHu8WYXvOcMR61CAZW6S6DYItyEP27VKo+/9cNuPRvxYgm9fj2dxyvbyBixR3+TFwDtqQyXDUCWx5lXhOWyI4wLs5rEBgmA+O

I'm using opam 2.0.4. I'm not sure what you mean by "what does the repo
say", but if I `ls .opam/repo/coq-released/packages/coq-mathcomp-
ssreflect/` then the only versions that come up are:

coq-mathcomp-ssreflect.1.6 coq-mathcomp-ssreflect.1.6.2 coq-
mathcomp-ssreflect.1.7.0
coq-mathcomp-ssreflect.1.6.1 coq-mathcomp-ssreflect.1.6.4 coq-
mathcomp-ssreflect.1.8.0

Trying `opam update` multiple times did not help.

Xuanrui

On Thu, 2019-05-30 at 11:33 +0200, Gaëtan Gilbert wrote:
> What's your opam version? What does opam repo say?
>
> Gaëtan Gilbert
>
> On 30/05/2019 11:30, Xuanrui Qi wrote:
> > Hello all,
> >
> > When I browse the coq-released OPAM repo in a browser, I see that
> > the
> > latest version of coq-mathcomp-ssreflect is 1.9.0 (
> > https://coq.inria.fr/opam/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.9.0/opam
> > ). However, when I do:
> >
> > opam update
> > opam install coq-mathcomp-ssreflect
> >
> > It installs v1.8.0 of the package. I've tried specifying version
> > 1.9.0,
> > but it just complains that:
> >
> > [ERROR] Package coq-mathcomp-ssreflect has no version 1.9.0.
> >
> > When I go into ~/.opam/repo/coq-released/packages/coq-mathcomp-
> > ssreflect, I see there's indeed no 1.8.0. Re-running `opam update`
> > or
> > purging and re-adding the repo doesn't help. There seems to be some
> > sort of inconsistency there.
> >
> > Is anyone experiencing the same problem at the moment?
> >
> > -Xuanrui
> >

[Coq-Club] Something wrong with the coq-released OPAM repo?, Xuanrui Qi, 05/30/2019
- Re: [Coq-Club] Something wrong with the coq-released OPAM repo?, Gaëtan Gilbert, 05/30/2019
  - Re: [Coq-Club] Something wrong with the coq-released OPAM repo?, Xuanrui Qi, 05/30/2019
    - Re: [Coq-Club] Something wrong with the coq-released OPAM repo?, Gaëtan Gilbert, 05/30/2019
      - Re: [Coq-Club] Something wrong with the coq-released OPAM repo?, Matthieu Sozeau, 05/30/2019
        
        Re: [Coq-Club] Something wrong with the coq-released OPAM repo?, Xuanrui Qi, 05/30/2019