11

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.

Zimm i48
  • 2,901
  • 17
  • 26
Marcus
  • 437
  • 2
  • 11
  • Does `opam install coq-mathcomp-ssreflect` not work? – Anton Trunov May 13 '17 at 16:13
  • No. I get the error message "No package named coq-mathcomp-ssreflect found". By the way, do I have to download these packages by myself? Where do I find them? – Marcus May 13 '17 at 19:02
  • If I try separately, opam says that coq is already installed and that mathcomp and ssreflect were not found. – Marcus May 13 '17 at 19:04

2 Answers2

8

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!

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • 1
    That worked perfectly, thank you so much! Now I can see that everything is installed with the correct version. However, I still get error messages when I write "Require Import ssreflect" in my scripts: "unable to locate library ssreflect". Something is still missing, any idea of what that could be? – Marcus May 13 '17 at 21:56
  • 2
    It's under mathcomp namespace: e.g. `Require Import mathcomp.ssreflect.all_ssreflect.` or `From mathcomp Require Import ssreflect.all_ssreflect.` or (if we want to import only some basic stuff) `From mathcomp.ssreflect Require Import ssreflect ssrnat ssrbool eqtype.` – Anton Trunov May 13 '17 at 22:09
  • Thanks, but I still get the message "Error: Cannot find a physical path bound to logical path matching suffix <> and prefix mathcomp.ssreflect" in the third case, and similar messages for the other two. – Marcus May 13 '17 at 22:56
  • 2
    It should work with CoqIDE if you have installed it via OPAM: `opam install coqide`. You might also need to install some additional libraries, in my case `sudo apt install libgtksourceview2.0` was enough. I just tried it and it worked, but be sure to run CoqIDE from OPAM, not Ubuntu's (old) version. I'm not a CoqIDE user, so I don't know how to tweak the preferences to make it work with the `apt`-installed version. – Anton Trunov May 13 '17 at 23:46
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.

Zimm i48
  • 2,901
  • 17
  • 26
  • 1
    Wow, so simple! Btw, after installing Nix I had to run `. $HOME/.nix-profile/etc/profile.d/nix.sh` to be able to execute `nix-shell`. – Anton Trunov May 16 '17 at 10:21
  • It seems that Nix installed Coq 8.4pl6 in this case, so `From ...` doesn't work. Is there a way to install a more recent version? (Normally, I'm on macOS if that matters). `nix-shell` version is 1.11.9. – Anton Trunov May 16 '17 at 10:53
  • @AntonTrunov Sorry I fixed the command to make sure Coq 8.6 is the installed version. – Zimm i48 May 16 '17 at 11:15
  • Thanks! Everything just works! I can invoke coqtop like so: `nix-shell -p coqPackages_8_6.mathcomp --run coqtop`. Is there a preferred way of integrating the Nix-installed Coq version with ProofGeneral? Or it's just the standard modify-the-`coq-prog-name`-variable approach? – Anton Trunov May 16 '17 at 11:52
  • 1
    @AntonTrunov Since you obviously already have Proof-General installed, I would just do `nix-shell -p coqPackages_8_6.mathcomp --run emacs` Note that if you drop the `--run` option, you get into a shell with extended `$PATH` and `$COQPATH` and this can be useful to invoke `coq_makefile` and `make`. – Zimm i48 May 16 '17 at 11:56