The Coq mailing list

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

Hi Jeremy,

> Sorry for the extra line breaks - it's thunderbird email

You can prevent those by using "Paste as Quotation" in the "Edit" menu.

Okay so the "coq-released" repo is not actually enabled for the with-coq 
switch.
 In current opam versions, "opam repo add foo" should do that, but version 
2.0.1
is quite old and a lot of bugs have been fixed since then.  Could you upgrade 
to
the latest version (2.0.6)?

Kind regards,
Ralf

On 25.03.20 15:20, Jeremy Dawson wrote:
> Hi Ralf,
> 
> thanks - the following output does seem peculiar
> 
> [jeremy@localhost Downloads]$ opam repo list
> [NOTE] These are the repositories in use by the current switch. Use 
> '--all' to
>         see all configured repositories.
> 
> <><> Repository configuration for switch with-coq 
> <><><><><><><><><><><><><><><>
>   1 default https://opam.ocaml.org
> [jeremy@localhost Downloads]$ 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 Downloads]$ opam repo list --all
> # Repository # Url                             # Switches(rank)
> coq-released http://coq.inria.fr/opam/released ocaml-base-compiler.4.02.3(1)
> default      https://opam.ocaml.org            <default>(1) with-coq(1)
>  
> ocaml-base-compiler.4.02.3(2)
> [jeremy@localhost Downloads]$ 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 Downloads]$ opam --version
> 2.0.1
> 
> Sorry for the extra line breaks - it's thunderbird email
> 
> Cheers,
> 
> Jeremy
> On 3/26/20 12:57 AM, Ralf Jung wrote:
>> 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/