Dear Coq community,
On behalf of the Coq development team, the release managers of
Coq 8.14 and Coq 8.15, and the Coq Platform team, we are happy to
announce the immediate availability of the Coq Platform version
2022.01.0.
Release highlights:
- An important newly added package, coq-hammer, provides the hammer
tactic, which uses external ATPs (Automated Theorem Provers) to
automatically create Coq proofs. Besides the plugin, Coq Platform
provides two automatically installed ATPs: E-Prover and Z3-TPTP.
- Another interesting new package, coq-coqprime-generator, provides
the executables pocklington, o2v and firstprimes which automatically
generate Coq proofs for the primality of (largish) prime numbers.
The main supported version is:
- Coq 8.14.1 with an extended and upgraded package collection.
Several compatibility versions with Coq 8.13.2 and 8.12.2 are
available. Furthermore, we provide the following preview version:
- Coq 8.15.0 with a preliminary (beta) package collection.
You may install the Coq Platform using opam-based scripts, or Windows,
macOS and Snap binary installers.
To learn about the Coq Platform and get access to the
installers, please refer to:
(The Snap installer is still in preparation and should be available in
a few days.)