coqide - 无法从同一文件夹加载模块

Question

我无法加载 CoqIde 中同一文件夹中的模块。

我正在尝试从 Software Foundations 加载源代码，我在包含带有 coqide 的 SF 源代码的文件夹中运行 coqide或 coqide ./ ，然后在打开并运行文件后，我收到此错误:

Error: Cannot find library Poly in loadpath

在这一行:

Require Export Poly.

其他的都是一样的 require命令。

那么你们是如何将 SF 中的程序加载到 coqide 中的呢？

Answer 1

如果需要，您需要将 .v 文件编译为 .vo 文件并将其目录添加到加载路径中。要编译它们，运行 coqc <file-path>在命令提示符中。要将文件的目录添加到 CoqIde 中的加载路径，您可以插入行 Add LoadPath "<directory-path>".在 .v 文件的开头。