在COQ项目中安装外部依赖项的最佳实践是什么？

Question

我了解我认为是官方利用的本质doc https://coq.inria.fr/refman/refman/practical-tools/utilities.html#building-a-coq-project ：

• 一个人创建a _coqproject，并用参数为COQC和要编译的文件名（希望以依赖关系的顺序），
• 然​​后使用coq_makefile -f _coqproject -o coqmakefile进行自动coqmakefile
• 然后使用他们的建议makefile运行自动生成的make文件。

但是，如果我们需要其他依赖项，它就不会说如何安装它们（或卸载）。这样做的标准方法是什么？

我的猜测是，一个人可能会在makefile结束时添加目标，并执行某种opam install？

例如，

# KNOWNTARGETS will not be passed along to CoqMakefile
KNOWNTARGETS := CoqMakefile
# KNOWNFILES will not get implicit targets from the final rule, and so
# depending on them won't invoke the submake. TODO: Not sure what this means
# Warning: These files get declared as PHONY, so any targets depending
# on them always get rebuilt -- or better said, any rules which those names will have their cmds be re-ran (which is
# usually rebuilding functions since that is what make files are for)
KNOWNFILES := Makefile _CoqProject

# Runs invoke-coqmakefile rule if you do run make by itself. Sets the default goal to be used if no targets were specified on the command line.
.DEFAULT_GOAL := invoke-coqmakefile

# Depends on two files to run this, itself and our _CoqProject
CoqMakefile: Makefile _CoqProject
    $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile

# Note make knows what is the make file in this case thanks to -f CoqMakefile
invoke-coqmakefile: CoqMakefile install_external_dependencies
    $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))

#
.PHONY: invoke-coqmakefile $(KNOWNFILES)

####################################################################
##                      Your targets here                         ##
####################################################################

# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
    @true

# I know this is not a good coq dependency example but just to make it concrete wrote some opam command
install_external_dependencies:
    opam install coq-serapi

我认为我在正确的位置编写了install_external_depentencies，但我不确定。那是对的吗？有人有一个真实的例子吗？

For all the code see: https://github. com/brando90/ultimate-utils/tree/master/tutorials_for_myself/my_makefile_playground/beginner_coq_project_project_with_makefiles/debug_proj

相关：有关：建立Coq Project of Coq Project of Coq Project of Coq Project的官方培训问题官方的位置到学习者 - 直接coq-coq-make-files-for-beginner/1682“ rel =” nofollow noreferrer“> https://coq.discourse.group/t/official-place-place-place-place-to-to - 浏览 - 固定 - coq-coq-make-for-for-beginner/1682

---

btw， 我还不了解Makefile中的最后一个。

# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
    @true

IE

• ％true在Make File模板COQ中给了我们。
• ％以规则的名义。
• 那条线做什么？

---

更新

我正在寻求一个端到端的小型演示，以了解如何使用_COQPROJECT和coq_makefile使用_coqproject coq_makefile ，如UTISITION doc doc doc a href =“ https://coq.inria.fr/refman/practical-tools/utilities.html” rel =“ nofollow noreferrer”> https://coq.inria.fr/refman/practical-tractical-toolsials/practical-toolsions.htmls.html 。理想的答案将包含一个单个脚本，以一次安装和编译所有内容 - 例如install_project_name.sh中。包括OPAM开关等。

---

相关：

• 当它找不到新版本的Mac M1机器中的存储库时，如何安装新版本的COQ？
• 使用opam
• https://coq.discourse.group/t/official-place-place-place-to-to-learn - 如何到达-coq-make-for-for-Beginner/1682

Answer 1

最简单的设置是用OPAM手动安装外部依赖关系。

opam install packages-needed-by-my-project

然后，他们将立即可以建立您自己的项目。

组织的下一个级别是打包您的项目。请参阅以下COQ社区资源：

• coq社区模板
• 推荐的项目结构

与您的问题立即相关的主要内容是拥有*。在项目根部的文件列出了其依赖项（可能具有版本要求）。然后，您可以使用OPAM安装安装它们。 - 只能Deps-。

---

您问题的MakeFile部分是关于无缝传递选项的过度工程，以coqmakefile。我不确定它是如何工作的，但无论如何都不重要，尤其是因为Dune已成为COQ项目推荐的构建系统。