The Coq mailing list

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

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