Coq/Ssreflect Set-up

[Back to the project page]

FCSL sources are checked to compile and tested with Coq versions 8.11 through 8.13 and Ssreflect/Mathcomp versions 1.11.0 and 1.12.0. They are not guaranteed to work seamlessly with different versions. Several recipes on how to build install the necessary software are provided below.

Installing Coq and Ssreflect using OPAM

To install Coq 8.11 and Ssreflect using OPAM, a package manager for OCaml, copy and paste the following comands into your terminal:

  opam repo add coq-released
  opam pin add coq-mathcomp-ssreflect 1.11.0

Installing Coq and Ssreflect natively

In order to install Coq and Ssreflect natively from source, you can download them from the following links. Follow the build instructions from each of the source packages.

Emacs and Proof General set-up

Emacs (or Aquamacs for macOS 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.11/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).
by case=>x H1 H2; apply: H1 (H2 x).

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-ecoop17 in the VM image).

[Back to the project page]

Last modified: Fri Feb 19 15:49:16 CET 2021