FCSL sources are checked to compile and tested with Coq version 8.7.0 and Ssreflect/Mathcomp version 1.6.4. They are not guaranteed to work seamlessly with different versions. Several recipes on how to build install the necessary software are provided below.
To install Coq 8.7 and Ssreflect using OPAM, a package manager for OCaml, copy and paste the following comands into your terminal:
opam repo add coq-released https://coq.inria.fr/opam/released opam pin add coq-mathcomp-ssreflect 1.6.4
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 (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.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.
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.
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.
To build FCSL, run
make clean; make from the folder, to which the
sources were unpacked (
~/fcsl-ecoop17 in the VM image).