The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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