我正在使用Coq（版本8.5-6），安裝w/Nix。我想安裝ssreflect，最好也是w/Nix。我發現的唯一信息是here。但是，這不是關於安裝ssreflect，只是嘗試它。儘管如此，我試圖嘗試一下，但最終得到了數百個警告（關於各種文件的內容.v和.ml4），並且不能等待該過程結束。一個相當典型的警告是這樣的：Nix：安裝ssreflect
文件 「./algebra/ssralg.v」，線路856字符0-39：警告： 隱參數已被棄用;使用參數，而不是
所以現在的問題：如何在地球上我安裝 ssreflect W /尼克斯？
編輯：在閱讀ejgallego的評論後，似乎可能不可能安裝ssreflect w/Nix - esp。如果只想安裝ssreflect w/out其他模塊（fingroup，代數等）。所以我也有以下問題：
請問standard Opam或make install安裝ssreflect工作w /一個NIX安裝Coq？
還有，你需要知道的幾件事情：
尼克斯是一個二進制緩存基於源的包管理器。很多軟件包是預先構建的，並且可以在二進制緩存中使用，因此它們的安裝不需要很長時間;一些軟件包（特別是開發庫）不是預先構建的，而Nix在安裝時需要花費時間編譯它們。請耐心等待：您只需等待第一次完整編譯（是的，編譯時數學comp會發出很多警告）;下一次，該軟件包將在您當地的Nix商店中提供。
由於OPAM也是基於源代碼的，所以使用OPAM代替Nix不會節省時間。你不能混用Nix安裝的Coq和OPAM安裝的SSReflect，因爲後者會希望前者作爲OPAM依賴。
Nix使用庫的方式不是安裝它們，而是使用nix-shell來代替它們。 nix-shell將「安裝」庫併爲您設置一些環境變量（例如，在這種情況下爲$COQPATH）。
您也可以使用Nix安裝的Coq自己編譯軟件包，但無法運行make install，因爲這會嘗試在安裝Coq的同一位置安裝SSReflect，但Nix存儲區不可變。相反，您可以跳過此步驟，並手動設置$COQPATH。
事實上，編寫完整的數學comp需要很長的時間。有一個較輕的Coq ssreflect軟件包。你可以使用獲得它：
nix-shell -p coqPackages_8_6.ssreflect
這些警告是可悲的是正常的，因爲開發商沒有固定的他們。 ssreflect需要花費時間來構建，特別是如果你想構建整個包和它的許多庫。您可以編輯ssreflect的Make來刪除一些庫，或者只是將包分開。 這取決於您的需求，例如，由於OPAM的大小，OPAM將數學comp分發爲5個獨立的包。 – ejgallego
如果你打算只使用戰術插件，它被包含在隊列8.7中，但是請注意，如果沒有至少它的主庫，戰術真的不是很有用。 – ejgallego