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