The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Jeremy,

I would also like to add that it's probably a good idea to use different switches for different versions of Coq and in that case it is less likely to get into the version hassles. it's also more convenient to switch between switches in emacs too.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Théo Zimmermann <theo.zimmi AT gmail.com>
Sent: March 23, 2020 12:39 PM
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] coq library std++ 1.3 / coq 8.11

 

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