ssreflect 的 CoqIDE 加载路径错误

Question

我是 Coq 新手，因此为了提高我对证明检查的理解，我正在尝试使用 Ssreflect 库。

我已经在终端运行的 Mac OS v 10.10.3 ( Yosemite ) 上安装了 Ssreflect v 1.5。

然而，当我尝试使用以下方法将库加载到 CoqIDE 8.4p15 时：

Require Import ssreflect.

我收到错误：

Cannot find library ssreflect in loadpath

我试过使用：

Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".

当前设置了 SSRCOQ_LIB，但我收到错误：

The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect

感谢您从 CoqIDE 中加载 ssreflect 库的任何帮助。

Answer 1

非常感谢 Coq-Club Forum 上帮助解决此问题的人员，尤其是 Pierre Boutillier，他查明了问题的原因并提供了解决方案。

问题是我有 2 个 coqtop 副本和 2 个标准库副本：

/opt/local/bin/coqtop 中的一个（这是安装我的副本的文件夹，你的可能在不同的文件夹中）并用于编译 ssreflect（我使用 MacPorts 安装 coq ）。
/Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop 中的一个，双击应用程序时由 CoqIDE 加载（我从 Cog 网站下载）。

因此，当我在 CoqIDE 中时，它调用的 coqtop 版本与我用来编译和安装 Ssreflect 库的版本不同。

解决方法如下：

双击 CoqIDE
在 CoqIDE 菜单中打开首选项
将 Externals -> coqtop（或者它可以是 AUTO）设置为“/opt/local/bin/coqtop”（或者安装您的版本的任何地方）应用 OK Close。
退出并重新启动 CoqIDE。

我在终端中使用 coqtop 并使用 CoqIDE 成功加载了 Ssreflect 库：

Require Import ssreflect.

CoqIDE loadpath error for ssreflect