3

我的问题似乎很常见，但找到的答案都无法解决。我正在关注 Coq 上的软件基础课程，所以我来了命令：

> From LF Require Export Basics.

无论我尝试什么，我总是得到以下答案：

“找不到绑定到逻辑路径匹配后缀 <> 和前缀 LF 的物理路径。”

我从 coqIde 编译了 Basics.v，并且正确创建了 Basics.vo 文件。我还从 coqc 命令行编译了它，正如某处建议的那样，我的 _CoqProject 文件存在于与 Basics.v 相同的文件夹中，并指出：-Q . LF _CoqProject 参数设置为“附加到参数”。

当我加载 Basics.v 时，我在 CoqIde 底部看到“从 ..._CoqProject 读取选项”，我将 lf 文件夹放入 coq 的 LoadPath 中的文件夹中。

我还能检查什么？

我的系统是 Windows 10。我运行 CoqIde 8.9.1

谢谢！

4

1 回答 1

1

我通常在 Linux 机器下工作，但在这里我使用虚拟机做一些事情。

  1. 我从https://github.com/coq/coq/releases/tag/V8.9.1下载了 Windows 安装程序
  2. 我从https://softwarefoundations.cis.upenn.edu/lf-current/index.html下载了 lf.tgz 文件
  3. 我为 Coq 运行了 Windows 安装程序。它将 coq 系统放置在 C:\coq
  4. 我使用cygwin工具来扩展文件lf.tgz，以便我有一个C:\Users\user\foundations\lf包含Basics.v等的目录_CoqProject。

然后我使用搜索命令查找coqide已安装的应用程序。然后我继续执行以下步骤：

  1. 开始coqide
  2. 打开文件Basics.v
  3. 使用选项编译->编译缓冲区

然后我可以观察到该目录C:\Users\user\foundations\lf包含一个名为Basics.vo

  1. 然后我打开了一个新的缓冲区，写了From LF Require Export Basics.并没有尝试执行这一行
  2. 我将此缓冲区保存在目录中的文件中C:\Users\user\foundations\lf。假设这个文件被命名为toto.v
  3. 我关闭了toto.v缓冲区。
  4. toto.v我使用选项 File->Open重新打开了
  5. 我执行了文件内容。

这个过程是反复试验的结果。我所知道的是，Require Export ...只有在您的磁盘上有...vo文件时才有效，但 coqide 需要知道在哪里查找这些文件。为此，它维护了一个“加载路径”。从给定目录打开文件时，coqide 会在该目录（和祖先）中查找_CoqProject文件，后者可能包含修改加载路径的指令。这里的情况是“-Q . LF”表示应考虑当前目录中的所有 .vo 文件，并且它们的符号名称应以前缀“LF”开头。

问题是，当您从一个空缓冲区开始时，没有_CoqProject文件被读取，并且 coqide 不会在哪里查找您的数据。这就是我执行步骤 5-6-7 的原因：在读取文件时toto.v，我引发了对_CoqProject文件的读取。

外卖课程：确保Basics.vo文件存在，然后确保您正在处理的缓冲区是通过同一目录中的读取操作获得的。如果需要，保存、关闭并重新打开以确保是这种情况。

于 2019-09-26T08:06:26.130 回答