深入 Coq 17：项目组织与持续集成

单文件脚本足够应付练习，但 MathComp、Iris、CompCert 这类真实库管理数百个 .v 文件。本篇覆盖两套主流构建系统（coq_makefile 与 dune）、opam 包发布流程、CI 管道配置和 Coq 版本管理策略。

_CoqProject 与 coq_makefile

_CoqProject 是 Coq 内置构建工具的项目描述文件。一个最小示例：

-Q theories MyLib
-Q tests MyLib.Tests

theories/Basics.v
theories/Induction.v
theories/Lists.v
tests/TestBasics.v

-Q theories MyLib 把 theories/ 目录映射到逻辑路径 MyLib，使得 Require Import MyLib.Basics 解析到 theories/Basics.v。另一个标志 -R 功能相同但会把所有名称不加限定地导入当前命名空间——新项目应避免使用，因为它污染命名空间。

生成 Makefile：

1	`coq_makefile -f _CoqProject -o Makefile`

生成的 Makefile 支持 make、make clean、make install，也支持并行构建：

1	`make -j$(nproc)`

一个常见错误是 _CoqProject 中文件的列出顺序不正确。coq_makefile 依赖 coqdep 分析依赖关系，但如果 Lists.v 依赖 Basics.v 而 Basics.v 列在后面，构建可能失败并报出：

1 2	`Error: Cannot find a physical path bound to logical path MyLib.Basics`

修复方式：手动调整文件顺序，或者重新生成 Makefile 后完整重建：

1 2	`coq_makefile -f _CoqProject -o Makefile make clean && make -j$(nproc)`

更稳健的做法是省略文件列表，只保留 -Q 映射：

1	`-Q theories MyLib`

Coq 8.16+ 支持这种写法，coqdep 会自动发现目录下所有 .v 文件。更早的版本需要显式列出每个文件。

dune 构建系统

dune（Dune 3.x+）通过 coq.theory stanza 提供原生 Coq 支持。在仓库根目录创建 dune-project：

1 2	`(lang dune 3.16) (using coq 0.9)`

每个包含 .v 文件的目录放置一个 dune 文件：

; theories/dune
(coq.theory
 (name MyLib)
 (theories Coq))

; tests/dune
(coq.theory
 (name MyLib.Tests)
 (theories MyLib Coq))

构建与清理：

1 2	`dune build dune clean`

dune 的核心优势在于依赖分析完全自动化。它解析每个 .v 文件中的 Require 声明，自动推导依赖图并确定编译顺序，不需要手动维护文件清单。增量编译也更精确：基于内容哈希而非时间戳，只重新编译受变更影响的文件及其下游依赖。

两套构建系统的核心差异：

维度	coq_makefile	dune
文件发现	手动列出或 -Q 自动发现	全自动
增量编译	基于时间戳	基于内容哈希
多目录组织	单一 _CoqProject	每目录一个 dune 文件
与 OCaml 混编	需手写规则	原生支持
社区采用	老项目居多	MathComp 2.x、Iris 等新项目

对于纯 Coq 项目，两者都能胜任。项目包含 OCaml plugin 或需要混编时（例如编写 Ltac2 扩展，参见本系列第 08 篇；或 extraction 后生成可执行程序，参见第 12 篇），dune 是更自然的选择。

opam 包管理与发布

Coq 社区通过 opam 管理包依赖。一个典型的 coq-mylib.opam 文件：

opam-version: "2.0"
name: "coq-mylib"
version: "1.0.0"
synopsis: "A small Coq library for demonstration"
maintainer: "author@example.com"
license: "MIT"

depends: [
  "ocaml" {>= "4.14"}
  "coq" {>= "8.18" & < "8.21~"}
  "coq-mathcomp-ssreflect" {>= "2.2.0"}
]

build: [
  ["dune" "build" "-p" name "-j" jobs]
]

install: [
  ["dune" "install" "-p" name]
]

depends 中的版本约束值得注意。coq {>= "8.18" & < "8.21~"} 表示支持 Coq 8.18、8.19、8.20，但排除 8.21 的开发版。~ 后缀在 opam 版本排序中排在正式版之前，因此 < "8.21~" 恰好排除所有 8.21 预发布版本。

本地测试安装：

1 2	`opam pin add coq-mylib . --kind=path opam install coq-mylib`

opam pin 把当前目录注册为包源码位置，opam 会就地构建并安装。修改代码后重新运行 opam install coq-mylib 即可更新。

发布到 coq-released 仓库（Coq 社区的官方 opam 仓库）需要向 coq/opam 提交 Pull Request，将 opam 文件放入 released/packages/coq-mylib/coq-mylib.1.0.0/ 目录。

CI 配置

GitHub Actions

coq-community 维护了一套 Docker 镜像，预装各版本 Coq 和 opam，是 CI 的首选基础设施：

# .github/workflows/ci.yml
name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  build:
    strategy:
      matrix:
        coq_version: ['8.18', '8.19', '8.20']
      fail-fast: false
    runs-on: ubuntu-latest
    container:
      image: coqorg/coq:${{ matrix.coq_version }}

    steps:
      - uses: actions/checkout@v4

      - name: Build
        run: |
          eval $(opam env)
          dune build

      - name: Verify no axiom leaks
        run: |
          eval $(opam env)
          coqc -Q theories MyLib scripts/check_axioms.v

check_axioms.v 是一个独立的验证脚本，对关键定理调用 Print Assumptions：

(* scripts/check_axioms.v *)
Require Import MyLib.Basics.
Require Import MyLib.Lists.

Print Assumptions app_assoc.
(* 预期输出: Closed under the global context *)

如果某个定理意外依赖了 functional_extensionality_dep 或其他公理，CI 日志会显示：

1 2	`Axioms: functional_extensionality_dep : ...`

coqc 仍然返回状态码 0，因此这不会自动导致 CI 失败。如需硬性检查，可以编写 shell 脚本解析输出并在发现非预期公理时返回非零状态：

#!/bin/bash
output=$(coqc -Q theories MyLib scripts/check_axioms.v 2>&1)
if echo "$output" | grep -q "^Axioms:"; then
  echo "ERROR: Unexpected axiom dependencies detected"
  echo "$output"
  exit 1
fi

docker-coq-action

对于发布到 coq-released 的项目，coq-community 提供了 docker-coq-action，自动化 opam 构建测试：

jobs:
  build:
    runs-on: ubuntu-latest
    strategy:
      matrix:
        coq_version: ['8.18', '8.19', '8.20']
    steps:
      - uses: actions/checkout@v4
      - uses: coq-community/docker-coq-action@v1
        with:
          coq_version: ${{ matrix.coq_version }}
          opam_file: coq-mylib.opam

这个 action 在容器内执行 opam install .，模拟用户从 opam 安装包的完整流程，包括依赖解析和编译。

Coq 版本管理策略

维护一个 Coq 库需要应对 Coq 自身的版本演进。几种常见策略：

开发期间锁定版本。通过 opam pin 固定 Coq 版本，避免上游变更打断开发节奏：

1	`opam pin add coq 8.19.2`

CI 矩阵仍然测试更宽的版本范围，但本地开发始终在同一版本上进行。

新版过渡期使用 extra-dev 仓库。当 Coq 发布新版本时，部分依赖库可能尚未适配。extra-dev 仓库包含这些库的开发版 opam 文件：

1 2	`opam repo add coq-extra-dev \ https://coq.inria.fr/opam/extra-dev`

这允许在 CI 中测试 Coq 新版本，即使部分依赖库尚未正式发布兼容版本。

多版本兼容的分支策略。MathComp 的做法是每个 Coq 大版本区间对应一个 release 分支（例如 mathcomp-2.2.0 支持 Coq 8.18-8.20），CI 矩阵覆盖所有支持的组合。维护多个分支的代价是分支间的 cherry-pick 和合并工作，但好处是用户安装时不会遇到版本冲突。

对于小型库，通常不需要分支策略。在 opam 文件中设置合理的版本区间（如 >= "8.18" & < "8.21~"），配合 CI 矩阵测试，就足以确保兼容性。当 Coq 新版本引入不兼容变更时，发布一个新版本适配即可。

练习

练习 1（基础）：为一个包含三个文件（Basics.v、Induction.v、Lists.v）的项目分别编写 _CoqProject 文件和 dune-project + dune 配置，确保 Lists.v 可以 Require Import 另外两个文件。分别用 coq_makefile 和 dune 构建，对比构建日志中的依赖分析输出。

练习 2（进阶）：为练习 1 的项目编写 GitHub Actions CI 配置。要求：(a) 在 Coq 8.19 和 8.20 上测试；(b) 在 CI 中对所有公开定理运行 Print Assumptions 并将输出保存为 artifact；© 如果发现非预期公理依赖，CI 应当失败。

练习 3（挑战）：编写 coq-mylib.opam 文件，声明对 coq-mathcomp-ssreflect >= 2.2.0 的依赖。使用 opam pin add coq-mylib . --kind=path 本地测试安装。然后故意将 Coq 版本上界设为当前安装版本之下（例如 coq {< "8.19"}），观察 opam 给出的版本冲突错误信息，理解 opam 的依赖解析诊断。