Coq/Ssreflect Set-up

[Back to the project page]

FCSL sources are tested with Coq versions 8.14 through 8.16, Ssreflect/Mathcomp versions 1.13 through 1.15 and FCSL-PCM version 1.6. They are not guaranteed to work seamlessly with different versions. Several recipes on how to install the necessary software are provided below.

Installing/updating dependencies using OPAM

To install Coq, Ssreflect and FCSL-PCM using OPAM, a package manager for OCaml, first register the Coq repository with your OPAM by running the following command in terminal: 

  opam repo add coq-released https://coq.inria.fr/opam/released
After this, you can install the dependencies by running this command from the root source folder of FCSL: 
  opam install . --deps-only
If you're not doing a fresh installation (i.e., you have previous versions of the dependencies installed and require updating), or would like to install the libraries manually, this can be achieved by running: 
  opam update
  opam pin add coq-mathcomp-ssreflect 1.15.0
  opam pin add coq-fcsl-pcm 1.6.0

Installing dependencies natively

In order to install Coq, Ssreflect and FCSL-PCM 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.15/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 a file with an extension .v and the following text in it: 

From Coq Require Import ssreflect.
From mathcomp Require Import seq.
From fcsl Require Import seqperm.
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.

Example permute : perm [::1;2;3] [:: 2;1;3].
Proof.
by apply/permutation_swap/pperm_refl.
Qed.

Print permute.

End Test.
After that, set the text caret to the very last position of the file and press Ctrl-c Ctrl-Enter (Alt-End if you're using VsCoq). 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.

[Back to the project page]

Last modified: Fri Sep 23 16:06:31 CET 2022