Skip to content

2022.04.0
Compare
Choose a tag to compare
@MSoegtropIMC MSoegtropIMC released this 20 Apr 17:34
· 609 commits to main since this release
2022.04.0
1af4a9d
This commit was created on github.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
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

The latest release version of Coq has been updated from 8.14.1 to 8.15.1 (see Coq 8.15 release notes)

QuickChick has been re-enabled on Windows, but only in "compile from sources" mode and not via the installer (this also applies to macOS and Snap).

Two packages have been added to the full level:

  • coq-ott and ott, a domain specific language and too chain for formalizing programming languages and calculi
  • coq-relation-algebra, a modular library for the algebra of relations with several high-level reflexive proof automation tactics

In addition two packages have been added to the extended level:

  • coq-mathcomp-algebra-tactics, a library with field and ring tactics for mathcomp
  • coq-extructures, a library for finite sets, maps and permutations which provide axiom free extensionality

Major changes

  • coq-flocq has been updated to version 4.0.0, which is (slightly) incompatible with Flocq 3. Since coq-vst and coq-compcert have not yet switched to Flocq 4, Flocq 3 is included as a separate package - see the notes below for details.

Included Versions of Coq

Recommended Coq version

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.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.1 package collection
  • Coq 8.14.1 with the first package collection from Jan 2022
  • 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.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.1 version are available as installers for macOS and Windows and only the 8.15.1 version as snap package. Other versions can be installed using the Coq Platform scripts.

Newly added / enabled packages:

  • coq-quickchick is now available in "compile from sources" mode on all platforms, but not (yet) via installers
  • coq-ott and ott, a domain specific language and too chain for formalizing programming languages and calculi
  • coq-relation-algebra, a modular library for the algebra of relations with several high-level reflexive proof automation tactics
  • coq-mathcomp-algebra-tactics, a library with field and ring tactics for mathcomp
  • coq-extructures, a library for finite sets, maps and permutations which provide axiom free extensionality

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

Removed packages:

(None)

Notes

  • Notes on the macOS installer: This installer is only compatible with macOS 11.0 or higher. 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. 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.

  • 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.

  • Note on Flocq: there is a new version 4.0 for coq-flocq which is not compatible with the previous 3.X versions. Since some packages are not yet compatible with Flocq 4.0, notably coq-compcert, the 2022.04 picks contain both, coq-flocq.4.0.0 and coq-flocq.3.4.3. Since one cannot install two version of one package, a new package called coq-flocq3 has been added which uses Flocq3 rather than Flocq as logical path. This way Flocq 3.X can be selected by using Flocq3 in the Require commands and Flocq 4.X can be selected by using Flocq in the Require commands. The package coq-compcert has been patched to require Flocq3. For convenience the proof automation packages used for float proofs, coq-gappa and coq-interval are also available in a Flocq 3.X and Flocq 4.X variant. The Flocq 4.X variants have the usual logical path, the 3.X variants use the logical paths IntervalFlocq3 and GappaFlocq3. The Flocq 3.X packages will be removed as soon as CompCert and VST are compatible with Flocq 4.0, but the opam packages will remain available and can be installed if needed.

  • Note on QuickChick: QuickChick requires an OCaml compiler to run. The binary installers for Coq Platform do not provide OCaml, so QuickChick does not work with the binary installers for macOS, Windows and Snap. It is recommended to use the "compile from sources" method if you want to use QuickChick. An alternative method is to install OCaml by other means and have it in the PATH, but this method is not supported by the Coq Platform team. We plan to add an OCaml compiler to the binary installers in the next release.

Installers

Binary installers are provided for the 2022.04 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 14
Loading