coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Something wrong with the coq-released OPAM repo?
Date: Thu, 30 May 2019 11:33:19 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay11.mail.gandi.net
Ironport-phdr: 9a23:vX/wuxTbGCiVDM7w49YEvuSOztpsv+yvbD5Q0YIujvd0So/mwa6yZhyN2/xhgRfzUJnB7Loc0qyK6vmmADZRqs/c+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiroQnLq8Uan49vJqksxhbJv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqQFhzY7aYI+bN/Rwca3SctwYWWVPUd1cVzBCD46mc4cDE+QMMOReooLgp1UOtxy+BQy0Ce3u0DBPmmP20rc80+s5EA/G3QggEMkQv3TOsNX+KaAfUe+vw6bW0TXMdfVW1S3y6IjJdhAuuu+DXahsccfK0kkvFAPEjk6TqYzkOjOV0/oCs3KB4+pmS+2vl3cqpgdsqTahwccsj5PGhoMTyl3c9CV5xpw1JdyiR0Jhb96kCp1dvDyZOYtuWs4uXXxktSQgxrAEpZK3ZjUGxZYkyhLFdfCKfZWE7gr9WOqMLzp0nm9pdbKhixqo7ESty/DwWtOq3FtFqidIlMTHuGoX2BzJ8MeHT+Nw/ke/1jaL0ADe8vtELl4wlaXBK58t36M8moAWsUvZHy/2nF/6jKCMeUUi5+eo6v7rYrP4qZ+AL4N0iwf+PboymsGnH+g0LwoDU3KZ9OigzrHv4E/0TbZQgvEonKTVrYjWJcEBqa64Bw9V3Jwj6xG6Dzq+39QXh2cILE5fdxKBlYTpNFDOIPTjAvihmVSsjCxmx+vFPrzhGZXNLXnDkLLkfblj8U5Q0gwzws5D555MELEOPOrzWlPttNzfFhI2Lwu0w//+BNph0oMeRHmAD7SCMKLStF+I/vggL/ONZI8Tojb9KuIq6+TgjX8jyhchevyi2oJSY3SlFNxnJV+YaDzimIQvC2AP6yU3z/DjjmqtUDpZamyuF/Yz7zwnAYTgAobHTI23nJSa3zagHZxTY21cTFaBDSG7JM2/R/4QZXfKcYdamTseWO35Et5z5VSVrAb/joFfAK/R8ywcu4jk0YErtfbQhAox9DlxAt7b1WyRHTgtwjE4AgQu1aU6mnRTj0+Z2PEm0edbBMdQ5vZMXx18M5PAnbQjVoLCHznZd9LMc26IB9WrBTZrEoArztsHch8kXdCrjxSF0COsD75TkbGXVsQ5

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