Coq proof assistant

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0 The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to ... [More] compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results. This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan to release 2021.02.1 as soon as the MacOS installer is ready. The following point releases, starting with 2021.02.2, will focus on including more Coq libraries (and no breaking change). [Less]

The Coq development team is proud to announce the immediate availability of Coq 8.13.1 Hotfix: Fix arities of VM opcodes for some floating-point operations that could cause memory corruption Please see the changelog to learn more about this release.

The Coq development team is proud to announce the immediate availability of Coq 8.13.0 Highlights: Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. Introduction of definitional ... [More] proof irrelevance for the equality type defined in the SProp sort. Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. Please see the changelog to learn more about this release. [Less]

We are happy to announce the release of Coq 8.12.2. This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the exists tactic). See the changelog for details.

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1 Here the full list of changes. We encourage our users to test this beta release, in particular: The windows installer is now based on the Coq ... [More] platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter. The notation system received many fixes and improvements, in particular the way notations are selected for printing changed: Coq now prefers notations which match a larger part of the term to abbreviate, and takes into account the order in which notations are imported in the current scope only in a second instance. The new rules were designed together with power users, and tested by some of them, but our automatic testing infrastructure for regressions in notation printing is still weak. If your Coq library makes heavy use of notations, please give us feedback on any regression. The 8.13.0 release is expected to occur about one month from now. [Less]

We are happy to announce the release of Coq 8.12.1. This release contains numerous bug fixes and documentation improvements. Some bug fix highlights: Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. ... [More] This allowed deriving an inconsistency. Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim. Several bugs with Search. The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual. View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly. See the changelog for details and a more complete list. [Less]

We are happy to announce the release of Coq 8.12.0. Some highlights from this release are: a new binder notation for non-maximal implicit arguments; an improved Search command which accepts more complex queries; many additions to the standard ... [More] library; a restructured reference manual; the deprecation of the omega tactic in favor the lia tactic. Please see the changelog to learn more about this release. [Less]

We are happy to announce the first beta release of Coq 8.12. This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference ... [More] manual. See the changelog for details. As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the updated reference manual. The 8.12 improvements to the reference manual are the start of an effort to improve Coq documentation. We believe the documentation needs considerable work to better serve the needs of the Coq community. Better documentation will encourage more people to learn, teach and use Coq. We need your help for this. We're looking for volunteers who will help rewrite or add new material (such as better explanations and new examples) to the new pages. Writers do not have to be experts on their topic: we can pair writers with experts that can answer questions and provide examples. Indeed, it's a great way to learn more about Coq. We'd also appreciate specific feedback, perhaps detailed, on what needs to be improved, what's missing and what things to improve first. If you are willing to help, please see the dedicated wiki page to learn more. [Less]

The 8.11.2 release of Coq is available. This version brings in a few minor fixes. See the changelog for more details.

The 8.11.1 release of Coq is available. The most salient change in the 8.11.1 release is support for OCaml 4.10.0. See the changelog for more details.