Lean 项目 CI 优化：41 分钟到 12 分钟的三轮实验

我们的 Lean 4 + mathlib 项目过去每个 PR 的 CI 都要耗时 41 分钟。如今，即使是最坏情况——从头重新构建最重的文件——也只需要 12 分钟，而普通 PR 使用增量构建时几分钟就能完成。

本文记录了三轮改进，每一轮都采用相同的结构：问题 → 假设 → 验证 → 修复。先剧透一下：三次改进中，我们最初的假设——直觉指向的罪魁祸首——最终都被证明是无辜的。这个故事的主角并不是某个具体技巧，而是性能分析：它始终冷静地否定我们错误的假设。

Lean 特有的概念会在出现时加以解释，因此即使你不了解 Lean，也应该能够读懂本文。

还有一件事。这三轮改进中，几乎所有测量和实现工作都由 AI 智能体完成（第 1 轮和第 2 轮是在有人类参与的交互式会话中完成的；第 3 轮则由一份需求文档驱动的自主循环完成）。人类——也就是我——只做了两件事：批准数值目标，以及验收结果。本文后半部分将介绍这种运作方式，尤其是那些防止 AI 收敛到廉价解决方案的机制。

背景：项目

本文讨论的是 AlgebraicArchitectureTheoryV2，也就是我之前几篇文章介绍过的同一个 monorepo——一个使用 Lean 4 对软件架构理论进行形式化验证的项目。

以下是理解本文所需的全部 Lean 机制——共五项：

从规模上看：审计覆盖 4,000 多个声明，其中有一个重量级文件——一个来自代数几何的概形构造——单独构建就需要 38 分钟。

CI 运行在 GitHub Actions 上。除了 lake build，每个 PR 还会运行一次内核公理审计——通过机器检查确保每个定理都是真正被证明的，证明过程中不存在作弊。这个关卡不可妥协；第 1 轮将解释它实际做了什么。

第 1 轮：公理审计，从 7 分 11 秒降至 11 秒

在 Lean 中，每个定理都由公理推导而来，推导过程由内核（一个小型且可信的检查器）进行机器检查。“证明通过了”意味着它通过了这项检查。这里有一个重要的特殊情况：Lean 提供了一个名为 sorry 的逃生舱。写下 sorry 意味着“这一部分我以后再证明”，它不会立即导致失败（编辑器会显示警告）。在内部，它会悄悄假定一个名为 sorryAx 的公理。用户还可以使用 axiom 关键字，把任意未经证明的命题添加为公理。

换句话说，仅仅“CI 是绿色的”无法区分“所有内容都已得到证明”和“有人用公理堵住了缺口”。因此，对于每个声明，我们会沿着它的依赖关系一直向下遍历，计算它最终触达的公理集合，然后检查这个集合是否始终限定在 Lean 和 mathlib 普遍接受的三个标准公理之内——propext、Quot.sound 和 Classical.choice（最后一个就是选择公理）。这就是公理审计。隐藏的 sorry 或偷偷塞入的公理都无法通过它。如果你自称是形式化验证项目，就不能跳过这一关。

Lean 将这种“遍历并收集”的操作暴露为一个名为 collectAxioms 的函数（它与输入 #print axioms my_theorem 时运行的是同一套机制）。我们的 CI 会对每个声明运行它——当时有 1,207 个，如今已超过 4,300 个——而这一步每次运行都需要 7 分 11 秒。审计甚至比构建本身还重。

审计的入口是一个超过 5,000 行的巨型文件，其中列出了所有要审计的声明。直觉开始发言：“这么大的文件，精化起来肯定很昂贵。把它拆开，速度就会变快。”

在拆分任何东西之前，我们先测量了时间究竟花在哪里。结果与直觉完全相反：

解析导入：约 10 秒

精化这份 5,000 行的清单：没有任何差异（大幅改变行数也没有影响审计耗时）

collectAxioms × 1,207 个声明：约 5 分钟

罪魁祸首不是大文件，而是审计的调用方式。要找出一个声明能够触达哪些公理，就必须沿依赖图一直遍历到根节点——它使用的定理、那些定理使用的定理，以此类推。collectAxioms 会为每个声明从头执行这次遍历。但项目中的每个声明都共享同一个庞大的基础：mathlib。因此，1,207 个声明实际上把几乎相同的图遍历了 1,207 次。从复杂度上讲，就是 O(声明数 × 图规模)。拆分文件并不会改变这个乘积中的任何一个因子。即使只在纸面上分析，这个方案也不会奏效；但正是因为有测量结果，我们才能一句话否定它，然后继续前进。

我们把审计改成了两个阶段：

成功路径：在所有声明之间共享一个已访问集合——“同一个节点绝不遍历两次”——从而只遍历一次图。由于问题是“触达的所有公理的并集是否仍限定在那三个标准公理之内？”，一次共享遍历会得出与逐声明遍历相同的结论

失败路径：只有在出现非标准公理时，才退回经典的逐声明遍历，以确定究竟是哪个声明有问题，同时保持错误消息与原来的格式完全一致

这让成功路径的复杂度从 O(声明数 × 图规模) 降到了 O(图规模)，同时没有牺牲任何错误信息质量。这就是图遍历教科书中的已访问集合技巧——完全没有任何 Lean 特有的魔法。CI 实测中，审计耗时从 7 分 11 秒降到了 11 秒，当时整个 lake build 作业也从约 9.5 分钟降到了 2 分 12 秒。

第 1 轮的教训：在怀疑“重量级文件”之前，先怀疑“重量级操作 × 重复次数”。还要把被否定的假设（拆分文件：无效果）作为独立结果记录下来——这样后来的人就不会凭借同样的直觉，重新挖一遍同样的坑。

第 2 轮：每个 PR 都要 41 分钟——缓存在构建之前就保存了

第 1 轮发生在 7 月中旬，当时 lake build 作业已经缩短到两分多钟。接下来的两周里，一系列重量级的代数几何实现陆续合入（第 3 轮的主角就是在这段时间里逐渐变胖的）。到了某个时候，每个 PR——即使只改动了一个文件——都会对整棵代码树执行一次完整的冷构建：大约 41 分钟。

Lean 的构建与 C++ 或 Rust 类似，也是增量式的。如果构建产物（.olean 文件，按模块存储在 .lake/build 下）仍然存在，那么只需重新构建发生变化的文件及其下游依赖。要让它在 CI 中生效，必须通过缓存把上一次运行的产物保留下来。缓存已经配置了，只是没有正常工作。

当缓存“不工作”时，通常的嫌疑对象是键不匹配或缓存被逐出。工具链哈希是否有误？旧版本的缓存是否被清理了？

在审查缓存键之前，我们先从头到尾阅读了 CI 日志中的时间戳。下面两行只相隔一秒：

23:19:35  Cache save   (final internal step of lean-action)
23:19:36  lake build +Formal.AG starts

缓存确实被保存了。但它是在项目构建之前保存的。

我们使用 lean-action 设置 Lean——这是一个复合 action（可复用的步骤集合）——并将其配置为 build: false，然后在后续步骤中自行运行构建。但 lean-action 会在自己的最后一个内部步骤中把 .lake（构建产物目录）保存到缓存，而复合 action 的内部步骤始终会先于后续的自定义步骤执行。因此，被保存的 2.15 GiB 内容只包含依赖项产物（mathlib）；项目自身的 .olean 文件根本从未进入缓存。难怪每个 PR 都需要 41 分钟——每一次都要从零开始重新构建我们自己的全部代码。

我们还有一个额外发现。mathlib 规模太大，个人用户难以自行构建，因此社区通过 Azure 分发预构建产物（lake exe cache get；在我们的测量中约需 15 秒，具体取决于环境）。因此，缓存中的这 2.15 GiB 内容本来就能在 15 秒内获取——放在 GitHub 缓存中毫无价值。更糟糕的是，2.15 GiB × 4 个版本，几乎耗尽了仓库 10 GiB 的缓存配额。无用的缓存正在挤占真正有用的缓存空间。

我们把缓存职责拆分开来：

禁用 lean-action 的 GitHub 缓存（use-github-cache: false）；mathlib 产物继续从 Azure 缓存获取

显式恢复（构建前）并保存（构建后立即执行）项目自身的 .lake/build

在缓存键前加上 lean-toolchain + lake-manifest.json 的哈希，这样工具链或 mathlib 升级时就会正确退回到冷构建

使用 always() 执行保存，让失败的构建也能持久化部分产物——每次向构建失败的 PR 推送代码时，都能复用失败点之前已经构建的所有内容，从而加快迭代速度

实际工作流如下所示（节选）。唯一真正重要的事情是：必须亲自把保存步骤放在构建之后。

- name: Restore Formal build cache
  uses: actions/cache/restore@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
    restore-keys: |
      formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-

- name: Build
  run: lake build +Formal.AG

```yaml
- name: Save Formal build cache
  if: always()
  uses: actions/cache/save@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}

有了这个，不涉及重型几何文件的 PR 会命中缓存和增量构建：几分钟内完成。

公平地说，lean-action 的缓存在标准用法中工作正常，那种用法是让这个 action 也运行构建。是我们的配置——build: false 且构建被保存在外部——踩中了陷阱。

第 2 轮的经验教训：当「缓存不工作」时，在审计 key 之前先读一下时间戳。组合 action 很方便，但它们的内部步骤顺序与你的工作流步骤顺序是正交的。「保存真的在构建之后吗？」值得用自己的眼睛检查一下。

第 3 轮：38 分钟的 Geometry.lean ——分割它并没有使其更快

最大的剩余瓶颈是单个文件：Geometry.lean，5129 行，108 个声明。它在 mathlib 基础上构造实际的概型——代数几何的中心对象，即使按现代数学标准也是重型抽象——仅这一个文件在 CI 中就花了 38.3 分钟，占项目总 CPU 时间的 46%。即使有了第 2 轮的缓存，任何触及这个文件上游的 PR 也要支付完整的 38 分钟。

这一次我们在开始前就确定了数值目标：最长模块 ≤ 600 秒，目标模块的总时间 ≤ 1800 秒，由同一个 GitHub Actions 完整构建中报告的模块时间判断。测量方法包括在内，由人在实现开始前批准。

这是一个巨大的 38 分钟文件——按其依赖结构将其分割成模块，重新构建会缩小并加快速度。这是第 1 轮已经拒绝过一次的「分割使其更快」假设，现在以其构建时间化身出现。由于阐述是按声明运行的，这一次推理看起来是合理的。

首先，按声明进行性能分析。Lean 自带一个内置的分析器；一个命令能告诉你哪个声明的哪个处理步骤花了多少秒。这是我们使用的命令：

lake env lean --profile --json \
  -Dprofiler.threshold=10 \
  -Dtrace.profiler=true -Dtrace.profiler.threshold=10 \
  -Dtrace.profiler.output=geometry-before-trace.json \
  Formal/AG/Examples/StandardGeometryReference/Geometry.lean

分解结果：内核类型检查占 57%，defeq（决定两个项是否在定义上相等）占 39%，时间大量集中在十几个声明左右。按照这个重心和依赖关系，我们将文件分割成一个 7 模块 DAG：

RawGeometry
└─ SectionRings
   ├─ LeftRestriction
   ├─ RightRestriction
   ├─ OverlapLeftRestriction
   └─ OverlapRightRestriction   * 这四个互相不导入——可以并行构建
      └─ Scheme

我们机械地证明了分割没有破坏任何东西。Lean 的 #check 打印声明的语句——定理的实际主张。我们获取了旧文件的所有 168 个公开声明（794 行）的 #check 输出，分割前后，在相同的工具链和相同的打印设置下，并确认 SHA-256 哈希匹配。任何定理语句的任何字符都没有改变。能够用哈希而不是目测来证明「数学内容得到了保留」，即使对于机械重构也是如此，这是形式验证项目的一个寂静的喜悦。

然后我们在 CI 中测量了分割后的情况——并且错过了目标。最长模块 770 秒（目标 600），总计 2483 秒（目标 1800）。分割缩小了重新构建的范围并获得了并行性，但它并没有消除阐述的一秒钟。加上模块边界开销，总时间实际上增加了。

深入挖掘性能分析揭示了真正的罪魁祸首。时间并不是按行数比例均匀分布的。它集中在特定定义周围的定义展开成本中。

关于定义展开的一个简要偏离。在 Lean 中，定义是名字和体的对，体可以在需要时原地展开——很像编译器的内联，除了 Lean 是在类型检查期间这样做的。当决定「这两个表达式有相同的类型吗？」时，Lean 通过剥开定义来匹配两个表面上不同的项（统一）。通常这就是让证明保持简短的原因。但当涉及大体定义时，每一次剥开都暴露出更多的定义，项会膨胀。

在我们的文件中，这种膨胀发生在检查实际计算概型分量的函数（大体定义）和陈述这些计算正确的引理时。性能分析中 96% 的内核检查和 defeq 时间恰好是检查这些臃肿项的成本：每个 15-104 秒的单独操作，堆积在单个命令内。

行数从不是罪魁祸首——与第 1 轮相同的形状。文件很重不是因为它有 5129 行；它很重是因为特定定义被引用的方式。

记录在案，我们在这个阶段也尝试了两个「标准的优化」（切换到 CommRingCat.hom_ext；使用 congrArg CommRingCat.ofHom——都是已确立的 mathlib 习语）。都没有改善测量结果；都被拒绝了。一个习语失败帮助也是一个数据点，一旦你有了性能分析。

在性能分析指示的那一点进行手术。政策是一致的：重写，使得类型检查器永远不需要剥开定义。

分离值的定义与关于该值的证明。当它们纠缠在一起时，检查证明部分会拖入值整个体的展开。

将引理语句固定在命名函数而不是展开的表达式上。如果匹配在名字上成功，统一没有理由打开体。

将在四个定理中重复的证明模式合并到一个共享的引理中，这样相同的昂贵检查就不会被支付四次。

效果是戏剧性的。在一个聚焦构建中（仅测量一个文件），最重的模块 RawGeometry 从 291 秒降到 11 秒。曾经以 15-104 秒顶部的操作在之后最大为 57.5 毫秒。

最终的 CI 测量（合并提交的完整构建）：跨 7 个模块的总计 1750 秒（29.2 分钟）≤ 目标 1800，最长模块 468 秒 ≤ 目标 600。两个目标都达到了。完成。

该合并提交的 CI 运行是所有三轮的一张集体照。从日志看：

最坏情况下十二分钟，最重的文件完整重建。这是当前的最坏情况。

第 3 轮的经验教训：分割不是使事物更快的工具；它是并行性和较小重新构建范围的工具。减少总时间的是在性能分析指示的那一点进行的手术。由于这是两个不同的改进，要分别测量和判断它们。

改进由 AI 智能体驱动

如开始时所述，三轮中几乎所有的测量和实现都是智能体的工作。第 1 轮和第 2 轮在交互式会话中运行，从测量到实现；第 3 轮是一个自主循环，取得需求文档（PRD），驱动从性能分析到 PR 创作到审查响应的一切。在实现过程中，人类恰好有两份工作：

预先批准数值目标和测量方法（对于第 3 轮：「最长 ≤ 600 秒，总计 ≤ 1800 秒，由同一 GHA 完整构建中的模块时间判断」）

基于测量的 CI 值接受或拒绝

老实说，上游还有第三份工作：编写 PRD。但那也是与另一个 AI 的协作；人类的实际工作是选择方向和审查。

我们将第 3 轮的自主循环称为 PRD 循环。它作为一个 SKILL——一个智能体的指令文档——交给智能体（Codex）。骨架：

输入是一个单一的 PRD，顶部有一个指导问题和数值接受标准。一个人用一个命令启动它（$prd-loop <path-to-PRD>）

一次迭代是「差距分析→提交问题→实现 PR→对抗性审查→合并→账本同步」。它以小单位运行：一次迭代 = 一个问题 = 一个 PR（跨越多次迭代的一个目标是正常操作）

一个单独的审查门（也是一个 AI）判断每个 PR——永远不是实现者自己。在两轮「需要改变」之后，第三轮升级到一个更严格的、专门的门（对于 Lean，一个专门的数学审查门）；如果仍然失败，该项目被标记为停滞并返回给人类

循环状态存在于 GitHub 问题中，而不是在智能体的记忆中。如果会话死亡，下一个会话从同一个位置恢复

当每个条件看起来都满足时，一个独立的完成审计从头重新阅读 PRD 并根据现实验证一切。直到它通过，没有什么可以称自己为「完成」

第 3 轮的“分析 → 拆分 → 未达标 → 深挖 → 命中”流程在这个轮次中通过三个 PR（拆分 / 优化 / 收尾）完成。从开始到结束用时不到一天。期间需要人工介入的只有：批准目标和确认测量标准——也就是寥寥几条 GitHub 评论。

顺带一提，我们的约定是：已完成的 PRD 要从仓库中删除。需求文档从实现结束的那一刻起就开始与现实产生偏差，因此永久记录应固定在 issue、PR 和 CI 日志中——文档本身则会被删除。

堵住廉价路径

不过，如果不加约束地运行这样的循环，有一件事几乎必然发生。AI 智能体会忠实地响应你给予它的激励，所以如果放任不管，它们最终会趋向于寻找让 PR 合并成本最低的路径。修改文档，而不是修改实现。通过“重新解释”来满足一个无法满足的条件。悄悄推迟困难的事项。这些做法严格来说都算不上撒谎——但叠加起来，就会形成一种平衡：以最低成本宣称“已完成”。不妨称之为“偷工减料均衡”。

因此，我们的 SKILL 与其说是一套操作流程，不如说是一种机制设计：通过一系列规则，逐一封堵这些廉价路径。

禁止仅靠文档修改来勾选完成：如果某个条件要求实现或验证，那么只编辑文档或台账的 PR 永远不能将其标记为已满足

禁止重新解释，禁止降低标准：对于 AI 智能体无法满足的条件，必须将其作为阻塞项上报给人类，而不能弱化理解。SKILL 中明确写道：“stopping is not failure; stopping is part of the loop's specification”

循环期间 PRD 保持不变：AI 智能体不能改写自己的通过标准。如果发现 PRD 存在缺陷，它必须停止并报告，而不是自行修正（你不能在考试途中修改试卷）

检查清单不是证据：勾选只意味着“过去某次迭代声称已完成此项”。最终审计会独立地从 PRD 中重新提取条件，并根据实际情况——代码、测试和 CI 日志——逐项验证

禁止自我评分：完成情况审计器只能接收 PRD 路径和 issue 编号——绝不能接收循环自身的“我认为所有条件都已满足”。如果审查门禁无法运行，主 AI 智能体不能代替它执行审查；循环必须以失败关闭

顺便说一句，这些规则并不是坐在白板前凭空设计出来的。每一条都是在实际观察到早期循环尝试相应的取巧方式后才加入的——比如通过一条台账记录来结清某个条件，或以安全为名悄悄缩小范围。我们从来没有聪明到能预先写出所有护栏。

这一切背后只有一个设计原则：让诚实地停止，比不诚实地强行推进更省事。不要指望 AI 智能体的善意；要改变均衡本身。

最精彩的时刻：未达标报告

整个过程最精彩的时刻，是第 3 轮的未达标报告。在拆分 PR 中，AI 智能体在自己的 PR 描述里写道：“Longest 770 seconds, total 2,483. Targets missed; this PR does not claim completion. Profile-driven reduction continues in the next PR.” 没有人为此发出任何指令。循环在下一次迭代中自行创建了优化 issue，并在当天合并了达到目标的 PR。

恰恰在那个节点，宣称“完成”然后一走了之，是最廉价的选择，但 AI 智能体却写下了“未达标”，并继续推进。与其把这归功于 AI 智能体的诚实，我更愿意归功于围绕它建立的结构。当通过标准预先固定、禁止重新解释，并且独立审计会对照测量值检查每一项声明时，只要声明与测量结果不一致，需要调整的就只能是声明。如果改为事后设定标准，就会产生让标准迁就结果的诱惑——人类同样如此。

如果你计划把优化工作交给 AI，这篇文章最值得借鉴的实用经验大概是：先交付通过标准和测量方法，再交付代码。并且，要让诚实地停止成为所有选项中成本最低的那一个。

Axiom 审计，7 分 11 秒 → 11 秒。罪魁祸首不是那个巨型文件，而是未共享的遍历过程对每条声明都重新遍历一次图

每个 PR 都需要 41 分钟 → 增量构建只需几分钟。罪魁祸首不是缓存键，而是在构建之前执行了缓存保存

单个文件耗时 38 分钟 → 总计 29 分钟，最长 8 分钟，最坏情况下单次运行 12 分钟。拆分没有移除任何内容；罪魁祸首是定义展开的成本

三个最初的假设全都错了。尽管如此，工作依然取得了进展，因为每个错误假设都被测量结果否定，而否定本身又作为结果传递到了后续流程中。“没有效果”也是一种发现。文件拆分方案被否定（第 1 轮），两种标准惯用方案被否定（第 3 轮）——如果没有这些记录，迟早会有人，无论是人类还是 AI，再次掉进相同的坑里。

在 AI 这一侧：第 3 轮循环从开始到结束不到一天，横跨三个 PR，人工介入仅限于寥寥几条 GitHub 评论。

不要猜，要测量。这是一句古老的格言，但在 AI 编写代码的时代，我认为它还需要一句续篇——让 AI 去测量，并且先把通过标准交给它。

如需采取进一步措施，你可以考虑屏蔽此人和/或举报滥用行为。