coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Release of Coq 8.13+beta1

From: Richard Ford <richardlford AT gmail.com>
To: coq-club AT inria.fr
Cc: coqdev AT inria.fr
Subject: Re: [Coq-Club] Release of Coq 8.13+beta1
Date: Tue, 8 Dec 2020 18:06:29 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richardlford AT gmail.com; spf=Pass smtp.mailfrom=richardlford AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f171.google.com
Ironport-phdr: 9a23:CZG0BB11QJxZEBBBsmDT+DRfVm0co7zxezQtwd8ZseMQLfad9pjvdHbS+e9qxAeQG9mCtLQd1LSd6v26EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMRm7rwTcusYLjYZiNKo61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoAODAk7WHXkdRwg7xHrxK9qRJ/xIvUb5uUNPp4Y6jRedwXSG5EUstXSidPAJ6zb5EXAuUOM+ZXrYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOakOUOC60KnIwi/Zb/xLxDzz6I/Icgo8rvqRWr9wa8vRxlUvFwzflFWftIjlPz2S1uQXrmeW9OVgVee1hG4mrwF9uCSgxsApioTQgI8e11/L+zljzokvOd24VFB0YcSiEJZItiyXKot7T8MtTW9nuSs0xaAKt5ClcSUWypkq2RDRZvKbf4SU7B/uSeWcLzh4in55ZL6xhwu//0i9xuDiSsW50lBHpTdLnNnLs3ACzR3T6s6fR/ty/0ehxTaP1x3I5e1ePU80kq/bJ4Yuwr4xipoTsVnDETTslEX3i6+bcFgv9Ouw6+n/fLnqupuRO5V3hwz+KKgihNCzDOciPgQTXWWX5OKx36D580LjWrVFlPg2n7HZsJ/EIcQboba0AwpP3YYi7xazFjOm0NYFkXUeIlJJZRCKg5XzN1HBJ/D4Cvi/g1Cynztx2//GObjhDo3MLnjFjrjhYa5w51BAxAc319xS5JJZBqsfLP7vWUL9rsHUAx0kPwCsxuboEtR91ocQWWKVBa+ZNbvfsUWJ5u0zI+mDfpUVtyv5K/gr4P7ul2I2lEQSfamsx5QXaXS4Eu56LEWeZHrgms0BHnsSvgoiUOzqj0WPXiJUZ3arRq4z+jU7CJ+9AorYXYCsgLmB3D+hEZFMZ2BGDEqMEXbyeImeVfcMcjqYItV9nTwcSbihV4gh2Amyuw/90rpoM/Tb+jMDuJL41Nl14vXTmgso+Tx1CcSdyWCNQHtukmMGXT9llJx49Ed60xKI1bVyq/1eD91aof1TASkgMpuJ9e1xC9noVkrvec2FAAK8Q96mCCs9Stw22dMmbEN0GtHkhRfGiXn5S4QJnqCGUcRnupnX2GL8cposkiqU5Owal1AjB/B3Gyi+nKcmrlrcAofIlwOSkKP4Lf1Njh6Iz3+KyC+1hG8dVQdxVavfWnVGPxnZqN344gXJSLr8UO16YDsE8taLL+5xUvOsjVhCQ629atHXYmb0n2XpQBjRmerKY43tdGEQmi7aDRpcng==

The documentation of Primitive Integers, Primitive Floats, and Primitive Arrays makes the point that, when extracting to OCaml, that implementations of Uint63, Float64, and PArray are not provided, but that the user must supply them. But it also points out that the Coq kernel has implementations of all of these. That being the case, could the building and installation of Coq be modified so that the binary form of these libraries is made available for those that would like to compile and execute Coq programs that use these features and are extracted to OCaml? That would save the user the work of extracting these from the Coq sources and having to rebuild them for each Coq version.

Thanks,

Richard L Ford

On Tue, Dec 8, 2020 at 3:13 PM Enrico Tassi <Enrico.Tassi AT inria.fr> wrote:

Dear Coq users,

The Coq development team is proud to announce the immediate
availability of Coq 8.13+beta1:

https://github.com/coq/coq/releases/tag/V8.13+beta1

The full list of changes is available at the following address

https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13

We encourage our users to test this beta release, in particular:

- The windows installer is now based on the Coq platform: This
greatly simplifies its build process and makes it easy to add
more packages. At the same time this new installer was only
tested by two people, so if you use Windows please give us
feedback on any problem you may encounter.

- The notation system received many fixes and improvements, in
particular the way notations are selected for printing changed:
Coq now prefers notations which match a larger part of the term to
abbreviate, and takes into account the order in which notations are
imported in the current scope only in a second instance.
The new rules were designed together with power users, and tested
by some of them, but our automatic testing infrastructure for
regressions in notation printing is still weak. If your Coq library
makes heavy use of notations, please give us feedback on any
regression.

The 8.13.0 release is expected to occur about one month from now.

Best,
--
Enrico Tassi, for the Coq dev team

[Coq-Club] Release of Coq 8.13+beta1, Enrico Tassi, 12/08/2020
- Re: [Coq-Club] Release of Coq 8.13+beta1, Richard Ford, 12/09/2020
  - Re: [Coq-Club] Release of Coq 8.13+beta1, Roger Witte, 12/09/2020
  - Re: [Coq-Club] Release of Coq 8.13+beta1, Richard Ford, 12/16/2020
    - Re: [Coq-Club] Release of Coq 8.13+beta1, Théo Zimmermann, 12/16/2020
      - Re: [Coq-Club] Release of Coq 8.13+beta1, Richard Ford, 12/17/2020
        
        Re: [Coq-Club] Release of Coq 8.13+beta1, Jim Fehrle, 12/17/2020
    - Re: [Coq-Club] Release of Coq 8.13+beta1, Michael Soegtrop, 12/17/2020