Dear Coq community,
On behalf of the Coq development team, the release manager of Coq
8.15, and the Coq Platform team, we are happy to announce the
immediate availability of the Coq Platform version 2022.04.0.
- Coq 8.15 is now stable and the default version proposed in the Coq Platform.
- Flocq has been upgraded to major version 4.0.0. Flocq 3 is still
available under the namespace Flocq3 because CompCert and VST depend
on it. It is expected that the Flocq3 package will be removed when
CompCert and VST become compatible with Flocq 4.
- QuickChick has been re-enabled in compile-from-source mode on Windows
- Several packages have been added: coq-ott and ott,
coq-relation-algebra, coq-mathcomp-algebra-tactics, coq-extructures.
The main supported version is:
- Coq 8.15.1 with an extended and upgraded package collection.
Several compatibility collections with Coq 8.12 to 8.14 are available.
You may install the Coq Platform using opam-based scripts, or Windows,
macOS and Snap binary installers (Coq 8.14 and 8.15 are available in
the Windows and macOS installers, and only 8.15 in the Snap
To learn about the Coq Platform and get access to the installers,
please refer to: