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

    为了完整起见,另一种方法是使用Nix包管理器 (而不是OPAM)。 安装完成后( curl https://nixos.org/nix/install | sh ),你可以使用以下命令启动CoqIDE和Math-Comp:

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

    然后你可以用From mathcomp Require Import ssreflect.来启动你的文件From mathcomp Require Import ssreflect.