我无法加载 CoqIde 中同一文件夹中的模块。
我正在尝试从 Software Foundations 加载源代码，我在包含带有coqideor的 SF 源代码的文件夹中运行 coqide coqide ./，然后在打开并运行文件后，出现此错误：
Error: Cannot find library Poly in loadpath
在这一行：
Require Export Poly.
其他所有require命令都一样。
那么你们是如何将 SF 中的程序加载到 coqide 中的呢？
如果需要，您需要将 .v 文件编译为 .vo 文件并将其目录添加到加载路径中。要编译它们，coqc <file-path>请在命令提示符下运行。要将文件的目录添加到 CoqIde 中的加载路径，您可以Add LoadPath "<directory-path>".在 .v 文件的开头插入该行。
我意识到这是一个旧线程，但是关于这个问题的资源并不多。我只是花了一些时间来解决它，所以我认为将它发布在我从谷歌搜索得到的第一个主题上会很好。我在 Arch Linux 上使用 Coq 8.4p16 编译，没有额外的配置。
所以，手册说变量像$COQPATH, ${XDG_DATA_DIRS}/coq/和${XDG_DATA_HOME}/coq/被检查，但是我对这些没有运气。
我也试过把coqc -I /folder/pathCoqIde放在Edit->Preferences->Externals那里，但是仍然没有运气。
我写这些是因为它们可能为某人工作。
唯一对我有用的全局方法是在其中编写一个 coqrc 文件Add LoadPath "<directory-path>".。在 Linux 上，该文件需要位于主文件夹中。
希望这可以节省一些时间。
为了能够在 coqtop、coqc、CoqIDE 或 Proof General 中加载源文件，有几种方法，一种方法如下：
假设您已经下载了 Adam Chlipala 编写的名为Certified Programming with Dependent Types的书的代码文件，这些文件可在此处获得，并将它们提取到我们称为 CODEHOME 的路径中。如您所见，任何源文件中都有第一行Require Import Bool Arith List Cpdt.CpdtTactics.
首先输入coqc -vcli（命令行界面），输出类似于The Coq Proof Assistant, version 8.4pl4 ....，然后创建一个名为coqrc.8.4pl4的文件，文件扩展名应与您使用的 coq 的版本一致，在 $HOME/ 中。 config/coq 目录，如果它不存在并将这一行写入其中，仅此Add LoadPath "CODEHOME/cpdt/src" as Cpdt .而已。
如果你开始你file.v的Module file.只是摆脱它（也摆脱它End file.），你的问题就解决了。