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 )。

双击应用程序时 CoqIDE 加载的/Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop 中的一个(我从 Cog 网站下载)。

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

解决方案如下:

双击 CoqIDE

在 CoqIDE 菜单中打开首选项

将 Externals -> coqtop(或者它可以是 AUTO )设置为“/opt/local/bin/coqtop”(或安装您的版本的任何地方) Apply OK Close。

退出并重新启动 CoqIDE。

我使用终端中的 coqtop 和 CoqIDE 成功加载了 Ssreflect 库:

Require Import ssreflect.