linux - 如何在 Linux 中安装 SSReflect 和 MathComp？

Question

我已经在 Linux (Ubuntu 17.04) 中成功安装了 Coq 8.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-comp：

$ 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-Comp 的 CoqIDE：

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

然后你可以开始你的文件From mathcomp Require Import ssreflect.