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

Question

我无法加载CoqIde中相同文件夹中的模块.

我试图从软件基金会加载来源,我跑在包含SF sources文件夹coqide 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文件的开头插入该行.

Answer 2

我意识到这是一个旧线程,但是这个问题没有太多资源.我只是花了一些时间解决它,所以我认为将它发布在我从google搜索获得的第一个主题上会很好.我正在使用Coq 8.4p16编译而没有在Arch Linux上进行额外配置.

因此,手册说变量喜欢$COQPATH, ${XDG_DATA_DIRS}/coq/和${XDG_DATA_HOME}/coq/检查,但我没有运气.

我也尝试过coqc -I /folder/path使用Edit->Preferences->ExternalsCoqIde,但是,那里仍然没有运气.

我写这些,因为它们可能适合某人.

对我有用的唯一GLOBAL方法是在其中编写coqrc文件Add LoadPath "<directory-path>"..在Linux上,该文件需要位于主文件夹中.

希望这能节省一些时间.