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

Question

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

我正在尝试从软件基金会加载源代码，我正在使用coqide或coqide ./在包含SF源代码的文件夹中运行coqide，然后打开并运行该文件后，我收到以下错误：

Error: Cannot find library Poly in loadpath

在这一行中：

Require Export Poly.

对于其他所有require命令也是如此。

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

Answer 1

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

Answer 2

我意识到这是一个古老的线程，但是关于这个问题的资源并不多。我只是花了一些时间来解决这个问题，所以我想把它发布在我通过谷歌搜索得到的第一个主题上会很好。我使用的是在Arch Linux上编译的Coq 8.4p16，没有额外的配置。

所以，手册上说像$COQPATH, ${XDG_DATA_DIRS}/coq/和${XDG_DATA_HOME}/coq/这样的变量都被检查过了，但是我没有用过这些变量。

我也试着让coqc -I /folder/path成为CoqIde的Edit->Preferences->Externals，然而，仍然没有成功。

我写这些是因为它们可能对某些人有用。

对我来说，唯一有效的全局方法是编写一个包含Add LoadPath "<directory-path>".的coqrc文件。在Linux上，该文件需要位于主文件夹中。

希望这能节省一些人的时间。

Answer 3

为了能够在coqtop、coqc、CoqIDE或Proof General中加载源文件，有几种方法，其中一种方法如下：

假设您已经为Adam Chlipala编写的名为“使用依赖类型进行认证的编程”这本书下载了代码文件，这些代码文件可用于here，并将其解压缩到我们称为CODEHOME的路径中。正如您所看到的，在任何源文件Require Import Bool Arith List Cpdt.CpdtTactics.中都有这第一行

首先在cli (命令行界面)中输入coqc -v，输出将类似于The Coq Proof Assistant, version 8.4pl4 ....，然后创建一个名为coqrc.8.4pl4的文件，文件扩展名应该与您正在使用的coq的版本一致，如果它不存在，请在$HOME/.config/coq目录中写入此行Add LoadPath "CODEHOME/cpdt/src" as Cpdt .，仅此而已。