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: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coq library std++ 1.3 / coq 8.11
  • Date: Tue, 24 Mar 2020 11:47:24 +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=CcXZVs5G+oSa/Bvnp+681/a3Ipbal38ooEOz2duAJro=; b=Khb/GocO7TESBjbAYuSAJiDsLiCWgL9B5lIGab1kIintdx78OCX77cMOx+vW1KqW6ntK0OGnvsbMFuuLgyG/SV+3ieBT3Qf8Q+ItDRJUUpQE+7u6BgyCpkvgdzrzIoIPV/OnpQX2zXNOD27DFwT9VDMiRJe+5UkSDcbgeqmNSbBVG32Wc3AggMWDr0sF5gDpuzLBmH3ciA1VsrWwlcPW/mgdTt4GU6Zd3hcvVeAQ5qyaRFLZ5cQu9YFYb/dtk9+ZvOnPJqioj2deR1UoEiq5XPlQNWEo2cfPfbthU/iR9vvDryWGQIWJrxqHayOrRV2EAddbDKnQrZU/J7JlfnNvgg==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=S+B6utyFuMJzEKDMBjSw+notNiHDZSHZrTr9rtzJdjacrJ2Jx4ACDEcq0QpF7OzrkXPTvnicxTz3+pB3wcINRneIFb5kkALc2/8SsHgIDk9QBU+EwF5sN+ZDE6v7Vd/io7SqurJkwgjH2qfJoUXQLsxTqHXKI/9shLnqgCCAP08QSWGvY2+T7LSbHdpFX0+lqXqauBubiNnUeAha2+27WWFzQjtP1sZHl+77GA3XlFVE2pU+MTE9MYPiF15h2MMtloswA18aWcKD8IXzpJB9ewZZ23Vie0NqFrrKH/fOp5dl+FE4q+1o6mDhaaRuq0gHBop5eIvzwhHpQNl40whDdQ==
  • 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:ZhJqHx1op70jIeYcsmDT+DRfVm0co7zxezQtwd8ZseMSI/ad9pjvdHbS+e9qxAeQG9mCt7Qd1rOempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTWwbalvIBi2sAnaq9Ubj5ZlJqstxRTFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTnjzoJNyMi8GHPlMN/kL5brhympxx62YHUYYeVP+d6cq7Sed4WQGxMVdtTWSNcGIOxd4sBAfQcM+ZEoYfzpFUOohm/BQaiGOzhxTBHi2Tq3aIhyektDR3K0QIiEt8IrX/arM/1NKAXUe2tyKfH0y/DYO1T2Tb99YPGfAouoP+XXbJ3d8ra1E4iGQfbgVWKt4PlOjOU2v4DvWeB4etgTuWvi2g8pg5rpDiv290ghZfUiYII0FzL7zh5zZ8zKNalRkB7ZtukH4FRtyGcL4Z2Q8UiQ3tpuCkg0LEGt4S7cDANyJs73RHfbviHf5KP4hL5W+adOTh4hHN5eLK/mha96lKsyuz7VsSyzV1ErTJFn8HDu3wRzRDf99SLR/ln8ku81zuC1Rrf5vxZLU03jabWJJoszqQtmpcQrUjPBDL6lFv3gaOMa0kp+fWk5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxASUmeV5OqwyKDv8VTkTrpIgPA6i67Zv4vEKsgBoa65HhNV3Z0k6xaiCTepzc4UnWEdLFJCZBKIkZTmO03PIPD/C/ezmVOskCp3x/DCOb3hBZbNImLfn7fmeLZx809cyAwtwtBD/59ZBa0NLOjuVkPtttHUFAI1PgK2zur9Fdlxy4ATVXqKAqCDMaPStVGI5vgoI+mJfIIbvCjyK+I76P7rjX41g1ETcrOn3JsMb3C4GO9rLF+fYXrxmNsOD3oFvhckQOPwlV2OSSRTaGqqX6Ig+jE7D5qrApvERoC0mbCOwCO7HoBNaW1dEVCNEXLod52eVPsWaSKSJNVhkj0eWrS7RY8hz0LmiAivgbFgN6/f/jASnZPlztl8oePJ31lm/jttSs+ZzmulTmdun2pOSSVgj45lpkko6FqZ3K1py9BRCsdU4bsdcAogOJvNicBzFMv1XCrIeMrPRVq7BNy7V2JiBuktysMDNh4uU+6piQrOinb7WuNHp/mwHJUxt5nk8T3pPc8kkSTP0rRnglU7BMJSZzX/1/xPsjPLDouMqH230qOjdKASxinIrT3RxGyT+kxUTUh5TPecBC1NVg7ttd38o3j6YfquBLAgblQT4PO5cvIPUeyyyFJMSbHkJcjUZH+3lyGoHxGUy7iQbY3sPWIAwCHaD0tCmAcWry+L

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