coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] coq library std++ 1.3 / coq 8.11
Date: Mon, 23 Mar 2020 02:26:57 +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=JoLdfVtLhGJOIKNeTiq+RG09c65qxX543iZTQ+9c/ns=; b=hDJtPuKCuSYO7AIwfIHyePw7+XNdmp8RtLeap4G+qU1bNud+ag8nCm6Ni3tJOxdm6PKx1mE0R9K5XtcelhiHuu4qtZGjNGDXsaPVQkoaj+a270y9j9Vt6zjTxCVI3F6KRScqCer48q9PxAG1j8S2kSIg7K6O7Fcngp6S3aVM+i5l8cKSj4H0+3A8lgEZ2QPxhvyfWxjPexcH6kHkv9zOynKTR3xBy0juCOAAjuUfsL3ke0ah1XFlSRrDO4JeMaTWh9C2AtEU4NqRRZYNDEH6YJedC7Vp8zvQkZ5Y1XUnHqFZ2lNZkOB4lfhqP6ztSV5C3cyGfUVod384QHhYulMO7g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=UFGzQVgq/0BRMCScC/XeH80B0UkqnEDMh2rhCjQ6eTExghB1BVSe3N9qhdlo6u38NTqsvkSXF4UWYaBbpy7TYm8+Mpt3NjNz21RF55IKa7TCONO/5OYbRk3eNLM5EJP18GNxuVz1G+fcoOwdgt5v74MIqZ7JH8GvSIHCyzXhXhe7Ks1Py0Szjkh3ycXkJjYpYmTxSokbIuKKbMU31kBSOcRwkOeHKq/3jNKUOGdWAC4YlGOCKpRuMz03NKaNhXUK2ZY1Gu/8FNDo4lhcYSFs1OFnmVaeUqSBjeU0DyY6U3U6IPmPY0lKjV11Kl0UxZ7w1kH74TFCEiRhUhCpaUNz9Q==
Authentication-results: mail3-smtp-sop.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:eKRlwBEQevJAF9mMeBeRH51GYnF86YWxBRYc798ds5kLTJ76rsiwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWapAQfERTnNAdzOv+9WsuL15z2hKiO/Mj4ZBwArz6ga/smJxKv6A7Vq8M+gI14K693xAGf8VVSfOED525yKFeC1zr1+dy3+tY30SlKtvcwseJJTr79eYwxS6EeATg7dWkosp64/SLfRBeCsyNPGl4dlQBFVk2ctEmjAsXB9xDiv+844xG0eNXsROluCz2k8uFmRAKugTpVb2doolGSsdR5iedgmDzkohV+x4DOZ4TMbqh3eL6bcN8HA2NcDJ8ICn5xR7ikZo5KNNIveOZVq46h+AknkCDmXEyXNbiqzTVFwHjrwac9zuItVxnc2xAtFM4Pt3KSq8jpMKAVUqa+y6yalDg=

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