0

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

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

所以问题是：我到底如何安装带有 Nix 的 ssreflect？

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

标准的 Opam或ssreflectmake install的安装是否可以与 Nix 安装的 Coq 一起工作？

4

1 回答 1

2

您需要注意以下几点：

  • 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
于 2017-06-11T13:23:49.137 回答