Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq library std++ 1.3 / coq 8.11

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq library std++ 1.3 / coq 8.11


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: Ralf Jung <jung AT mpi-sws.org>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coq library std++ 1.3 / coq 8.11
  • Date: Wed, 25 Mar 2020 13:17:00 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=BSyv8DWr4A/urDBDfke7pp6GKDikqEhXCo379DIO30c=; b=hIJ1pxjLFQP9kKbgisXCQECQ8z2YTJQOVld58kt/hXv1TvI9442ma/5KOv0PEslovbwYe8Zc7GuttM44tjPKhWxUFOKMhd91I1gsb0la3YF0qLe10tyAusGMu9u47J4o81dcBdEz/GQwFsZnM1zBNFXC1EUOsVbCk7Pmtut0u66LcG+9Z2zFoZyKoAuRx0k77vIfUexIdq7FOxRA8wX26Gl1iePlPOUqhe53zs8yTLY7DK0RfOHog5HIxhduRfYClmbUEMKFfdPzf5u2IsBom4p8F1CLmfb1wj4VOL/baTqRfxxSixAHIfRmkdhlUo7Pl+BuKXJIS1AruzRmuVq8lw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=gAObJL9CxeIdYvNIFyZQzte7PQKmx3+EEx/1XLX0MBQYKztsA1LZGPNnL2tVwGiqbR44OG+ol4DYWpxQnIeJfBWyrbhJwNwx0u5a2xjqwClB8XbQZID7bzH6iV4MnsL9QcroEl+13Syjng00Sz3NQr+qn0oY9u5wfpPFnFIqblAX/XDNWA8glo4Dc81vTwQHFQ4GpRV7G2T2kErBKxL8wH3Td16linZ9/3R07+yEldX0HAlOx3fa1wjywtMqrlM4AY2Dnf66YfjR2vtcVjatKaiCODszBhgsNf58PeR8HP8J6wYtKIU8grS2MDOD0XW7jkcszJyskLmyjQ9BoHRn7A==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:5zAJohMsALOCGPiSjm4l6mtUPXoX/o7sNwtQ0KIMzox0K/z5oMbcNUDSrc9gkEXOFd2Cra4d16yP7vyrAzBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRq7oR/MusQWjoZuJbg9xxTUqXZUZupawn9lKl2Ukxvg/Mm74YRt8z5Xu/Iv9s5AVbv1cqElRrFGDzooLn446tTzuRbMUQWA6H0cUn4LkhVTGAjK8Av6XpbqvSTksOd2xTSXMtf3TbAwXjSi8rtrRRr1gyoJKzI17GfagdFrgalFvByuuQBww4/MYIGUKvV+eL/dfcgHTmZFR8pdSjBNDp+5Y4YJCOUPIPtYr5Llp1QQsRS+GQeiBOTqyjBSh3/227Ax3+AuHAzC2QAtGc8FvnbJo9XvLKocUf67wrTUzTvNbP1W1zXy6InGfR89rv+DUql9cdbKxkQ1Cw/JkludpI7jMjiI1uoNqW+b7+94WOyrlWEnsR9+oj2vx8wxhIfGnIwUykvD9SV/3Y04Itm2R1BhYdG6FZtRtzuWOYVsTcIsWGFovyA6x6Yctp69YSgG0oooyAPCa/CdaYeI/wvuWeCMKjl2g3Jlfaiwhxe08UW4y+38UNO00FdQoSZfnNnMrGgB1xvP5cedT/t9+l2t2TGV1wDc8u1ELkE0lbbbK5482bE8jJsTsUPFEyTrm0v2lLebe0o49uSy9ujrfrfrqoWBO4J6iAzyKLkil8KiDeggPQUDW3KX9fm/2bH/50H0QrFHgucrnqTdsJ3XI9kQqLSjDA9PyIkj7g6yDze439QcmnkKNE5IdxyagYT1Jl3COe32AvWxjli1lzdk3O7JMqfmApXQMnjMi7Dhfat760FB0gYz1cpf55VICr4fPP3zRk7xtNveDhMjNAy03vrnCNF61oMZWmKDGLOWMKTXsVOQ5+IvJfeDZJMNtTvyN/Qp/ePigWM7lFMHYKWk05kaZGqlEvloPkmVeX/sjc0AEWcOsAo+VuvqiFiaXDBXeXmyRbwz5jQ7CY68A4nMXI6sgKeG3Ce9BZBZfGZGCk2WHXj2aoqERu0AZziPIsN5iDwLSaChS5M91RGprAL1171nLvPN9iIEsZLjycN66vbIlRAy8Dx0F96S33uMT2FyhGMIRiU50LpxoUxnmR+/1v1CivhWXf5O4fwBBgUnM5H0yvR7TsvtQUTGZNjfDB7sSdK/RDo1U9gZwtkUYk87Fc/oxkTI2DPvCLsInZSKAoY1++TSxS6iCdx6ziPk2bMsikhubsJQLmqgzvpd+hLeAp+Pv0yGjKGsXa0awWjA+HrFxHfY7xIQaxJ5TaiQBSNXXUDRt9msox6bFuL8OfEcKgJEjPW6BO5KZ9nu0QoUbcrYYI2bWFPq3mC6CFCP26+Ga5fsdyMFxiLBBUMYkgcVu3GbKQw5ASTnqGXbXmU3SQDfJnj0+Ow7k0uVC1cuxljQPURnyvy49gNTjOHOE6pCjIJBgz8ornBPJHj42tvXD9SaoA84JvdVZ8577Vtak2vE5VVw

Hi ralf,

Thanks - but I think that is what I have done, have I misunderstood this?

[jeremy@localhost laptops]$ 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 laptops]$ opam repo add coq-released
https://coq.inria.fr/opam/released
[ERROR] Repository coq-released is already set up and points to
http://coq.inria.fr/opam/released. To change that, use 'opam
repository
set-url'.
[jeremy@localhost laptops]$ opam search coq-stdpp
# Packages matching: match(*coq-stdpp*)
# No matches found
[jeremy@localhost laptops]$

Cheers,

Jeremy


On 3/24/20 11:37 PM, Ralf Jung wrote:
> Hi Jeremy,
>
> You need to do the "repo add" when "with-coq" is your current switch.
> Repositories are per-switch with opam.
>
> Kind regards,
> Ralf
>
> On 24.03.20 12:47, Jeremy Dawson wrote:
>> Hi Theo,
>>
>> Thanks - but if you mean doing this, it seems not to be needed
>>
>> [jeremy@localhost directory]$ opam repo add coq-released
>> https://coq.inria.fr/opam/released
>> [ERROR] Repository coq-released is already set up and points to
>> http://coq.inria.fr/opam/released. To change that, use 'opam
>> repository
>> set-url'.
>>
>> Cheers,
>>
>> Jeremy
>>
>> On 3/24/20 8:01 PM, Théo Zimmermann wrote:
>>> 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
>>>>>>>>>
>>>>>>>>
>



Archive powered by MHonArc 2.6.18.

Top of Page