Coq项目coq_makefile构建时外部依赖安装最佳实践

官方标准基础构建流程 #

已梳理官方实用工具文档中描述的Coq项目基础构建流程核心要点，共三步：

• 创建_CoqProject文件，写入传递给coqc的参数，以及按依赖顺序排列的待编译文件列表
• 执行coq_makefile -f _CoqProject -o CoqMakefile命令，自动生成构建文件CoqMakefile
• 使用官方推荐的外层Makefile调用自动生成的构建文件，完成项目编译

外部依赖配置方案 #

官方文档未说明项目所需外部依赖的标准安装、卸载方案，可在外层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                         ##
####################################################################

# 自定义外部依赖安装目标（正确位置：兜底通配规则之前）
install_external_dependencies:
    opam install coq-serapi

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

注：install_external_dependencies目标必须放置在兜底通配规则之前，否则会被通配规则提前匹配，导致依赖安装逻辑无法执行。该配置写法可参考真实开源Coq项目的实现做校验。

模板规则疑问解答 #

针对官方Makefile模板末尾的通配符规则，相关概念解释如下：

规则原文：

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

• %是Makefile的模式通配符，可匹配任意字符串，代表所有未在前面规则中明确定义的构建目标，比如常用的clean、install、vio2vo等Coq原生构建目标都会被该规则匹配
• @true分为两部分：@前缀表示执行后续命令时不在终端打印命令本身；true是Shell内置命令，执行后返回代表成功的0状态码，无任何输出，作用是避免Make因匹配到的目标无对应执行命令抛出错误
• 整条规则的整体功能是做目标转发：所有外层Makefile未显式处理的目标，都会先触发invoke-coqmakefile逻辑完成依赖检查和CoqMakefile生成，再交给自动生成的CoqMakefile实际执行，外层Makefile仅做桥接层，不处理具体构建逻辑

需求说明 #

需要基于_CoqProject+coq_makefile的官方构建流程，提供安装所有项目依赖的端到端最小演示示例，理想方案为提供可一键完成opam switch配置、依赖安装、项目编译全流程的install_project_name.sh脚本。

相关参考要点 #

• Mac M1系列设备无法找到opam软件源时，可通过更新opam源、添加适配arm架构的Coq软件源完成新版Coq安装
• Coq第三方包统一通过OPAM包管理器安装，避免手动编译导致的版本不兼容问题
• 可参考Coq社区中关于初学者Makefile配置的公开讨论内容，获取最佳实践

内容的提问来源于stack exchange，提问作者Charlie Parker