ssreflect LibraryThe easiest way to obtain a working Coq environment is to use the latest stable release of the Rocq Platform distribution. The Rocq projects provides detailed installation instructions for macOS, Windows, and Linux.
On Linux and macOS, the default installation of the Rocq Platform distribution is sufficient to work with Prosa, so no further steps are required.
On Windows, it is further recommended to download and install MSYS2 since some of Prosa’s scripts assume a Unix-like shell environment.
Once the Rocq Platform has been installed, Prosa can be directly installed with the opam package manager.
If you are unfamiliar with opam, please refer to the opam installation instructions to properly set up opam first (typically, it suffices to run opam init once).
Once you have a working opam installation, run:
opam repo add rocq-released https://rocq-prover.org/opam/released
opam update
opam install coq-prosa
The above commands should install the latest stable release of Prosa.
For further information, please also refer to the section on using opam to install Prosa in the project’s README file.
For new developments, it is typically more convenient to compile the latest version of Prosa from source.
First, clone the Prosa source repository:
git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git prosa
cd prosa
If you don’t yet have a suitable opam switch configured, run scripts/ mk-opam-switch.sh to set up a suitable environment with all of Prosa’s dependencies in place.
Given a working Rocq environment with dependencies installed, Prosa is easy to compile: simply run make -j all to compile the entire Prosa codebase.
make -j all
The Prosa project uses a continuous integration (CI) pipeline to ensure that the latest version always compiles cleanly.
Current CI status: 
For further details, please also consult the instructions provided in the Prosa README file.
In addition to the essential setup described above, the following tools also greatly help with proof development.
For users interested in a modern editor experience, we recommend the plugin for Rocq support in Microsoft Visual Studio Code.
Many Coq users prefer to use Emacs with the Proof General extension for proof development. Traditionally, it has been the most stable and mature choice. However, it is inherently tied to Emacs, which not all users appreciate to the same degree.
Follow the instructions for installing the Emacs Proof General extension via the MELPA package manager for Emacs. Please consult the excellent Proof General documentation for a tutorial on how to get started.
The Company-Coq extension for Proof General provides a more convenient IDE for writing Coq specifications and proofs. In addition to offering auto-completion and shortcut capabilities, Company-Coq overrides the symbols used by Emacs to exhibit a more visually appealing specification during development (e.g., with unicode symbols, proper subscripts, etc.).
For additional information and installation instructions, please refer to the Company-Coq webpage.
The Alectryon tool is a great way to obtain nicer HTML documentation with steppable proofs.
When trying to identify the assumptions required by a particular analysis, instead of manually searching the code, it is possible to automate the process by using a dependency graph generator such as dpdgraph. Using this tool, one can track the use of definitions, hypotheses and theorems without laborious manual effort.
For additional information and installation instructions, please refer to the dpdgraph webpage.