Skip to content

2022.01.0
Compare
Choose a tag to compare
@MSoegtropIMC MSoegtropIMC released this 26 Jan 19:00
· 715 commits to main since this release
2022.01.0
5d6bc01
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

General information

See README for general information and installation of Coq Platform.

See Charter for the concept and goals of Coq Platform.

See CEP52 for the Coq and Coq Platform release cycle.

Major enhancements

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. See the notes below on restrictions which (for the time being) apply to Windows users.

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.

Included Versions of Coq

Recommended Coq version

Preview Coq versions

  • Coq 8.15.0 with a preliminary (beta) package collection - all packages already support Coq 8.15.0, but some packages might still be updated.

Compatibility Coq versions

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

  • 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 8.14.1 package pick
  • Coq 8.13.2 with an updated package collection from September 2021
  • Coq 8.13.2 with the original package collection from February 2021
  • Coq 8.12.2 with the same package collection as the 8.12.2 Coq Platform release

Only the 8.14.1 and the 8.15.0 beta version are available as installers for macOS and Windows and only the 8.14.1 version as snap package. Other versions can be installed using the Coq Platform scripts.

Newly added packages:

  • coq-hammer (not available on Windows)
  • eprover ATP for coq-hammer (not available on Windows)
  • z3_tptp ATP for coq-hammer (not available on Windows)
  • coq-coqprime-generator

See the package collection links in the Coq versions above for details on the included packages.

Removed packages:

  • coq-quickchick has been removed on Windows, because it does not work - we are working on getting it back with the 2022.03 release.

Notes

  • Notes on the macOS installer: This installer is only compatible with macOS 10.13 or higher. Because the application is signed but not "notarized", on macOS 10.15 (Catalina) and 11.X (BigSur), it won't open by default, unless you right-click the application in Finder and chose Open. Cf. #51 to learn more.

  • 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, so this not officially supported. We appreciate bug reports for Apple silicon, but we will ask you for help fixing them.

  • Note on the 8.15 version: This package pick contains Coq 8.15.0, but with a preliminary collection of packages. From a Coq Platform point of view, the Coq 8.15.0 variant is a beta release, so it is called 8.15~beta1. A Coq Platform release with a final package collection for Coq 8.15 is expected end of February 2022. The beta release is complete (all packages compile) and most versions have been confirmed by the package maintainers, so only minor changes are expected.

  • Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics, which reconstruct generated proofs, do work on Windows, though. 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. Also you can manually write CoqHammer tactic calls (that is use it as replacement for auto) on Windows.

Installers

Binary installers are provided for the 2022.01 pick of Coq 8.14 and 8.15 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package is available via the snapcraft.

Assets 10
Loading