The easiest way to obtain a working Coq environment is to use the latest stable release of the Coq Platform distribution. The Coq Platform project provides detailed instructions for macOS, Windows, and Linux. Please follow the instructions appropriate for your system.
On Linux and macOS, the default installation of the Coq 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 Coq Platform has been installed, Prosa can be directly installed with the opam package manager.
opam install coq-prosa
However, for new development, it is typically better to compile Prosa from source.
Given a working Coq environment with ssreflect available, Prosa is easy to compile. Simply:
Makefile with ./create_makefile.sh andmake -j to compile everything.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 Coq 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 stepp-able proofs. For example, check out the current Prosa spec with stepp-able 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.