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

我已经在Linux(Ubuntu 17.04)中成功安装了Coq 8.6和CoqIDE。但是，我不知道将SSReflect和MathComp添加到此安装的过程。我检查过的所有引用文献似乎令我感到困惑。有人对此有一个简单明了的秘诀吗？我确实安装了opam。

最佳答案

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