#Coq programming language generator

Since the CoqHammer tactic running on macOS and Linux creates simple and fast Coq tactic call snippets which are intended to replace the slow generator tactics, it is possible to use the auto generated tactics on Windows as well. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them. Notes on Apple ARM silicon: Coq Platform has been tested by users on Apple silicon (M1), but we have no means to run CI tests on Apple silicon (yet), so this not officially supported. Because the application is signed but not 'notarized', it won't open by default, unless you right-click the application in Finder and chose Open. Notes on the macOS installer: This installer is only compatible with macOS 11.0 or higher. Other versions can be installed using the Coq Platform scripts. Only the 8.14.1 and the 8.15.2 version are available as installers for macOS and Windows and only the 8.15.2 version as snap package.

Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release.Coq 8.13.2 with the original package collection from February 2021.Coq 8.13.2 with an updated package collection from September 2021.Coq 8.13.2 with an updated package collection from January 2022 - this package pick is made to be as compatible as possible with the first 8.14.1 package collection.Coq 8.14.1 with the first package collection from Jan 2022.

Coq 8.14.1 with an updated package collection from Apr 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection.

They can be installed in parallel with other versions of Coq (Coq Platform will create separate opam switches for each Coq version). The compatibility versions are intended to help porting packages from an older to the latest release.

Coq 8.15.2 with the same package collection as the 2022.04.0 release.

Included Versions of Coq Recommended Coq version

A wrong standard library axiom for the native float implementation allowed a proof of false.

Various issues introduced in CoqIDE by the implementation of the Ltac Debugger have been fixed, most notably a quadratic blow up in parsing time.

This is a bug fix release with a few important fixes: The latest release version of Coq has been updated from 8.15.1 to 8.15.2 (see Coq 8.15.2 release notes). See CEP52 for the Coq and Coq Platform release cycle. See Charter for the concept and goals of Coq Platform. See README for general information and installation of Coq Platform.

Coq programming language