The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

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