coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Coq 8.11+beta1 is out
- Date: Fri, 6 Dec 2019 14:49:50 +0100
- Autocrypt: addr=pierre-marie.pedrot AT inria.fr; prefer-encrypt=mutual; keydata= mQINBFOFpSQBEACyDotTWHydRK+7nzdk+ULrBszrG8Eu7J59+eogMOIOQYKw/joFiTOHnJgG vUzt//PqMURC7tZ72teZHeyLKHwr3a9oOC4W36Wrt4jVGvAnYk60hF20i921ljIN8aj41UYz t+8vgsqgpTCNbcgxhhgXSQ+9n/OZs1yoy6kgIE378HsIhGoGTQxmwdz2k0Aic/qun2Z4CO9v zjTjkUYMJxs4XwVsprMkO/a6qVBkNtEjbwVDJS5d7qzfph2DHJXFyUOPc1GudPI+VW2Abi4A 2US/ycyGMUTYRVaUDUF/GqfqmYgUj4vFvANdB3Roa3XDVxAlkYcNuUqtcpQi9yoU6t+Agobp nqcn+WrtOwrJtvEh3KaaQvI4Yudz3pEmP9KL2VYenUQLuDqVL4KgdCPcAZmpkSC7KCm8Ns2v y69zHasNsPD9YiIXCgpGNZEEUjrG8Si+ej3/3MTqTBQqpSzqTagtGhGANrjEgHj6zdh+plby k/bCYHjX4oDPJZQx6GjmtGPandUAD+SImEwS6WMyCKtUSKJtqD+DVNWiwKAK3+CNxDW/DbRS /N2ACdtItJhFmPAb9Nxs6O27xyPCse4n9fMCT5pLQpDfMmkOQsjr1kCWiOWgjIgfOG64HrxQ Vcjg6mf9EEGVi4kpMhl6RzZ7wsg+ff3w/5NR1e1HX9yj/UbsLwARAQABtDNQaWVycmUtTWFy aWUgUMOpZHJvdCA8cGllcnJlLW1hcmllLnBlZHJvdEBpbnJpYS5mcj6JAj4EEwECACgFAlOF pSQCGwMFCRLMAwAGCwkIBwMCBhUIAgkKCwQWAgMBAh4BAheAAAoJEHkiwB/Zujx745sP/3JA gDdlat/mjqxgpC30Jy5Rnkgblxo/qnEmmhPxSQJKt77JaaDgRfsTrJZcO1K9LN6aLs8dPo26 V29TSt0UJhw5bQcTqi/wlD/ZfQ3I69gn9x6ln3T/7TV/g0tyObbzPYQLsi6p8wgJzO1F3Dr2 9XjEfB2jVs7ancTKbE+5yvwN0v3VCrtG5cFpAdkrMtZzXbXMAxRa7HueUjtxm/ls5zqbwTZ6 1tmJlSJJS+rL43InCxDFRbPO4YzV3z7+sEw/Kpn3HwVQz6y3aDQWqQlq/vF8r0p+3E3CB+h/ h6coMySbpwHZAAMsu9KpQBqGpbAjI5RXvcNJD+7MCqT5LYy/QmULqVaLS7zaspcZc2V2CW1w 4LaZtlMjt4gedGvd/UICuy1pw1GdR3YRlUCQGKnzVp8Cw1Bsd1SbZu0DT/DOt3DHyZLliENu P6PRPQT+Rmj21mDpj+bLJliIpRWQ99/cFA6mmKv7qYk49xWsUL0YxcGabGIObBbMpFoq+Coj 8Gmm10706NrJuhYJMxdxHQNbiV8eYnC6jKnL0F3BPeEloSpw0saq/8PVU7eTwvkrOBTVfiwa UFe7HLFDo6SaRoXJAeBa22ADM4bTQCrf856BMT/4BjHdSUAj4Sq1j1QUHVTWWRVsnNH8Nz10 /n2x8sxQIf8yVX4aN/Km/uz7Xq14hL6suQINBFOFpSQBEADMsZKO9fPtbmyMlS5YQl3B+p5E 17sEJAHSNGA4rfx7Uxij1H1PnTZ0kHhngrhEG1wzv2+1aORCg31Jqrwf//XPbcv6QL4CinD7 QUpbMdrZFo296AkAjuhO8J0LvB8CY3GY6n/G3njy9ISmemEH3dAzOM87Wt0En1dcSYJxdfM2 fmWq6ghlmcQA6A6g1vJ0iKnFcvh/IXHBm1/dtVSOj+2+S4/PLALMCUzugFQLVAKiv7pkdxPz KGxMMEnQuLXjoFivXV6i3q9+0FVVo2t9LfD1EzTNoKwx4866nVnVMU9myd6IS03lKAREmHhb YRKJt+dlmJoqttVczsruFa1SRmzhpp5O2jFWzR0C+SD23s70PXaZ4wcn4TzQKL+tGMRqELLF XepqWcmKnROvX+agmeZK1UxhaIGI0JpPtZHsNGNoU1dbzUE+opzHP5Lpouc5Te+MkXe4wSM6 WrfyTRqUfVr7CeaSozkX/AfgubNnNYmi8RduUjUBjukMEsRchirbyCh1397xK90HDpiiqPy/ PLaUx/sp2vp0TSxGPFtl9CmuSOPVi0HQI51SrnckMA/zQJu6AZyFkbb7fpUi/cPds7AVCLjd mNkLOe77sZ+/D3YKXiHujrpncau+NaQ2SKMrqcRocAeogbd+VV3DFGRgHereAZwHD87ruHeg jEO92QRw/QARAQABiQIlBBgBAgAPBQJThaUkAhsMBQkSzAMAAAoJEHkiwB/Zujx7eSsQAJnw yYs/yiYjwzYdlmGQP1fuG0RG6DwHXZDti9etXRhjgOMvE4+TKqSeM9gXCxdGE7M2aKV+PJvi twb4FRLBOl9YwlHTiV5UIJpcbJv+zvdNSDrlqSSln1Qfqq7HJUvDwSKcY8316pVuF5Q9gknX P/gRG4O8e/fBXuSiL08cDudnkbhSm6zb+VGaewivO0FuuCX4RpYtF4EULbCKof7SSCK3/WWl roX6H3S6dNo/3cUGahj7FfTaQMwHH34P6wGWtJCh7vhaxQ5QdXjj8ZkJfcE03uo+GbF7/xmo g5wxtsFUWhs5G0P534BmahBBKsINIyExt6JYASYL/oouC9c+AOjc3bON7Ae1jeHgx3BSSUju 81x+5MrXAqrLhJ6xDsQpATL7qDcBEHBodo0xlAIgb71qeIU5gZUOw/43eJOnexDFs4VWMthJ z2ot6WdRzYEKt75nuCZqaaUEM+MvOGNZZRM3Dkbqw3Jik1X+lOjc/OgUs+Xn9oaIylA1nojO 9E31ulGmniydilLd+4Vd+WQn0ZEwy75EzDTl0Ne/j8nvLyzeYIWbt5/06mR2L87DIEXmXkAM mwfFXNzzX9gVX8m7owb4CPTf5DCDrguwNdvcPePy81w+fXM7c0Dq+5hzPvh5MRruEDOfqaZw HXQ4ZkGmhsCD6dMF2cKX+EqLjopA136U
Dear coq-club,
The Coq development team is literally delighted by the critical success
of the release of the first beta version of Coq 8.11, available at
https://github.com/coq/coq/releases/tag/V8.11+beta1
Despite a unexpected minor delay of a few days, the release has landed
without too much fuss. The outside temperature is 1°C and there are
already binary packages for MacOS and Win32/64. The other distribution
systems should follow soon. The release manager wishes you a pleasant
bug reporting and thanks your for your trust.
The two main changes brought by Coq version 8.11 are:
- Ltac2, a new tactic language for writing more robust larger scale
tactics, with built-in support for datatypes and the multi-goal tactic
monad.
- Primitive floats in terms. They follow the binary64 format of the IEEE
754 standard, as specified in the Coq.Float.Floats library.
Many other cleanups, improvements and outright features are waiting for
you to discover them at
https://coq.inria.fr/distrib/V8.11+beta1/refman/changes.html?highlight=changes#version-8-11
The 8.11.0 release is expected to occur about one month from now,
assuming no hardcore soundness bug in the meantime.
PMP for the Coq dev team,
16 Frimaire an 228
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Coq 8.11+beta1 is out, Pierre-Marie Pédrot, 12/06/2019
Archive powered by MHonArc 2.6.18.