coq - 如何使用 Proof General + Emacs 编译 Coq 文件？

Question

现在，我要从软件基础中继续前进，在软件基础中，一切都放在盘子上，我在弄清楚如何建立自己的项目时遇到了困难。有some instructions那里，但由于我刚刚开始，我发现在尝试设置 hello world 程序时这太复杂了。我还有一些其他问题。

hello.v

我成功编译空 hello.v 的方法是将以上内容放入 _CoqProject 文件中，然后运行...

coq_makefile -o Makefile.coq -f _CoqProject

这将生成 makefile。

make -f Makefile.coq

这会编译项目，但我无法使用 make hello 来使用它，而 Proof General 在编译单个文件时恰好使用了它。

make hello.vo
make: *** No rule to make target 'hello.vo'.  Stop.

以上是我尝试从 Proof General 进行编译时得到的结果。

我应该在这里做什么？使用空文件设置项目以与 Proof General + Emacs 一起使用的最简单的方法是什么？

-Q . VFA

此外，为什么 SF vol 3 可以工作，尽管它的 _CoqProject 文件中没有太多内容？它只有以上内容。

Answer 1

2022 年更新

有一个模板可用于创建新项目并生成关联的样板:https://github.com/coq-community/templates

---

原始答案

这是传统设置的样子(它实际上并未标准化，您会发现各种变化，特别是对于旧项目以及 dune 现在支持 Coq 的 future 项目):

_CoqProject
Makefile
theories/
  hello.v

使用以下_CoqProject:

-Q theories/ MyProject
theories/hello.v
# list paths to .v files here

特别是，限定项目 (-Q path/ProjectName) 可以避免歧义(如果在其他地方使用相同的模块名称)，并且可以更轻松地从其他项目导入。

以及以下Makefile:

build: Makefile.coq
    $(MAKE) -f Makefile.coq

Makefile.coq: _CoqProject
    coq_makefile -f _CoqProject -o Makefile.coq

.PHONY: build

build 目标被标记为 .PHONY 以表明它并不意味着创建文件/目录。这可以避免其他工具出于任何原因创建 build 目录时出现问题。

命令行

要从命令行构建整个项目，请键入 make (默认情况下相当于 make build，因为 build 是第一个Makefile 的命令)。
要仅构建一个 .vo 文件(例如 theories/hello.vo)，请输入 make -f Makefile.coq theories/hello.vo。它必须列在 _CoqProject 中(以便 coq_makefile 然后将其放入 Makefile.coq.conf)。

一般证明

在 Proof General 中有一个选项“Compile Before Require”，正如其名称所示。 (Coq > 自动编译 > 在 Require 之前编译)

由于当前缺乏可配置性，您似乎一直在使用的 coq-Compile 命令似乎已被放弃。 coq-Compile 调用 make hello.vo，但 Makefile 中没有 hello.vo 目标，这会导致是 make 默认查看的一个，除非设置了 -f 选项。使此 PG 命令与该设置配合使用的一种方法是将生成的 Makefile.coq 包含在 Makefile 中:

# Add this line to Makefile to enable PG's "coq-Compile"
-include Makefile.coq

我个人对此犹豫不决，因为我不太了解 Makefile.coq 中的内容。

---

Also, why does SF vol 3 work despite not having much in its _CoqProject file? It only has the above.

现在所有 SF 卷都以这种方式运行。对于使用 Proof General/CoqIDE 进行交互式编辑，只有 -Q 选项很重要(实际上，-R 和其他一些选项也很重要)，而不是文件名。文件名由 coq_makefile 使用，但您也可以更改 coq_makefile 的调用以从其他地方获取文件名，例如作为直接命令行参数:

# If _CoqProject only contains the -Q option
coq_makefile -f _CoqProject theories/hello.v