Nix：インストールssreflect

Question

私はCoq（バージョン8.5-6）を使用しています。私はssreflect、好ましくはw/Nixもインストールしたいと思う。私がこれについて見つけた唯一の情報はhereです。しかし、単にssreflectをインストールするだけではありません。それにもかかわらず、私はそれを試してみましたが、何百という警告（さまざまな.vと.ml4ファイルの内容について）が終了し、処理が終了するのを待つことができませんでした。かなり一般的な警告は、このように見えた：

ファイル「./algebra/ssralg.v」、行856、文字0-39：警告： 暗黙の引数が廃止されました。代わりに

使用引数そこで質問：どのように地球上で私は ssreflectニックス/ wのインストールのですか？

EDIT：ejgallegoのコメントを読んだ後、ssreflect w/Nix - espをインストールすることができないようです。 ssreflectのみをインストールしたい場合は、他のモジュール（fingergroup、algebraなど）を使用してください。だから私はまた、次の質問をした：

standard Opamまたはmake installインストールssreflectのインストールは、Nix-installed Coq？

Answer 1

あなたが知っておく必要があるいくつかあります。

• ニックスはバイナリキャッシュとソースベースのパッケージマネージャです。多くのパッケージがバイナリキャッシュにあらかじめ構築されており、利用可能であるため、インストールに時間がかかりません。いくつかのパッケージ（特に開発ライブラリ）はあらかじめビルドされておらず、Nixはそれらをコンパイルするのに時間がかかります。最初は完全なコンパイルを待つだけで済みます（そして、コンパイル時にたくさんの警告を出します）。次回は、あなたのローカルのNixストアでパッケージが利用可能になります。

• OPAMもソースベースであるため、Nixの代わりにOPAMを使用しても時間が節約されるわけではありません。 OPAMがSSReflectをインストールして、後者はOPAM依存性として、元をお勧めしますので、あなたは、ニックス、インストールCoqの重複が整理することはできません。

• ライブラリを使用するNixの方法は、インストールするのではなく、代わりにnix-shellをロードすることです。 nix-shellは、ライブラリの「インストール」と（この場合、例えば$COQPATH）あなたのためのいくつかの環境変数を設定します。

• またニックス-インストールコックを使用してソースから自分でパッケージをコンパイルすることができますが、これはコックがインストールされているが、ニックスストアが非可変である同じ場所でSSReflectをインストールしようとするので、あなたはmake installを実行することはできません。代わりに、この手順をスキップして$COQPATHを手動で設定できます。

• 確かに、完全な数学-COMPのコンパイルは、非常に長い時間がかかります。より軽いCoq ssreflectパッケージがあります。あなたは使用してそれを得ることができます。

  nix-shell -p coqPackages_8_6.ssreflect