Dear Coq community,
the Coq development team is proud to announce the immediate
availability of the Coq Platform version 2021.02.1, based on Coq
8.13.2.
The Coq platform is a distribution of the Coq proof assistant together
with a selection of Coq libraries. See [1] for the project homepage,
and [2] for the new instructions for getting Coq.
For expert users it provides a set of scripts to compile and install
OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and
many Linux distributions in a reliable and extensible way with
consistent results.
For beginners it provides easy to use binary installers for Windows,
MacOS and Linux.
The next point releases, starting with 2021.02.2, will focus on
including more Coq libraries (and no breaking change).
Highlights for Coq version 8.13.2:
- Fix crash when using vm_compute on an irreducible PArray.set
- Fix crash when loading .vo files containing a vm_compute
normalized primitive array
- Fix Ltac2.Array.init computational complexity
Highlights for the Coq Platform version 2021.02.1:
- DMG installer package for macOS
- Homotopy Type Theory library version 8.13
- The Verified Software Toolchain updated to 2.7.1
Best regards,
Enrico Tassi for the Coq Team
[1]: GitHub - coq/platform: Multi platform setup for Coq, Coq libraries and tools
[2]: Install Coq | The Coq Proof Assistant