The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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