coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 06:22:45 +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=PWj8tcR+KLeTEPsWUFKqggzw6eaaeGfSJnAQK9v/PXM=; b=NLIOkNM148ac4GVHRSniC9o9KlJ5KPkqlfkVm/Gz54kDdJl3oKVSoOZqFkKKRIPAtBZNQ1YKO6qXjuJITN8jkEyNVe4uX477Gy0lYtYQpn3Wjccpe/MxdF7SiY0l76Rr1KsB8+8LCXZy9YUpJ/6bn3JAmHumAZGgJywuc+Js72HEnnIlED79F7l5Y2QFx4tpOxtoh43UhOx/6oscLbXbxqg8/ZtvO2oSPyyXkzj6u7AXjHGdWlcLe4Hl9/MllSAhZ0by43uH6L0Zn0m+37/bLRRgkCtLS3OwjSsi/15MCKv16JBoR9FjuH0iaPBcvJMpCCyAG/pRICcWLzE0gLtpQA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=KIsSuK739CMshjvomsXeC7ezNCX70N9w/SyccZUQkClYdzdcJ7OHNBDeaVKJ+pT4LIiYdUCHJVCdlmBv1RKCnl1U8CL6i12H2hfGhClwf4hyNF1RnFYe+MrYDis05nJaJgU/QVx/KDUAkjrFJpxbdH1qPcvMEu3Bq6xwfBhS4M3u9TpY5CiWsiB18jjGMVf6QMRMcNiSfmhUHKinmr0NGiHc0DAbvTWuycDihELk1jnle9FeoPjWUqJ9UcDhE3JcBetwVgIovJOPEGwsL2yjNikdJnXsAIlIdu1msZ0bJ/vodsbb3nHIniuyahLloxoscOyIMVf7EoExuZDaactJwA==
- 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:cTeE9RH19qqsu0dlvD+7rZ1GYnF86YWxBRYc798ds5kLTJ7yosSwAkXT6L1XgUPTWs2DsrQY0raQ6vyxEjxRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi5oAnLq8Ubjo9vJqkyxxbNv3BFZ/lYyWR0KF2cmBrx+t2+94N5/SRKvPIh+c9AUaHkcKk9ULdVEjcoPX0r6cPyrRXMQheB6XUaUmUNjxpHGBPF4w3gXpfwqST1qOxw0zSHMMLsTLA0XTOi77p3SBLtlSwKOSI1/H3Rh8dti61VvQ+hpwdnw4HKfI6VKPRwfqTYfdwARGpBWNtaWyhOD464aocCCfcKM+RFoInnv1YArQWwCxSwBO3hyTFIiH353aw03Os9Hg/J0xctH84XsHnOsNn5KKkfXOCzwaLVzTvDdfRW2TLl5YbMbB8hu++DXbdwcMHMx0cgDQ3Ejk6XqYzjIjiY0eADvHaB7+V+UOKui3QrpQ9rrTmh3ccsjY/Ji5kPxVDC6CV12pg6KsClSEJhe9GkDYJduieHPIV4RcMiRntnuCc8yrAevp60YDIFyJEjxxLFbPyHaYeI7grsVOaQPTd4hG9ld6mlixaz9kis0uz8Vs+u0FZLtCVJiNfMtmoL2hfO6caHUuNw80i91TqVygzf9uNJLVopmafVKZMt2KM8m5QRvEjbESL7nF/6gLKVe0k44OSk9vrrb7T8qpOBNIJ4lwfzObk0lMOlG+Q3KA0OUnCb+eui0L3j+lX0TalEgfMrjqXVrYnWK9kZqaO3GgNV1Z0s5AilAzehzdQYgWIILFVYeBKBkoflIUnOIOr/DfejnVujjCtrx/HBPr3nGJnNKWXDkKvlfbZ67E5cyxA/wsxY55JREr0BIfTzVVHttNHAARI1Lxa4z/v7BNh/zI8SRGyCD62DPK/Pv1KF5PojI+yWa48UvDb9JeIl5/nrjXIhnVESY7Op0oUSaHG4BPhoLV+WYHT3gtcGF2cHpRAxTOr3iFGYTzFcemuyU7gm6TEmEI6mF5vMRpixgLyd2ye2BoFZZmdfClyVDXjoc5iEVOwXZSKJIs5hlyQEWqK7R48g0xGurg76xKB9Iura4C1L/a7kgZJ+4PSWnhUv/xR1Cd6c2ieDVSs8ymgPXno92L11iU170FaKl6Zi1a92D9tWstFESAo/JNbwxvNhDNa6DiDMZNqMWRCKS8q9BjcZR9QshdICfgB0BoPx3Vj4wyO2DupNxPSwD5su//eAjiGtdfY48G7P0ewat3djWtFGbDf0j6hisQXfGsjAjhfBzvf4ReEnxCfIsVy74y+LtUBcXhR3VPyfD3kZew3bocm/716QFubzW4RiCRNIzIu5EoUPatDtigkZFt7eA4yHJlmAwCK3DxvOwa6QZo33fWlbxD/aFEUPjwEU+zCBKBQ6ASCi5WnZCW43GA==
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
>> >>>
>> >>
- [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Théo Zimmermann, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Li-yao Xia, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Théo Zimmermann, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jason -Zhong Sheng- Hu, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/24/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Théo Zimmermann, 03/24/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/24/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/24/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/25/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/25/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/25/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/25/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/24/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jason -Zhong Sheng- Hu, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Théo Zimmermann, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Théo Zimmermann, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Jeremy Dawson, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ralf Jung, 03/23/2020
- Re: [Coq-Club] coq library std++ 1.3 / coq 8.11, Ian Zimmerman, 03/25/2020
Archive powered by MHonArc 2.6.18.