coq - 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!