Setup Instructions

This guide provides simple step-by-step instructions for setting up a Coq environment that is suitable for working on Prosa.

Regardless of the installation method that you use, make sure you use the version of Coq matching the current Prosa release.

Setting Up Coq for Prosa on Mac OS X

On Mac OS X, we recommend to use the Homebrew package manager for installing Coq, and the Emacs.app GUI application with the Proof General extension as the frontend.

1) Install the Coq package with the Homebrew package manager:

$ brew install coq

After installing Coq, the aliases to the Coq utilities (e.g., coqc, coqchk, etc.) should be accessible via your terminal (i.e., /usr/local/bin should be in your shell’s $PATH).

2) Download and extract the latest release (version 1.6 at the time of writing) of the Mathematical Components library from the Mathematical Components project homepage.

3) Compile and install the ssreflect library, which is a part of the Mathematical Components library:

$ cd path/to/extracted/library
$ cd mathcomp/ssreflect
$ make -j 4
$ make install

After following these steps, the ssreflect library can be readily imported in Coq source files, so you should be able to compile Prosa.

4) Go to your checkout of Prosa and compile the project.

$ cd path/to/Prosa
$ ./create_makefile.sh
$ make -j 4

Installing Proof General (Optional)

We recommend to use Emacs.app with the Proof General extension for proof development. Alternatively, it is also possible to other Coq IDEs, but in our experience Proof General is the most stable and mature choice.

1) Get Emacs.app from https://emacsformacosx.com and install the application by dragging the icon into the Applications folder.

2) Follow the instructions for installing the Emacs Proof General extension via the MELPA package manager for Emacs.

3) Add the following lines to your ~/.emacs file:

;; Make sure we can find coqtop
(setq exec-path (append exec-path '("/usr/local/bin")))

At this point, you should be able to step through any Prosa file with the help of the Proof General environment in Emacs.app. Please consult the excellent Proof General documentation for a tutorial on how to get started.

Setting Up Coq for Prosa on Ubuntu Linux

Since the latest Coq versions are usually not available in the stable releases of Ubuntu, we provide instructions for compiling recent versions of Coq from source. Although we have tested Prosa in Ubuntu only, the same instructions may apply to other distributions.

1) Install the opam package manager:

$ sudo apt-get install opam

You migth also need to enable the “universe” repository, which can be done with the following command:

sudo add-apt-repository universe

2) Once opam is installed, it must be initialized before first usage:

$ opam init
$ eval $(opam env)

3) Install the Coq 8.10.2 package with the opam package manager. Note that installing Coq using opam will build it from sources, which will take several minutes to complete:

opam pin add coq 8.10.2

4) Compile and install the ssreflect 1.9.0 library, which is a part of the Mathematical Components library:

$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam pin add coq-mathcomp-ssreflect 1.9.0

After following these steps, the ssreflect library can be readily imported in Coq source files, so you should be able to compile Prosa.

5) Go to your checkout of Prosa and compile the project.

$ cd path/to/Prosa
$ ./create_makefile.sh
$ make -j 4

Installing Proof General (Optional)

Use the package manager to install Proof General. Emacs will also be automatically downloaded if it is not already available.

$ sudo apt-get install proofgeneral

After the installation, a link to Proof General will be available in the Applications/Programming section of the Ubuntu Menu.

Setting Up Coq for Prosa on Microsoft Windows

Here we describe how to compile Prosa on Windows. Since the Prosa compilation requires a Makefile, we use make via Bash shell from the MSYS2 project. Note, however, that this method is a workaround and does not run as smoothly as on Linux or Mac.

1) Download and install Coq v8.10.2 using either the win32 installer or the win64 installer, depending on your Windows version. Just follow the setup and keep the default installation directory C:/coq.

2) Download and install MSYS2 from the project webpage. Choose the link that corresponds to your version of Windows (i686 for 32bits or x86_64 for 64 bits).

3) On Windows, open the file C:\msysXX\home\YOUR-USER\.bashrc with some editor and add the following line. (Note that XX stands for 32 or 64.)

export PATH=$PATH:/c/coq/bin

This adds the Coq bin/ directory to the PATH variable used by the MSYS2 shell.

4) Now open All Programs > MSYS2 XXbit > MSYS2 in the Windows Start Menu.

5) In the MSYS2 Shell, use the package manager to install make:

$ pacman -S make

At this point, you should be able to run both coqc and make in the MSYS2 shell.

Figure: MSYS2 shell screenshot
Figure: MSYS2 shell screenshot

6) Also in the MSYS2 Shell, use the package manager to install python3 and patch:

$ pacman -S python3
$ pacman -S patch

These packages are needed to generate the makefile for the project.

7) Download and extract the Mathematical Components library 1.8 from the Mathematical Components project homepage.

8) Compile and install the ssreflect library, which is a part of the Mathematical Components library:

$ cd path/to/extracted/library
$ cd mathcomp/ssreflect
$ make -j 4
$ make install

9) Download and install Git using the Windows installer. During the installation, you should choose the default options.

10) Still in the MSYS2 Shell, clone the Prosa repository using Git and compile the project. (Note that Windows directories can be accessed normally by MSYS2. For example, you can use ls c/Users/YOUR-USER/Desktop to list files.)

$ cd path/to/Prosa
$ ./create_makefile.sh
$ make -j 4

11) Now you can alternate between editing the Prosa files with Coq IDE (on Windows) and compiling the code using the Makefile (within MSYS2 Shell).

Additional Tools

In addition to the essential setup described above, the following tools also greatly help with proof development.

Company-Coq

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.).

Figure: Company-Coq screenshot
Figure: Company-Coq screenshot

For additional information and installation instructions, please refer to the Company-Coq webpage.

dpdgraph

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.