How to install SSReflect and MathComp in Linux?

Question

I have successfully installed Coq 8.6 and CoqIDE in Linux (Ubuntu 17.04). However, I don't know to proceed in order to add SSReflect and MathComp to this installation. All the references that I have checked seemed to be very confusing to me. Does anyone have a straight and simple recipe to that? I do have opam installed.

Answer 1

I'm on Ubuntu 16.04. Let's take a step back and begin by installing OPAM:

$ sudo apt update && sudo apt install opam
$ opam --version
1.2.2
$ opam init     # agree to modify your dot-files
$ eval `opam config env`
$ ocamlc -version
4.02.3

Next, you may want to switch from Ubuntu's pretty old OCaml version to a more recent one. This step is optional and it takes around 10 min.

$ opam switch 4.04.1
$ eval `opam config env`
$ ocamlc -version
4.04.1

Now, let's add the following repository to be able to install math-comp:

$ opam repo add coq-released https://coq.inria.fr/opam/released

And, finally, install ssreflect:

$ opam install coq-mathcomp-ssreflect

OPAM will figure out the dependencies (including Coq), download and install what we have asked!

Answer 2

For sake of completeness, an alternative way is by using the Nix package manager (instead of OPAM). After installing it (curl https://nixos.org/nix/install | sh), you can launch a CoqIDE with Math-Comp available with the following command:

nix-shell -p coqPackages_8_6.mathcomp --run coqide

Then you can just start your file with From mathcomp Require Import ssreflect.