Skip to content

2022.09.0 with Coq 8.16.0 and beta package collection

Pre-release
Pre-release
Compare
Choose a tag to compare
@MSoegtropIMC MSoegtropIMC released this 11 Oct 06:20
· 321 commits to main since this release
2022.09.0
7548f1f

Recommended binary installers

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.

See macOS, Linux and Windows for detailed installation and usage instructions.

Major enhancements

A beta package pick for Coq 8.16.0 is included with an updated and substantially extended package list.

These packages have been added to the "full" level in the 2022.09 pick:

  • coq-itauto.8.16.0
  • coq-mathcomp-algebra-tactics.1.0.0 (moved from "extended")
  • coq-mathcomp-word.1.1

These packages have been added to the "extended" level in the 2022.09 pick:

  • coq-metacoq.1.1+8.16
  • coq-fiat-crypto.0.0.15
  • coq-bedrock2.0.0.3
  • coq-bedrock2-compiler.0.0.3
  • coq-rupicola.0.0.5
  • coq-coqutil.0.0.2
  • coq-rewriter.0.0.6
  • coq-riscv.0.0.2

Things to have an eye on in the beta releases

This Coq Platform release contains a macOS/Snap/Windows installers for 8.16.0 with a beta package pick. If you try these beta installers, we would like you to have an eye on the following points:

  • With Coq 8.16.0, Coq uses Ocamlfind to find shared libraries. Ocamlfind has not been designed with installers and relocation in mind - that is, using software in a different place than it was compiled in. Some patching was done to Ocamlfind by the Coq Platform team to make the installers work. To test this, please have a look at all your favorite plugins.
  • There are two patches to CoqIDE included, which are not in the 8.16.0 release:

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.15.2 with an updated package collection which is as much as possible compatible with the new 8.16.0 beta package pick
  • Coq 8.15.2 with the first package collection from April 2022
  • Coq 8.14.1 with an updated package collection from April 2022 - this package pick is made to be as compatible as possible with the 8.15.2 package collection
  • Coq 8.14.1 with the first package collection from January 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.16.0 and 8.15.2 versions with the new (beta) package collection are available as installers for macOS and Windows and only the 8.16.0 version as a Snap package. Other versions can be installed using the Coq Platform scripts or the binary installers from previous Platform releases.

Notes

  • Notes on compiling from sources on Windows: If you compile from sources on Windows, please use main instead of the tag - the tag has build issues caused by changes in opam.

  • Notes on the macOS installer: 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. The installer is now designed to be compatible down to macOS 10.13, but this is not much tested. We appreciate bug reports for 10.X macOS versions, 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 is 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 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.

  • Note on Serapi: The SerAPI executables like sertop require a --coqlib=${coqc -where} or similar option. The `COQLIB environment variable is not used.

Installers

Binary installers are provided for the 2022.09~beta1 pick of Coq 8.16.0 for macOS, Windows and Linux (snap). The macOS and Windows installers can be downloaded below. The snap package will be available soon via snapcraft.

Assets 8
Loading