The Coq mailing list

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

Hi Jeremy,

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

I am not sure what is wrong with your opam state -- unfortunately opam is 
pretty
fragile and likes to get itself into a bad state, where the best solution is 
to
delete it and start from scratch.

If you are using opam for the library, you have to use oapm for coq, and 
should
uninstall the fedora package to avoid confusion.

If you want to use the fedora package, you will have to install stdpp by hand,
as described at:
<https://gitlab.mpi-sws.org/iris/stdpp/#building-from-source>
But that is not recommended.

Kind regards,
Ralf

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