Recommended binary installers
Note: Snap is no longer supported (a replacement is in progress).
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
None.
Changelog
- feat: new version of package pick 9.1 (be95c16)
- fix: sanitize invalid unicode character in coq-gappa file paths on Windows (9.1) (8572215)
- doc: bump version in README files (1df857f)
- feat: prepare release 9.1; change switch name CP to RP; update packages (a659475)
- fix: solved ci bug on META file (63a9d16)
- feat: bump version of coq-deriving to 0.2.3 (af75eb8)
- feat: bump version of rocq-iris, rocq-iris-heap-lang to 4.5.0 and rocq-stdpp to 1.13.0 (a3b1f9c)
- fix: add archive ocaml repos fot 8.12 / 8.13 on Ubuntu (e5c5446)
- feat: bump version of rocq-elpi to 3.4.0 and elpi to 3.7.1 (dd43de4)
- fix: resolve checksum error about coq-simple-io (6b722e8)
- rollback version for elpi and rocq-elpi (34ec70f)
- version unimath 20260603 (483a5c8)
- bump version mtac2 to 9.1 (4f0d0fc)
- compcert and vst available in package_pick file (9ca6ca1)
Included Versions of Coq
Recommended Rocq version
- Rocq 9.1.0 with the first package collection from January 2026
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).
- Rocq 9.0.1 with the first package collection from August 2025
- 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 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 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 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
Binary installers are provided for Rocq 9.1.0. The installer for macOS (Apple Silicon) and Windows can be downloaded above.