CoqIDE (8.5pl1, OS X) bundled with ssreflect.

CoqIDE bundled with ssreflect.md

The CoqIDE bundle (8.5pl1, OS X) with ssreflect preinstalled.

coqide-8.5pl1-ssreflect.7z - around 75 MB. (Smaller than the standard CoqIDE bundle!)

A great big caveat: the app bundle is no longer codesigned. If you wish to keep CoqIDE*.app codesigned, install a clean CoqIDE*.app, and replace the Resource/bin and Resources/lib/coq/user-contrib with the ones here.

Sanity testing the installation

I’m sure the reference manual is out of date - instead, I use test cases from the mathcomp/ssrtest folder. Note the new, extended library import paths. Try this, for example:

(* From mathcomp/ssrtest/occarrow.v. *)
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import eqtype ssrnat.

Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n.
move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-.
by move: E => {3}->.
Qed.

Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m).
by move=> n m; constructor=> [|{2}->].
Qed.

You could have done this yourself:

• Get coq and ssreflect. I installed OPAM via Homebrew, added Coq’s OPAM archive to OPAM (instructions at https://github.com/coq/opam-coq-archive), and then ran “opam install coq coq-mathcomp-ssreflect”.

• Separately, get the CoqIDE bundle. Coq’s website is useful.

• The CoqIDE bundle was then modified: from OPAM’s installation, lib/coq/user-contrib/mathcomp was copied in. Similarly, bin/coq* and bin/gallina were replaced.

• Remove the code signature from the coqide executable.

Notice that the files OPAM has built are no longer fully binary-compatible with the CoqIDE bundle: OPAM will generally use a newer version of the OCaml compiler.