Nix:安装ssreflect

Question

我使用Coq (版本8.5-6)，安装了w/ Nix。我想安装ssreflect，最好也安装w/ Nix。我发现的唯一有关这方面的信息是here。然而，这并不是关于安装merely，而只是尝试一下。尽管如此，我还是尝试过尝试，但最终得到了w/数百条警告(涉及各种.v和.ml4文件的内容)，并且迫不及待地等待进程结束。一个相当典型的警告如下：

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

因此，问题是:我到底该如何安装ssreflect / Nix？

编辑:在阅读了ejgallego的评论后，似乎不可能安装ssreflect / Nix - esp。如果只想安装etc/out其他模块(fingroup、代数等)。因此，我还有以下问题：

Nix的standard Opam或make install安装会反映工作w/ a Nix安装的Coq吗？

Answer 1

有几件事你需要注意：

• Nix是一个基于源代码的包管理器，具有二进制缓存。很多包都是预构建的，可以在二进制缓存中使用，因此它们的安装时间不长；有些包(特别是开发库)不是预构建的，而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。
• 事实上，完整的数学计算需要很长的时间。有一个包，它更轻。你可以用： nix-shell -p coqPackages_8_6.ssreflect