Nix：安装 ssreflect

Question

我正在使用 Coq（版本 8.5-6），安装有 Nix。我想安装 ssreflect，最好还带有 Nix。我发现的唯一信息是here。但是，这与安装 ssreflect 无关，只是尝试一下。尽管如此，我还是尝试尝试一下，但最终收到了数百条警告（关于各种 .v 和 .ml4 文件的内容），并且迫不及待地等待该过程结束。一个相当典型的警告如下所示：

文件“./algebra/ssralg.v”，第 856 行，字符 0-39：警告： 不推荐使用隐式参数；改用参数

所以问题是：我到底如何安装 ssreflect w/ Nix？

编辑：阅读 ejgallego 的 cmets 后，似乎不可能安装 ssreflect w/Nix -- 尤其是。如果只想安装 ssreflect 而不安装其他模块（fingroup、代数等）。所以我也有以下问题：

standard Opam 或 make install 的 ssreflect 安装是否可以通过 Nix 安装的 Coq 工作？

Answer 1

您需要注意以下几点：

• Nix 是一个基于源代码的包管理器，带有二进制缓存。很多包是预先构建的并且在二进制缓存中可用，因此它们的安装不会花费很长时间；一些包（特别是开发库）不是预先构建的，Nix 在安装它们时会花费一些时间来编译它们。请耐心等待：您只需要等待第一次完整编译（是的，math-comp 在编译时会发出很多警告）；下次，您当地的 Nix 商店将提供该软件包。

• 由于 OPAM 也是基于源的，因此使用 OPAM 代替 Nix 不会让您节省时间。您不能将 Nix 安装的 Coq 与 OPAM 安装的 SSReflect 混为一谈，因为后者会希望前者作为 OPAM 依赖项。

• Nix 使用库的方法不是安装它们，而是使用 nix-shell 加载它们。 nix-shell 将“安装”库并为您设置一些环境变量（例如 $COQPATH 在这种情况下）。

• 您也可以使用 Nix 安装的 Coq 从源代码自己编译包，但您不能运行 make install，因为这会尝试将 SSReflect 安装在安装 Coq 但 Nix 商店非可变的。相反，您可以跳过这一步，手动设置$COQPATH。

• 确实，完整的数学运算的编译需要很长时间。有一个更轻的 Coq ssreflect 包。您可以使用：

  nix-shell -p coqPackages_8_6.ssreflect