Coq/Ssreflect Set-up

Installing Coq and Ssreflect natively

FCSL sources are checked to compile and tested with Coq version 8.4 and Ssreflect version 1.4. 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.

Linux, Cygwin and Mac OS X

Linux and Mac OS X users are recommended to compile Coq 8.4 and Ssreflect 1.4 from sources, which would take around two hours (getting Coq 8.4 using a system-specific package manager, such as aptitude or MacPorts is another option, although the Coq version acquired this way is not guaranteed to work with Ssreflect 1.4).

Coq 8.4 sources
Ssreflect 1.4 sources

In order to be compiled, Coq 8.4 requires Objective Caml version 3.11.2 or later, Camlp5, GNU Make version 3.81 or later (see the INSTALL file 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 ~/.bashrc or ~/.profile configuration 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"

After compiling Ssreflect, the file bin/ssrcoq should be created in the ssreflect-1.4 folder. It should be then manually copied to the same folder where the Coq binaries are located (e.g., /usr/local/bin in the default case of Unix-like systems). It is also recommended to keep Ssreflect's sources easily accessible as reading them might be helpful when working with libraries (see the files in the folder ssreflect-1.4/theories/). Upon installing Ssreflect via make install, the following environment variable should be also set up:

    export SSRCOQ_LIB="/usr/local/lib/coq/user-contrib/Ssreflect/"

Alternatively, instead of running make install, one can set up the environment variable SSRCOQ_LIB to point to the folder ssreflect-location/theories, which contains all Ssreflect modules compiled (and ssreflect-location denotes the location of the directory where Ssreflect has been unpacked to).

Windows

Windows users are encouraged to use Pierre-Yves Strub's installer with the Coq bundle (also available from http://pierre-yves.strub.nu), which already contains all the necessary components including Coq v8.4pl2, Ssreflect v1.4 and Emacs with Proof General installed.

WARNING: The FCSL sources have not been tested properly on a Windows configuration (although they should work in principle), so any feedback is welcome. In particular, some troubles might be experienced when compiling libraries via make-scripts.

Emacs and Proof General set-up

GNU Emacs (or Aquamacs for Mac OS X users) text editor provides a convenient environment for Coq development, thanks to the Proof General mode.

On Windows, installing Coq bundle guarantees that Emacs is properly configured, so (presumably) no additional actions is required.

On Unix-like systems, after downloading and installing Emacs, download and install Proof General, 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).

    ;; Proof General support
    (load-file "~/misc/ProofGeneral-4.2/generic/proof-site.el") 

    ;; Ssreflect support 
    (load-file "~/misc/ssreflect-1.4/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. Once the mode is launched, in the menu Proof-General, choose the item:

    Advanced -> Customize -> Coq -> Coq Prog Name

and change the value of the variable to

    ssreflect-location/bin/ssrcoq

    ssreflect-location\bin\ssrcoq

for Windows/Cygwin users, where ssreflect-location is the location of your Ssreflect directory with compiled binaries (or, alternatively, a parent catalogue of the bin folder containing Coq and Ssreflect's binaries, where ssrcoq has been previously copied, as it was suggested).

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

[Back to the artifact page]

Last modified: Wed Apr 8 14:32:46 CEST 2015