The Coq mailing list

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

Hi Theo,

Thanks - I wasn't aware of the details in your second para, but what I 
am trying to do is to get access to the features described in the email 
to this list of 21/3/20, where it said

we are pleased to announce the release of std++ 1.3: an extended 
"standard" library for Coq. The std++ library includes a large selection 
of definitions and lemmas on common data structures like lists, 
relations, sets, finite sets, finite maps, and finite multisets; a 
number of type classes for common properties of types (e.g., decidable 
equality, countable, finite, infinite, inhabited); and useful tactics.

This release of the std++ library adds support for Coq 8.11 and is 
available in Coq's opam repository.

I was assuming that this std++ library is what opam refers to as coq-stdpp

Cheers,

Jeremy Dawson


On 24/3/20 1:40 am, Théo Zimmermann wrote:
> Hi Jeremy,
> 
> Indeed, opam is not really user-friendly when you are not used to it
> and when the copy-paste instructions do not work out of the box.
> 
> But before trying to explain to you how to tackle this issue, would
> you mind confirming that you are indeed trying to update stdpp which
> is a library which *extends* the standard library of Coq, and not the
> standard library itself?
> 
> The standard library is bound to the version of Coq: you get updates
> whenever you update Coq. External packages such as stdpp provide
> additional functionalities and can be installed via opam, but then it
> requires you to install Coq via opam as well (as opposed to using your
> distribution's package manager).
> 
> Théo
> 
> Le lun. 23 mars 2020 à 15:32, Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
>  a écrit :
>>
>> 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
>>>>
>>>