Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq library std++ 1.3 / coq 8.11

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq library std++ 1.3 / coq 8.11


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coq library std++ 1.3 / coq 8.11
  • Date: Wed, 25 Mar 2020 14:57:50 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:nGbiCxAhn0FoE4Q2cZvyUyQJP3N1i/DPJgcQr6AfoPdwSPX/oMbcNUDSrc9gkEXOFd2Cra4d16yP7vyrAjVIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRq7oR/MusQWjoZuJag8xgbUqXZUZupawn9lKl2Ukxvg/Mm74YRt8z5Xu/Iv9s5AVbv1cqElRrFGDzooLn446tTzuRbMUQWA6H0cUn4LkhVTGAjK8Av6XpbqvSTksOd2xTSXMtf3TbAwXjSi8rtrRRr1gyoJKzI17GfagdFrgalFvByuuQBww4/MYIGUKvV+eL/dfcgHTmZFR8pdSjBNDp+5Y4YJCOUPIPtYr5Llp1QQsRS+GQeiBOTqyjBSh3/227Ax3+AuHAzC2QAtGc8FvnbJo9XvLKocTP67zKfIwzvAYf1Z1zjy54rUfR4uuvyMQbF9fNDNxUUzGQ7IjFOdopHlMTOP0eQNtnCW4fZ6WuKrhW4stgV/oiWpxscjl4LEgYAVyk3C9SV224s1IMW4SE9ibd6/HppQrDuWN4xsQsMtWmxlvjsxxLMBuZ6+ZicKyZInygbea/yBaYiI4wjsWPyfITdinH5lf66wiAy38Uik0OH8UdO00FlSoipKk9nMqnAN1wHI5cSdS/t9+V+t2TOX1wDS8+1EOk41lbHBJ54m2L4wmZweulnAEC/ugEj6kaGbe0E+9uS17+nreLbrq56GO4J7lg3yKqYjl86lDeglMQUCQXKX9fq92bH5/0D1XrNHheAsnKbDqpDVP8Ebq7a5AwBL1oYj7A6yDzW70NQemnkLNldFeAqGj4TwOFHOJOv4Auylj1SpiDdryOrKMaD/DZnVL3jDlqnufapl5kJBxgc+ycpT649QB70bI//+W1X9udPEAhMhNgy72efnCNFz1oMEXmKPB7eUMKHPsV+O6eIiOOyMZJcUuDrkMPgk6eXugWU+mV8HcqmlxYEXZ2ygHvR6P0WZZmLhjcsGEWcTpwYxUOjqiECZXjNIfHazX6c85ikhB468DIfDQJqtgL2b0yuhEJ1WfDMONlfZM3ryeoCVE9sFdzmVJIc1sDEeWL2wDaMoygqpsifzzachI+bJvCQF49arntNy/qjYkQw43T1yFcWUlW+XBSkglWQRAjQywapXoEpny17F37Iu0NJCEtkG3fpNXE8YKJjTh7h4Ftb9cgfZf5KSV03gRc+pV2JiBuktysMDNh4uU+6piQrOim/3WuZJxYzOP4Q99+fn51a0P9x0ki2U0bEgykI5WY1IL2L03vcipTiWPJbAlgCir4jvdakY23SXpmWey23IuVlZFQ10Sq+DWGgQIEfb/4ygtxHyCoS2ALFiCTNvjMuLK69EcNrs1A4UQe/ifc/BeCS2gWjiXBs=

Hi Jeremy,

Well, that is pretty strange. What does "opam repo list" say?

Also, let me repeat what Theo said earlier:

> I'll add to the excellent advice of Ralf and Li-yao that another
> source of confusion can be the version of opam itself. Please make
> sure that opam --version gives you something above 2.0, otherwise it
> won't work to get recent Coq and Coq packages versions.

It's really important that you use opam 2.

Kind regards,
Ralf

On 25.03.20 14:17, Jeremy Dawson wrote:
> Hi ralf,
>
> Thanks - but I think that is what I have done, have I misunderstood this?
>
> [jeremy@localhost laptops]$ opam switch
> # switch compiler description
> ocaml-base-compiler.4.02.3 ocaml-base-compiler.4.02.3
> ocaml-base-compiler.4.02.3
> -> with-coq ocaml-base-compiler.4.05.0 with-coq
> [jeremy@localhost laptops]$ opam repo add coq-released
> https://coq.inria.fr/opam/released
> [ERROR] Repository coq-released is already set up and points to
> http://coq.inria.fr/opam/released. To change that, use 'opam
> repository
> set-url'.
> [jeremy@localhost laptops]$ opam search coq-stdpp
> # Packages matching: match(*coq-stdpp*)
> # No matches found
> [jeremy@localhost laptops]$
>
> Cheers,
>
> Jeremy
>
>
> On 3/24/20 11:37 PM, Ralf Jung wrote:
>> Hi Jeremy,
>>
>> You need to do the "repo add" when "with-coq" is your current switch.
>> Repositories are per-switch with opam.
>>
>> Kind regards,
>> Ralf
>>
>> On 24.03.20 12:47, Jeremy Dawson wrote:
>>> Hi Theo,
>>>
>>> Thanks - but if you mean doing this, it seems not to be needed
>>>
>>> [jeremy@localhost directory]$ opam repo add coq-released
>>> https://coq.inria.fr/opam/released
>>> [ERROR] Repository coq-released is already set up and points to
>>> http://coq.inria.fr/opam/released. To change that, use 'opam
>>> repository
>>> set-url'.
>>>
>>> Cheers,
>>>
>>> Jeremy
>>>
>>> On 3/24/20 8:01 PM, Théo Zimmermann wrote:
>>>> Hi again Jeremy,
>>>>
>>>> This is probably because you need to add the coq-released repository
>>>> again to your current switch. See "Using opam to install Coq packages"
>>>> on https://coq.inria.fr/opam-using.html.
>>>>
>>>> Théo
>>>>
>>>> Le mar. 24 mars 2020 à 07:23, Jeremy Dawson
>>>> <Jeremy.Dawson AT anu.edu.au>
>>>> a écrit :
>>>>>
>>>>> Thanks all for the replies. I've now got a separate switch with
>>>>> coq 8.11.0 installed, but the std++ library seems to have disappeared
>>>>> since my first email:
>>>>>
>>>>> [jeremy@localhost directory]$ opam switch
>>>>> # switch compiler description
>>>>> ocaml-base-compiler.4.02.3 ocaml-base-compiler.4.02.3
>>>>> ocaml-base-compiler.4.02.3
>>>>> -> with-coq ocaml-base-compiler.4.05.0 with-coq
>>>>> [jeremy@localhost directory]$ opam install coq-stdpp
>>>>> [ERROR] No package named coq-stdpp found.
>>>>> [jeremy@localhost directory]$ opam update
>>>>>
>>>>> <><> Updating package repositories
>>>>> ><><><><><><><><><><><><><><><><><><><><><><>
>>>>> [default] no changes from https://opam.ocaml.org
>>>>> [jeremy@localhost directory]$ opam install coq-stdpp
>>>>> [ERROR] No package named coq-stdpp found.
>>>>>
>>>>> Why might this be, and what should I do from here?
>>>>>
>>>>> Thanks
>>>>>
>>>>> Jeremy
>>>>>
>>>>> On 3/24/20 7:17 AM, Jason -Zhong Sheng- Hu wrote:
>>>>>> Hi Jeremy,
>>>>>>
>>>>>> I would also like to add that it's probably a good idea to use
>>>>>> different
>>>>>> switches for different versions of Coq and in that case it is less
>>>>>> likely to get into the version hassles. it's also more convenient to
>>>>>> switch between switches in emacs too.
>>>>>>
>>>>>> *Thanks,*
>>>>>> *Jason Hu*
>>>>>> *https://hustmphrrr.github.io/*
>>>>>> ****
>>>>>> ------------------------------------------------------------------------
>>>>>> *From:*
>>>>>> coq-club-request AT inria.fr
>>>>>>
>>>>>> <coq-club-request AT inria.fr>
>>>>>> on behalf
>>>>>> of Théo Zimmermann
>>>>>> <theo.zimmi AT gmail.com>
>>>>>> *Sent:* March 23, 2020 12:39 PM
>>>>>> *To:* Coq Club
>>>>>> <coq-club AT inria.fr>
>>>>>> *Subject:* Re: [Coq-Club] coq library std++ 1.3 / coq 8.11
>>>>>> I'll add to the excellent advice of Ralf and Li-yao that another
>>>>>> source of confusion can be the version of opam itself. Please make
>>>>>> sure that opam --version gives you something above 2.0, otherwise it
>>>>>> won't work to get recent Coq and Coq packages versions.
>>>>>>
>>>>>> Le lun. 23 mars 2020 à 16:35, Li-yao Xia
>>>>>> <lysxia AT gmail.com>
>>>>>> a écrit :
>>>>>>>
>>>>>>> Hi Jeremy,
>>>>>>>
>>>>>>> Your current switch uses ocaml 4.02 but coq 8.11.0 depends on ocaml >=
>>>>>>> 4.05 && < 4.10. Create a new switch with a more recent version of
>>>>>>> ocaml,
>>>>>>> (But not too recent, < 4.10) so you can install coq 8.11.
>>>>>>>
>>>>>>> > However it (apparently) tried to reinstall coq 8.8.2 (why?) and
>>>>>>> failed,
>>>>>>> > saying ERROR while compiling coq.8.8.2
>>>>>>>
>>>>>>> The error message includes the logs below that line. There is an
>>>>>>> output-file where to find the complete logs, and also an "### output
>>>>>>> ###" section with the most recent output from the build.
>>>>>>>
>>>>>>> > I think at the moment I have a working version of coq thanks to
>>>>>>> the
>>>>>>> > fedora package of coq, but how can I tell which version of the
>>>>>>> library
>>>>>>> > it is using?
>>>>>>>
>>>>>>> You should probably not get coq via your OS distribution's package
>>>>>>> manager. Only install it with opam.
>>>>>>>
>>>>>>> Most OS distributions move slowly, so they're always a few versions
>>>>>>> behind, and they only provide a limited selection of packages. If you
>>>>>>> want to keep up with the bleeding edge, you should only install OCaml
>>>>>>> and Coq packages through opam.
>>>>>>>
>>>>>>> Don't hesitate to ask for further clarification.
>>>>>>>
>>>>>>> Cheers,
>>>>>>> Li-yao
>>>>>>>
>>>>>>> On 3/23/20 10:31 AM, Jeremy Dawson wrote:
>>>>>>>> Hi Ralf,
>>>>>>>>
>>>>>>>> Thanks - I tried opam update, and then as its output suggested doing
>>>>>>>> opam upgrade, I tried that.
>>>>>>>>
>>>>>>>> However it (apparently) tried to reinstall coq 8.8.2 (why?) and
>>>>>>>> failed,
>>>>>>>> saying ERROR while compiling coq.8.8.2
>>>>>>>>
>>>>>>>> It suggested running
>>>>>>>> opam switch import
>>>>>>>> "/home/jeremy/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/.opam-switch/backup/state-20200323132407.export"
>>>>>>>>
>>>>>>>> which seemed to hang at the point Processing 9/13: [coq: make]
>>>>>>>>
>>>>>>>> I think at the moment I have a working version of coq thanks to the
>>>>>>>> fedora package of coq, but how can I tell which version of the
>>>>>>>> library
>>>>>>>> it is using?
>>>>>>>>
>>>>>>>> Thanks
>>>>>>>>
>>>>>>>> Jeremy
>>>>>>>>
>>>>>>>> On 3/23/20 7:04 PM, Ralf Jung wrote:
>>>>>>>>> Hi Jeremy,
>>>>>>>>>
>>>>>>>>> std++ 1.3 is compatible with Coq 8.8.2 (and even with Coq 8.7.2),
>>>>>>>>> so that cannot
>>>>>>>>> be the problem. It looks like your package definitions are quite
>>>>>>>>> outdated,
>>>>>>>>> given that it cannot even find Coq 8.11.0. Did you try "opam
>>>>>>>>> update"?
>>>>>>>>>
>>>>>>>>> Kind regards,
>>>>>>>>> Ralf
>>>>>>>>>
>>>>>>>>> On 23.03.20 03:26, Jeremy Dawson wrote:
>>>>>>>>>>
>>>>>>>>>> Hi,
>>>>>>>>>>
>>>>>>>>>> > This release of the std++ library adds support for Coq 8.11
>>>>>>>>>> and is
>>>>>>>>>> available in Coq's opam repository.
>>>>>>>>>>
>>>>>>>>>> At present I have Coq 8.8.2 on my machine, and I don't know what
>>>>>>>>>> version
>>>>>>>>>> of the standard library. How do I find that out?
>>>>>>>>>> How do I install a new version of the standard library (ie what do
>>>>>>>>>> I do
>>>>>>>>>> to make use of the fact that it is "available in Coq's opam
>>>>>>>>>> repository"?
>>>>>>>>>>
>>>>>>>>>> Trying opam install coq-stdpp seems to start installing coq-stdpp
>>>>>>>>>> 1.1.0
>>>>>>>>>> which I assume is not what I want.
>>>>>>>>>>
>>>>>>>>>> In any event I assume I have to upgrade to Coq 8.11 to make use of
>>>>>>>>>> it,
>>>>>>>>>> would that be right?
>>>>>>>>>>
>>>>>>>>>> I've tried to do that, following instructions at
>>>>>>>>>> https://coq.inria.fr/opam-using.html but part way through I get
>>>>>>>>>>
>>>>>>>>>> [jeremy@localhost sysadmin]$ opam pin add coq 8.11.0
>>>>>>>>>> [ERROR] Package coq has no known version 8.11.0 in the repositories
>>>>>>>>>>
>>>>>>>>>> What do I need to do?
>>>>>>>>>>
>>>>>>>>>> Thanks
>>>>>>>>>>
>>>>>>>>>> Jeremy
>>>>>>>>>>
>>>>>>>>>
>>

--
Website: https://people.mpi-sws.org/~jung/



Archive powered by MHonArc 2.6.18.

Top of Page