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

Question

我有一个 Coq 项目，其库被组织到子目录中，例如：

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

当我编译文件时，我希望从工作目录 MyProj（通过生成文件）进行编译。但我也想使用 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

我正在寻找一种解决方案，该解决方案适用于与合作者（并希望最终与用户）共享的库，因此特别是它不能使用绝对文件路径。我目前发现的最好的方法是添加 emacs 局部变量以在 Proof General 调用 Coqtop 时设置 LoadPath：

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

但这 (a) 似乎有点老套，并且 (b) 仅适用于 Proof General，不适用于 Coqide 或普通 Coqtop。有更好的解决方案吗？

Answer 1

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

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

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

Answer 2

如果您使用 coq_makefile，您可以在您的系统中安装该库。

没有 OPAM

要初始化您的项目：

coq_makefile -f _CoqProject -o Makefile

与其他项目共享您的库：

make install

使用 OPAM

假设您安装了 OPAM，您可以使用 coq-shell 来帮助您处理依赖项。

要设置您的项目：

coq_shell_url="https://raw.githubusercontent.com/gares/opam-coq-shell/master/src/opam-coq"
curl -s "${coq_shell_url}" | bash /dev/stdin init 8.4 # Install Coq and its dependencies
eval `opam config env --switch=coq-shell-8.4`         # Setup the environment
coq_makefile -f _CoqProject -o Makefile               # Generates the makefile
opam pin add coq:YOURLIBRARY .                        # Add your library to OPAM

当你更新你的图书馆时，你应该这样做：

opam upgrade coq:YOURLIBRARY

下面是一个使用 OPAM 方法的项目示例：

https://bitbucket.org/cogumbreiro/aniceto-coq/src

Answer 3

请允许我通过提亚戈暗示的替代过程来回避你的问题。

假设您的项目树如下所示：

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

在 MyProj 中，写一个 _CoqProject 文件列出所有 Coq 文件

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

当您打开这些 Coq 文件之一时，emacs 将查找 _CoqProject 并做正确的事 (tm)。

如Tiago所示，coq_makefile还将免费赠送一份Makefile

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

Coq: manage LoadPath in project with subdirectories

coq

没有 OPAM

使用 OPAM