Search code examples
linuxcoqssreflect

How to install SSReflect and MathComp in Linux?

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.

Solution

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