coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Something wrong with the coq-released OPAM repo?
Date: Thu, 30 May 2019 05:30:54 -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:Ikw81xXwY/ZhCkoD3ZWEZn1hH0zV8LGtZVwlr6E/grcLSJyIuqrYbBaPt8tkgFKBZ4jH8fUM07OQ7/m5HzVasN3Y7zgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajZVmJ6o+1xfEoGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+27QlMJ/kq1aoA64qRx5x47VYJiZOONic67Tf94XS3NNUtpeWidcBo+xb5cDA+8HMO1FrYfyukEOoAO9CwexBO3h1DFGiWP40qI13OosCh3G0Q46Et4SrHjZttf4OaEPWu611qnIyjDDYutX1jfg8ofIdAohoeyNXbltasTRyFQkGgTKj1WJqIzpIy6Z2/8RvGiA9eZgSf+vi2A7qwFquDSg2NojipTQi48T11vK+yJ5wIMvKt25Tk52ed+kEJ1KtyGbLYR6WM0iQ3twtCc1170Jo5i7fDIXyJQm3h7fauaLfJSP4hLmUuuaPDR2hGp9db6iiRu+7VKsx+zzW8WuzlpHoDBJn9fOu3wVyRDf9syKRuF880u71juC2Rrf5vxFLE02k6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk5O2o5/36bbr4op+cNpF0hR/kMqUuh8CzG/o3PRYSUGiA4+i8yKDj/UPlQLVRlPE5jLTWsI3CKcQaoK62HRNV354+5xuxEzuqytUVkHYdIF5bdh+LlYbkNlPWLPD9F/i/glCskDlxx/DBO73sGprMLmHCkLv9YLpw8FJTyBEpwdBD+pJUBK0BIOnpVkDvqdPYEwc1MxaozOb/FNV9yoQeVHqTDa+eKaPeqEOH5uYyI+aXf4IVozb8K/095/H0l3M5mFkdfbOo3ZQNcny4EO5mcA2lZi/nhc5EGmMXtCI/SvbrgRuMS219fXG3CpIh7zchFYPuNIaLEpC0geTY9CygWIFLaHxdTF2ADCG7JM2/R/4QZXfKcYdamTseWO38E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090su7/Yjlcu6DJoFIKQ33zfFjgozFNNfCc/2eVEmWI40k2KiPQqiOceCcFd++gPXwsnZ8aFkr5KTuvqUweERe+nDVarRtL8UGMvS5c9ztsPfUtnCozkgx3IxGy2HrEJjPqGCIFmqq8=

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

--
Xuanrui (Ray) Qi

xqi01 AT cs.tufts.edu
me AT xuanruiqi.com
https://www.xuanruiqi.com

[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