The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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
>>>>>>>
>>>>>>