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 16:05:23 -0400
Authentication-results: mail2-smtp-roc.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:Nxvwfh0i8ZC5wvU8smDT+DRfVm0co7zxezQtwd8Zse0eKPad9pjvdHbS+e9qxAeQG9mCsrQd0bud6vy7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCegbb9oMRm6swHcusYLjYZtJKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpYrhy8pxJx3YDab4ObNPVicKzSctwUSHFdXstSTSFNHp+wYpENAucHIO1Wr5P9p1wLrRamBAasGfngyjlShn/r3K0xzv8vEQDb1wEnENMOqXXUoMnoOKoJTe+117PEzSneb/NYxTf985LEfQ48rvGRRL99d9fax0coFwPAlFqQqIrlMiuU1uQLqWib7vBvWfihi249sw1xrTmvxtssionUnY0Z0EzL9SJ8wIszONa2S1Z7bMa5HJZeqy2WLYp7T8w4T212tis20LMLtJyjcCQU1JgqwwTTZv2df4WH7B/vTvudLDZ6iX9jZbmxnQy98VK6xe35TsS00EhFri5CktTUqHAN0gXf5dWZRft5/0ehxyiA1xrT6+1ZO0w7i7TUJII6wrIqipoTrErDHjPtmEnskqCZa1gk9vCp6+ThfLrmuoeRO5J6hw3iKKgjm8OyDf4mPgUARWSW9+ax2KXm/ULjQbVKivM2krPesJDfPckaqbe5Aw5J3oo+8BuwEyym3M4EnXkaIlJFZAmHg5L3NF7TPfD0Fe2/jEi0kDd32/DGOaXsDYnKLnjaibvuYbJ961NHxwco1tBe55dUCqkbL/7pW0/xssbYDh4jPACuzebnEoY16oRLUmWWR6SdLan6sFmS5+tpLfPfSpUSvWPNNvEj/ePvxUY40QsNZKjxhLMcczakA/p6OAOUbWe60YRJKnsDogdrFL+is1aFSzMGPy/jDZJ53SkyDcedNamGQ4mshLKb2yLiQs9dfSZaF16QCjHle5jWAq5ROhLXGddol3k/bZbkS4Il0kv/5hH/jrZqKuvK9zcJ7NTu2dNuofHOmw0pszF4EpbFij3ffyRPhmoNAgQO8uVnu0UklgWIyu5knvJEDppe6+4bCgo=

Thank you Matthieu. I will follow this issue.

Xuanrui

On Thu, 2019-05-30 at 21:05 +0200, Matthieu Sozeau wrote:
> Hi,
>
> The issue is known, is server-side and its resolution can be
> tracked here:
> https://github.com/coq/opam-coq-archive/issues/730#issuecomment-497441656
>
> Best,
> -- Matthieu
>
> Le 30 mai 2019 à 21:01, Gaëtan Gilbert
> <gaetan.gilbert AT skyskimmer.net
> > a écrit :
>
> > I mean the "opam repo" command
> >
> > Gaëtan Gilbert
> >
> > On 30/05/2019 20:56, Xuanrui Qi wrote:
> > > 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