SSReflectとMathCompをLinuxにインストールするには？

Question

私はCoq 8.6とCoqIDEをLinuxにうまくインストールしました（Ubuntu 17.04）。しかし、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 

それでは、数学-COMPをインストールできるようにするには、以下のリポジトリを追加してみましょう。

$ opam repo add coq-released https://coq.inria.fr/opam/released 

そして、最後に、ssreflectをインストールします。

$ opam install coq-mathcomp-ssreflect 

OPAMは、依存関係を把握します（Coqを含む）、私たちが尋ねたものをダウンロードしてインストールしてください！

Answer 2

もう1つの方法は、the Nix package manager（OPAMではなく）を使用する方法です。それ（curl https://nixos.org/nix/install | sh）をインストールしたら、以下のコマンドで数学・コンプでCoqIDE利用可能を起動することができます。

は

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

それからちょうど `opamはのCoQ-mathcomp-ssreflectをインストールしていFrom mathcomp Require Import ssreflect.