The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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/