7

我是一名 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 库的任何帮助。

4

1 回答 1

8

非常感谢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 菜单中打开首选项
  • 将 Externals -> coqtop（或者它可以是 AUTO ）设置为“/opt/local/bin/coqtop”（或安装您的版本的任何位置）应用 OK 关闭。
  • 退出并重新启动 CoqIDE。

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

Require Import ssreflect.
于 2015-06-12T18:49:49.287 回答