我正在使用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