现在我正在从软件基础继续前进，在那里一切都在盘子上提供，我很难弄清楚如何设置自己的项目。那里有一些说明，但由于我刚刚开始，我在尝试设置hello world程序时发现这太复杂了。我还有一些其他问题。
hello.v
我设法编译空hello.v的方法是将上述内容放入_CoqProject文件中，然后运行......
coq_makefile -o Makefile.coq -f _CoqProject
这会生成生成文件。
make -f Makefile.coq
这会编译项目，但我无法make hello只使用它，而 Proof General 碰巧在编译单个文件时使用它。
make hello.vo
make: *** No rule to make target 'hello.vo'. Stop.
以上是我尝试从证明一般编译时得到的。
我应该在这里做什么？用空文件设置一个项目以与 Proof General + Emacs 一起使用的最简单方法是什么？
-Q . VFA
另外，为什么 SF vol 3 尽管它的_CoqProject文件中没有太多内容，但它仍然可以工作？它只有上述内容。
2022 年更新
有一个模板可以创建新项目并生成关联的样板：https://github.com/coq-community/templates
<小时 />原答案
以下是传统设置的样子(它实际上并不是标准化的，你会发现野外的变化，特别是对于旧项目，以及现在支持 Coqdune的未来项目(：
_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中(。
证明一般
在证明一般中，有一个选项"在需要之前编译"，顾名思义。(Coq>自动编译>需要前编译(
您似乎一直在使用的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里有什么。
另外，为什么SF vol 3在_CoqProject文件中没有太多内容的情况下仍然可以工作？它只有上述内容。
现在所有 SF 卷都是这样工作的。对于使用Proof General/CoqIDE进行交互式编辑，只有-Q选项很重要(实际上，-R和其他一些选项也很重要(，而不是文件名。文件名由coq_makefile使用，但您也可以更改coq_makefile的调用以从其他地方获取文件名，例如作为直接命令行参数：
# If _CoqProject only contains the -Q option
coq_makefile -f _CoqProject theories/hello.v