The Coq mailing list

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

Hi again Jeremy,

This is probably because you need to add the coq-released repository
again to your current switch. See "Using opam to install Coq packages"
on https://coq.inria.fr/opam-using.html.

Théo

Le mar. 24 mars 2020 à 07:23, Jeremy Dawson 
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> Thanks all for the replies.  I've now got a separate switch with
> coq 8.11.0 installed, but the std++ library seems to have disappeared
> since my first email:
>
> [jeremy@localhost directory]$ opam switch
> #   switch                      compiler                    description
>      ocaml-base-compiler.4.02.3  ocaml-base-compiler.4.02.3
>            ocaml-base-compiler.4.02.3
> ->  with-coq                    ocaml-base-compiler.4.05.0  with-coq
> [jeremy@localhost directory]$ opam install coq-stdpp
> [ERROR] No package named coq-stdpp found.
> [jeremy@localhost directory]$ opam update
>
> <><> Updating package repositories
>  ><><><><><><><><><><><><><><><><><><><><><><>
> [default] no changes from https://opam.ocaml.org
> [jeremy@localhost directory]$  opam install coq-stdpp
> [ERROR] No package named coq-stdpp found.
>
> Why might this be, and what should I do from here?
>
> Thanks
>
> Jeremy
>
> On 3/24/20 7:17 AM, Jason -Zhong Sheng- Hu wrote:
> > 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
> >> >>>
> >> >>