Overview

The Rocq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.

The Rocq Platform is a distribution of Rocq together with a selection of libraries and plugins. The main goal of the Rocq Platform is to provide a distribution for developing and teaching with Rocq that is:

• operating system independent
• dependable
• easy to install
• comprehensive

See the Charter for more on the Platform concept, and CEP 52 for more on how the Platform is related to the Rocq release cycle.

The Rocq Platform is based on the OCaml package manager opam and provides a set of scripts to compile and/or install opam, Rocq and the platform contents on macOS, Windows and many Linux distributions in a reliable way with consistent results. In addition pre-compiled binary packages or installers are provided for macOS and Windows (Docker is in preparation). Note that snap for Linux is no longer supported (the maintenance effort was too high).

The Rocq Platform supports installing several versions of Coq - also in parallel, e.g., for porting developments from one version of Rocq to another. For the previous release version of Rocq, Rocq Platform provides extended and updated package picks which are as much as possible compatible to the pick of the latest release version of Rocq. For this reason for some Rocq versions several different package picks are provided.

The table below contains links to the README files for the supported versions of Rocq and libraries. Each README file contains a list of included packages with detailed information for each package.

• Rocq 9.0.1 (released Aug 2025) with the first package pick from Aug 2025
• Coq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025
• Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024
• Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023
• Coq 8.18.0 (released Sep 2023) with a package pick based on mathcomp 2.1
• Coq 8.17.1 (released Jun 2023) with the first package pick from Aug 2023
• Coq 8.16.1 (released Nov 2022) with an updated package pick from Aug 2023
• Coq 8.16.1 (released Nov 2022) with the first package pick from Sep 2022
• Coq 8.15.2 (released Jun 2022) with an updated package pick from Sep 2022
• Coq 8.15.2 (released Jun 2022) with the first package pick from Apr 2022
• Coq 8.14.1 (released Nov 2021) with an updated package pick from Apr 2022
• Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022
• Coq 8.13.2 (released Apr 2021) with an updated package pick from Jan 2022
• Coq 8.13.2 (released Apr 2021) with an updated package pick from Sep 2021
• Coq 8.13.2 (released Apr 2021) with original package pick from Feb 2021
• Coq 8.12.2 (released Dec 2020)
• Coq Developer (latest developer branch)

If you have questions on the Rocq Platform, please contact us on zulip chat Rocq-Platform & users

Installation

The Rocq platform is the recommended way to install Rocq for both beginners and experts. Beginners are encouraged to use one of the binary installers. Experienced users are advised to run the scripts provided by the Rocq platform to install from sources as this will allow them to install additional packages with opam. Please refer to the ReadMe file for your operating system, which contains information on both methods respectively.

• macOS: see README_macOS.
• Windows: see README_Windows
• Linux: see README_Linux.

Additional information

<details><summary><font size="+1">Licenses</font></summary>

The Rocq Platform setup scripts and the selection of package recipes and patches are licensed Creative Commons CC0. This license does not apply to the packages installed by the Rocq Platform. The README files linked above provide license information for each package. This information is also available as .CSV files here doc. Please note that the license information is obtained from opam. The Rocq Platform team does no double check this information.

</details> <details><summary><font size="+1">Release notes / changelog</font></summary>

Changes in 2025.08.0

• added new pick 9.0~2025.08

Changes in 2025.01.0

• added new pick 8.20~2025.01
• added package vscoq-language-server to picks 8.20~2025.01 and 8.19~2024.10
• Windows: link DLLs into opam switch bin folder, so that binaries can be called from outside cygwin
  • this enables the use of a Windows "from sources" installation outside of cygwin without setting PATH
  • added script windows/link_shared_libraries.sh to hard link cygwin provided DLLs into the opam switch bin folder
  • call this script automatically during cygwin setup

Changes in 2024.10.1

This is a "source only" bugfix release which addresses changes in the opam file format in opam 2.3.0. The installers and package pick lists are unmodified from the previous release.

Changes in 2024.10.0

• added new pick 8.19~2024.10
• the MacOS installers for Apple silicon (ARM) are now fully supported (no longer experimental)
• on Windows enabled long path support by
  • using a manifest where this is enabled during build of all executables
  • checking in the script if the registry key is set
  • Not that this is only required during build - if using an installer the provided binaries still have this enabled in the manifest, but the user is not asked to enable it in the registry
• on Windows set the stack size of `ocamlc`` to 64MB (essentially by patching the binary) - this allows to build fiat-crypto
  • note that coqc is not pacthed in this way - it can be done if needed. See the folder windows/set_stack_size and the script shell_scripts/install_ocaml_stacksize.sh
  • also note that on Windows any stack size can be set in case this should be required (MacOS has a hard limit of 64MB, though (as of macOS Sonoma) so try to avoid this to stay portable)
• on Windows re-enables coq-fiat-crypto
  • on Windows no packages are excluded any more except for coq-hammer which heavily uses Unix style fork
• support for snap has been removed
  • there is currently no known method to build snaps in case the build process requires more than 2GB of RAM
  • the overall maintenance effort for snap was very high
  • we are looking for a replacement - suggestions welcome

Changes in 2023.11.0

• when using the build from sources script on Windows the root folders changed to shorten the path length (e.g. coq-serapi had build issues cause by long path names)
  • the opam path is now <cygroot>/opam instead of <cygroot>/home/<user>/.opam
  • the platform path is now <cygroot>/platform instead of <cygroot>/home/<user>/platform
  • the (longest) recommended cygwin root path is now C:\bin\cygwin_coq_platform or C:\bin\cygw32_coq_platform
• added new pick 8.18~2023.11
• added new pick 8.18~mc2
• the doc folder now contains an opam package dependency graph for all picks, e.g. [doc/DependencyGraph~8.18~2023.11.pdf]
• coq-ott has been added back on Windows
• coq-fiat-crypto is still removed on Windows, since version 0.0.24 results in stack overflows - there is no good work around for this - we recommend to use the prior pick 8.16~2022.09

ATTENTION:

Please see the Pick Readme 8.18~2023.11 and Pick Readme 8.18~mc2 for details on the package list.

Changes in 2023.03.0

• Added new picks 8.17~2023.08 and 8.16~2023.08
• coq-ott has been removed on Windows, since version 0.33 has issues there - if you need coq-ott we recommend to install version 0.32 via opam on Windows
• coq-fiat-crypto has been removed on Windows, since version 0.0.20 results in a stack overflows - there is no good work around for this - we recommend to use the previous pick 8.16~2022.09

Please see the Pick Readme for details on the package list.

Changes in 2022.09.1

• Changed picks 8.16~2022.09 and 8.15~2022.09 from beta to release
• Updated pick 8.16~2022.09 to Coq version 8.16.1
  • Coq and CoqIDE 8.16.1 contain various substantial fixes over 8.16.0

Please see the Pick Readme for details on the final package list.

Changes in 2022.09.0

• added a "coq-shell" on macOS, Windows and Snap installers
  • the coq-shell starts a shell or CMD window with environment set to use the installed Coq
  • on macOS, the DMG installer contains a coq-shell.command file one can copy e.g. to the desktop - see macOS for details
  • on Windows a coq-shell.bat file is installed and added to the start menu - see Windows
  • on Linux/Snap there are two methods to start a Coq shell - see Linux
• added a coq-env.sh file on macOS and Linux/Snap to be used with eval - see macOS and Linux for details
• on macOS the installer should now work for macOS down to version 10.13 - this is not much tested, though - bug reports are welcome
• many small usability improvements and bug fixes
• beta package pick for Coq 8.16.0 with