如何在Linux中安装SSReflect和MathComp？

Question

我已经在Linux (Ubuntu17.04)中成功地安装了Coq8.6和CoqIDE。但是，我不知道如何将SSReflect和MathComp添加到这个安装中。我查过的所有参考资料似乎都让我很困惑。有没有人有一个直接而简单的食谱？我确实安装了opam。

Answer 1

我在Ubuntu 16.04。让我们后退一步，从安装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

接下来，您可能希望从Ubuntu相当老的OCaml版本切换到最近的版本。这一步是可选的，大约需要10分钟。

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

现在，让我们添加以下存储库，以便能够安装math：

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

最后，安装ssreflect：

$ opam install coq-mathcomp-ssreflect

OPAM将找出依赖项(包括Coq)，下载并安装我们所要求的！

Answer 2

为了完整起见，另一种方法是使用Nix软件包管理器 (而不是OPAM)。安装它(curl https://nixos.org/nix/install | sh)之后，您可以使用Math启动一个可用的CoqIDE，命令如下：

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

然后您可以使用From mathcomp Require Import ssreflect.启动您的文件。