Coq:需要导出的问题

Question

我的问题似乎很常见，但找到的答案都无法解决。我正在学习 Coq 上的软件基础类(class)，所以我来命令:

> From LF Require Export Basics.

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

"Cannot find a physical path bound to logical path matching suffix <> and prefix LF."

我从 coqIde 编译了 Basics.v，并且正确创建了 Basics.vo 文件。我还按照某处的建议从 coqc 命令行编译了它我的 _CoqProject 文件存在于与 Basics.v 相同的文件夹中，并且声明: -Q 。低频_CoqProject 参数设置为“附加到参数”。

当我加载 Basics.v 时，我在 CoqIde 的底部看到“Reading Options from ..._CoqProject”我将 lf 文件夹放入 coq 的 LoadPath 中的文件夹中。

我还能检查什么？

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

谢谢!

Answer 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. 使用选项 Compile->Compile buffer

然后我可以观察到目录 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. 我使用选项 File->Open 重新打开了 toto.v
5. 我执行了文件内容。

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

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

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