单反射的CoqIDE加载路径错误

Question

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

我已经在运行在终端上的MacOSv10.10.3(约塞米蒂)上安装了SsResive1.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上帮助解决这个问题的人，特别是皮埃尔·布蒂利尔，他指出了问题的原因并提供了解决办法。

问题是我有2份coqtop和2份标准库：

• 其中一个在/opt/local/bin/coqtop (这是安装我的副本的文件夹，可能是在另一个文件夹中)，用来编译where (我使用MacPorts安装coq )。
• 一个在/Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop中，当双击应用程序时由CoqIDE加载(我从Cog网站下载了它)。

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

解决办法如下：

• 双击CoqIDE
• 在CoqIDE菜单中打开首选项
• 将外部-> coqtop (或者可能是自动的)设置为"/opt/local/bin/coqtop“(或在安装您的版本的地方)应用OK、Close。
• 退出并重新启动CoqIDE。

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

Require Import ssreflect.