Coq:使用子目录管理项目中的LoadPath

Question

我有一个Coq项目,其库被组织成子目录,如:

…/MyProj/Auxiliary/Aux.v
…/MyProj/Main/Main.v  (imports Auxiliary/Aux.v)

当我编译文件时,我希望从工作目录MyProj(通过makefile)这样做.但是我也想使用Proof General/Coqtop来处理文件,在这种情况下,工作目录默认是文件所在的目录.

但这意味着两个上下文之间的LoadPath是不同的,因此库导入所需的逻辑路径是不同的.如何设置coqc调用,LoadPath和导入声明,以便它们在两个上下文中都能工作？

我尝试过的每种方法都出了问题.例如,如果我Aux.v通过调用编译

coqc -R "." "MyProj" Auxiliary/Aux.v

并将其导入Main.v为

Require Import MyProj.Auxiliary.Aux.

然后,当我编译时Main.v,这工作

coqc -R "." "MyProj" Main/Main.v

但在Coqtop失败了Error: Cannot find library MyProj.Auxiliary.Aux in loadpath.另一方面,如果在Require Import我添加之前

Add LoadPath ".." as MyProj.

然后这在Coqtop中工作,但是失败coqc -R "." "MyProj" Main/Main.v了

Error: The file […]/MyProj/Auxiliary/Aux.vo contains library

MyProj.Auxiliary.Aux而不是库MyProj.MyProj.Auxiliary.Aux

我正在寻找一个对于与协作者共享的库(并希望最终与用户共享)的强大解决方案,因此特别是它不能使用绝对文件路径.我现在发现的最好的方法是在Proof General调用Coqtop时添加emacs局部变量来设置LoadPath:

((coq-mode . ((coq-prog-args . ("-R" ".." "MyProj" "-emacs")))))

但是这个(a)似乎有点hacky,而且(b)只适用于Proof General,而不适用于Coqide或普通的Coqtop.有更好的解决方案吗？

Answer 1

请允许我通过建议蒂亚戈暗示的替代流程来支持你的问题.

假设您的项目树看起来像这样:

MyProj/Auxiliary/Aux.v
MyProj/Main/Main.v

在MyProj,写一个列出所有Coq文件的_CoqProject文件

-R . ProjectName
Auxiliary/Aux.v
Main/Main.v

当您打开其中一个Coq文件时,emacs将查找_CoqProject和do-the-right-thing(tm).

如Tiago所示,coq_makefile还将免费提供Makefile.

Answer 2

我知道您明确要求某种可以跨不同平台工作的东西，但已经有一种特定于证明通用的解决方案，它比您现有的解决方案更简单。Proof General有一个名为的特殊变量coq-load-path，您可以使用局部变量进行设置，就像您对coq-prog-args. 优点是您不必担心需要传递的任何其他参数coqtop（例如-emacs在您的示例中）。因此，您的.dir-locals.el文件可能有这样的行：

((coq-mode . ((coq-load-path . ((".." "MyProj"))))))

不幸的是，我不知道任何跨平台的东西，尽管我很确定 CoqIDE 特定的东西一定存在。如果是这种情况，也许您可​​以设置一个脚本来保持这些配置文件在不同平台上更新？