The Coq mailing list

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

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