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)，下载并安装我们要求的内容!