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

Question

现在，我要从软件基础中继续前进，在软件基础中，一切都放在盘子上，我很难弄清楚如何建立自己的项目。那里有一些说明，但由于我刚刚开始，在尝试设置 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

另外，为什么《科幻小说》第 3 卷尽管文件内容不多，但仍然有效_CoqProject？它只有以上这些。

Answer 1

2022 年更新

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

原答案

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

_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 buildbuildMakefile
.votheories/hello.vomake -f Makefile.coq theories/hello.vo_CoqProjectcoq_makefileMakefile.coq.conf

证明一般

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

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

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

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

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

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

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