Coq/Ssreflect Set-up

[Back to the project page]

Installing Coq and Ssreflect natively

FCSL sources are checked to compile and tested with Coq version 8.5pl1 and Ssreflect/Mathcomp version 1.6. They are 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.


Emacs and Proof General set-up

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 .emacs file:
    (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 .v file will automatically trigger the Proof General mode.


Checking your set-up

To check that your setup is correct, create in Emacs a file with an extension .v and the following text in it:

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.
After that, set the text caret to the very last position of the file and press 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 defined
which would mean that your set-up is correct and you are ready for hacking in Coq/Ssreflect.


Building FCSL

To build FCSL, run make clean; make from the folder, to which the sources were unpacked (~/fcsl-oopsla16 in the VM image).

[Back to the project page]


Last modified: Sat Jun 11 16:05:02 BST 2016