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.

Using our VM Image (Quick Start)

The easiest way to compile Prosa is to use our ready-made Ubuntu 16.04 VM image, which comes with all necessary packages pre-installed. This VM also includes Proof General, an extension for Emacs for editing Coq proofs in an interactive manner.

The VM image is available here: Ubuntu 16.04 VM image.

After decompressing the gzip file, you should obtain a file called prosa.qcow, a disk image that can be imported into VirtualBox. For further instructions on how to boot the image, please see the VM booting guide.

Before initializing the VM, make sure it has at least 2GB of allocated memory. If you need root privileges, use prosa as both login and password.

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

$ git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
$ cd ~/.emacs.d/lisp/PG
$ make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

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

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
;;
;; 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 OCaml and a few other required packages.

$ sudo apt-get install ocaml ocaml-native-compiler camlp5 \
                           liblablgtk2-ocaml-dev libgtk2.0-dev \
                           liblablgtksourceview2-ocaml-dev 

2) Download the Coq source code from the project website and extract the files. Coq version 8.5pl2, which is the latest version at the time of writing, is available here.

3) Go to the extracted Coq directory and compile the proof assistant.

$ cd path/to/extracted/coq
$ ./configure
$ make -j 4
$ sudo make install

The configure step should inform you about any missing packages (e.g., ocaml, camlp5). Note that the package liblablgtk2-ocaml is only required if you decide to use the Coq IDE.

After installing Coq, the aliases to the Coq utilities (e.g., coqc, coqchk, etc.) should be accessible via your terminal.

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

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

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

$ cd path/to/Prosa
$ 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. If you prefer not to install additional third-party software, we suggest using the Virtual Box VM image.

1) Download and install Coq v8.5pl1 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 Mathematical Components 1.6 (compiled with Coq v8.5pl1) using either the win32 installer or the win64 installer, depending on your Windows version. During the setup, keep the installation directory C:/coq.

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

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

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

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

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

8) 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
$ make -j 4

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