All Releases

Coq Platform 2025.01.0

This page describes the Coq Platform version 2025.01.0, released on Feb 6th, 2025. Go here for a list of all Coq, Rocq and Platform releases. Go here for a list of all Rocq/Coq Platform releases.

This is the first platform supporting Coq 8.20.

Github release

Reference Manual

OCaml API

Stdlib Theories

Note: the MacOS intel installer is work in progress, and the arm installer is not yet signed. The unsigned Mac installers are hard to use, especially when a signed version has been installed before. In case you need this urgently (e.g. for a lecture) we can supply a script which signs it locally after installation (such a signature is only valid on the machine it was made on as far as we can tell). The previous MacOS (arm) installer for Coq 8.19.2 is signed.

Note: snap is no longer supported (we are working on a replacement)

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

  • The language server for the VsCoq plugin is now included
    • VSCoq can be connected directly to the vscoq-language-server supplied by a binary installer
    • On Windows it is now also possible to connect VSCoq to a language server built from sources. This is achieved by hard linking all cygwin supplied MinGW DLLs into the folders of the executables which use them. This is done via link_shared_libraries.sh which is called automatically by coq_platform_make.sh. In case you install additional binaries which need addtional DLLs are called via VSCoq, e.g. solvers like gappa or z3, you might have to run this script again, but this should be rare since common DLLs are already linked.

Additional packages will be added in an intermediate release.

Included Versions of Coq

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.19.2 with the first package collection from October 2024
  • Coq 8.18.0 with the first package collection from November 2023
  • Coq 8.17.1 with the first package collection from August 2023
  • Coq 8.16.1 with an updated package collection from August 2023 which is as much as possible compatible with the first 8.17.1 package collection
  • Coq 8.16.1 with the first package collection from September 2022
  • Coq 8.15.2 with an updated package collection from September 2022 which is as much as possible compatible as possible with the first 8.16.1 package collection
  • Coq 8.15.2 with the first package collection from April 2022
  • Coq 8.14.1 with an updated package collection from April 2022 which is as much as possible compatible as possible with the first 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 which is as much as possible 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

Notes

  • Notes on the macOS Intel installer: There are some issues with the Intel installer - we recommend to build from sources if you have an Intel Mac.

  • 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 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 and Windows. 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 a future release.

  • Note on SerAPI: The SerAPI executables like sertop require that either the COQLIB environment variable is exported or a --coqlib=${coqc -where} or similar option is given. Other Coq tools like coqc determine the Coq library path from the binary location, but sertop does not (yet).

  • Note on coq_makefile on Windows: The Windows installers don't supply make because make is quite limited without a posix shell. An addon is supplied which contains a Windows native gnumake and a patched template file for coq_makefile which allows to use coq_makefile and gnumake with CMD as shell.