Sunday, 12 April 2026 @ 09:17 UTC ~2 12,244 130,117

Coq

The Coq Team · Coq.CoqPlatform

Coq is a formal proof management system.

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 compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

winget install --id Coq.CoqPlatform --exact --source winget

Latest 2025.08.2

Release Notes

This is a minor release to bump version of rocq-hierarchy-builder to 1.10.2 The remainder of the release notes is a copy of the previous release. Recommended binary installers

  • Windows (64 bit) installer for Rocq 9.0
  • MacOS (arm) installer for Rocq 9.0 Note: snap is no longer supported (we are working on a replacement) General information See README for general information and installation of Rocq Platform. See Charter for the concept and goals of Rocq Platform. See CEP52 for the Rocq and Rocq Platform release cycle. See macOS, Linux and Windows for detailed installation and usage instructions. Major enhancements Included Versions of Coq Recommended Rocq version
  • Rocq 9.0.1 with the first package collection from August 2025 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.20.1 with the first package collection from January 2025
  • 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 Installers Binary installers are provided for Rocq 9.0. The Installer for MacOS Apple silicon and the Windows installer can be downloaded below.

Installer type: nullsoft

Architecture Scope Download SHA256
x64 — Download 4444BF4EF1039415F950CBAFB970E0064E4392354E5508634E3D89EB339213C2

Details

Homepage
https://github.com/coq/platform
License
CC0-1.0
Publisher
The Coq Team
Support
https://github.com/coq/platform/issues

Older versions (3)

2025.1.0
Architecture Scope Download SHA256
x64 — Download 1AE0222C094A90BF4F43E77B180F74404D6F6C85166E0A55823F99CDF14E0A7A
8.14.1
Architecture Scope Download SHA256
neutral — Download D45A07422C3CA017142515E8CEF7C995C280EBB107326398CCAE02AAC31D563E
8.13.2
Architecture Scope Download SHA256
neutral — Download 42913CF2BD80B33796B79F76F7A49CDA806A7966110647E39E15943DD78D06D1