Geek Answers Handbook

How to install SSReflect and MathComp on Linux?

I have successfully installed Coq 8.6 and CoqIDE on Linux (Ubuntu 17.04). However, I do not know how to do this to add SSReflect and MathComp to this installation. All the links that I checked seemed to me very confusing. Does anyone have a simple and simple recipe? I have opam installed.

+5
source share
2 answers

I'm on Ubuntu 16.04. Let's take a step back and start 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

Then you can switch from the old version of OCaml Ubuntu to a newer one. This step is optional and takes about 10 minutes.

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

Now 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 detect dependencies (including Coq), download and install what we set!

+4
source

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

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

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

+1
source

More articles:


All Articles