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论坛上帮助解决这个问题的人们,特别是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菜单中打开首选项
• 将外部 - > coqtop(或可能是AUTO)设置为"/ opt/local/bin/coqtop"(或安装版本的任何位置)应用OK关闭.
• 退出并重新启动CoqIDE.

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

Require Import ssreflect.