In order to follow the course, execute the examples and complete the exercises, you are expected to have the Coq Proof Assistant with Ssreflect extension installed at your machine. This page contains some general instructions on the installation and set-up.
There is also an option to use a virtual machine image instead of installing all the software natively (the instruction on obtaining the VM are below).
For further information or assistance on set-up, please, contact .
The sources of the course files are checked to compile and tested with Coq version 8.6 and Ssreflect/Mathematical Components version 1.6.1. It is not guaranteed that the same examples will work seamlessly with different versions. Therefore, several recipes on how to build install the necessary software are provided below.
INSTALLfile from the archive with sources for the full list of requirements on configuration and installation). Once compiled, the following environment variables should be set (e.g., in
~/.profileconfiguration files) to build Ssreflect (with the respective paths chosen during the Coq's installation):
export COQBIN="/usr/local/bin/" export COQ_MK="/usr/local/bin/coq_makefile"It is also recommended to keep sources of Ssreflect and Mathematical Components easily accessible as reading them might be helpful when working with libraries (for instance, in the folder
~/misc/mathcomp-1.6/mathcomp). Upon installing Ssreflect via
make install, the following environment variable should be also set up:
export SSRCOQ_LIB="/usr/local/lib/coq/user-contrib/mathcomp/ssreflect"Alternatively, instead of running
make install, one can set up the environment variable
SSRCOQ_LIBto point to the folder
ssreflect-location/theories, which contains all Ssreflect modules compiled (and
ssreflect-locationdenotes the location of the directory where Ssreflect has been unpacked to).
Emacs (or Aquamacs for Mac OS X users) text editor provides a convenient environment for Coq development, thanks to the Proof General mode.
On Unix-like systems, clone Proof General from
its GitHub repository, following the instructions below. Upon
downloading and unpacking, add the following lines into the
.emacs configuration file located in the home directory
~/) in Unix and in
C:\ root in Windows
(possibly replacing the
~/misc/ part with the path where
Proof General and Ssreflect sources were unpacked/cloned).
;; Proof General support (load-file "~/misc/PG/generic/proof-site.el") ;; Ssreflect support (load-file "~/misc/mathcomp-1.6/mathcomp/ssreflect/pg-ssr.el")Linux users, more used to the Windows-style Copy/Paste/Undo keystrokes can also find it convenient to enable the Cua mode in Emacs, which can be done by adding the following lines into the
(cua-mode t) (setq cua-auto-tabify-rectangles nil) (transient-mark-mode 1) (setq cua-keep-region-after-copy t)Every Coq file has the extension
.v. Opening any
.vfile will automatically trigger the Proof General mode.
WARNING: The virtual machine image hasn't yet been updated for Coq 8.5 and Ssreflect 1.6 and contains an older version of the course.
If compiling and installing Coq and Ssreflect from scratch looks
like too much hassle, there is also a possibility to use a virtual
machine image with all necessary libraries preinstalled and Emacs set
up to work with Ssreflect. The image requires Oracle VirtualBox to be
used; it is about 1.8 GB size and can be obtained by the following link. It
runs Ubuntu 14.04 and automatically logs in when started with the user
coquser (use the password
it is required). The folder
~/misc contains the sources
of Ssreflect and Proof General.
To check that your setup is correct, create in Emacs a file with an extension
.v and the
following text in it:
From mathcomp.ssreflect Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module Test. Variable A : Type. Theorem counterexample P : (exists x : A, ~P x) -> ~(forall x, P x). Proof. by case=>x H1 H2; apply: H1 (H2 x). Qed. Print counterexample. End Test.
Ctrl-c Ctrl-Enter. This will activate the Proof General interactive checking mode and will interpret the file. As the result, the buffer
*goals*should display the following message:
Module Test is definedwhich would mean that your set-up is correct and you are ready for hacking in Coq/Ssreflect. [Back to the course page]