Lean 4 分阶段构建与 Olean 持久化信息测试理解 stage1 假性失败并正确切换到 stage2【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4Lean 4 是一款自举bootstrapped实现的定理证明器与编程语言其编译器主体由 Lean 自身编写因此仓库采用多阶段stage0/stage1/stage2/stage3构建链来打破自举循环。本篇指南聚焦一个非常具体、且在实际开发中极易踩坑的场景当你的改动影响了写入.olean文件的信息例如新增或修改了环境扩展 Environment Extension时stage1 测试可能假性失败。本文将基于仓库内建开发指南与源码解释根因、诊断流程并给出切换到 stage2 构建与测试的完整实操命令。读完本文你将能够识别某次 stage1 测试失败是否属于olean 持久化信息不一致导致的假性失败在用户确认后正确构建 stage2用 stage2 环境运行测试套件并理解clean-stdlib、按模块 Lake 构建等细节背后的原因。1 背景为什么 Lean 需要 stage0 / stage1 / stage2 多阶段构建Lean 编译器与前端src/Lean下数千个.lean文件本身就是 Lean 程序因此存在鸡生蛋问题编译编译器需要编译器。仓库通过doc/dev/bootstrap.md描述的机制打破这一循环——把预先编译好的 C 代码归档在stage0/src检入仓库代替最初的 Lean 输入然后分多个阶段向上编译到固定点。从仓库根目录CMakeLists.txt可以看到各阶段的定义stage0 使用SOURCE_DIR ${LEAN_SOURCE_DIR}/stage0构建随后依次是stage1-DSTAGE1 -DPREV_STAGE${CMAKE_BINARY_DIR}/stage0、stage2-DSTAGE2 -DPREV_STAGE${CMAKE_BINARY_DIR}/stage1与 stage3依赖 stage2并声明add_custom_target(check-stage3 COMMAND diff stage2/bin/lean stage3/bin/lean)来校验 stage2/stage3 二进制一致。各阶段目录的典型布局如下见 doc/dev/bootstrap.mdstage0/ bin/lean # 自举二进制由 stage0/src 编译而来视为黑盒 stage1/ include/config.h # 构建 lean 用的配置变量如分配器 include/runtime/lean.h share/lean/lean.mk # leanmake 使用的 Makefile lib/lean/**/*.olean # 由上一阶段 lean 编译出的 Lean 库含编译器 lib/temp/**/*.{c,o} # 库导出为 C 并用 leanc 编译的结果 lib/libInit.a libLean.a libleancpp.a libleanshared.so bin/lean # 最终编译器 服务器直接调用 libleanshared.so bin/leanc # C 编译器包装器提供搜索路径等 bin/leanmake stage2/... stage3/...构建任意阶段用make stageN在构建目录内。直接运行make默认构建 stage1通常足以用于测试测试套件或 stdlib 之外的改动。关键认识doc/dev/bootstrap.md原文要点每个阶段的 stdlib 使用前一阶段的编译器构建但从不加载前一阶段的 stdlib一切皆为prelude因此当前阶段的meta代码改动通常只影响后续阶段——这既是分阶段的意义也是假性失败的根源stage3 理论上应与 stage2 完全一致仅作为健全性检查check-stage3目标即比较两者二进制。2 核心概念.olean 文件与持久化环境扩展2.1 .olean 是什么.olean是 Lean 的编译产物对象文件它序列化了模块的声明、以及编译器后续读取所需的信息。在 src/Lean/Environment.lean 中OLean相关代码注释明确说明.olean序列化会调用Environment.toKernelEnv第 67 行附近且定义了一个 .olean 文件的内容第 107 行附近。stage1 目录中的lib/lean/**/*.olean正是 Lean 库含编译器自身的 olean 集合——它们由 stage0 编译器生成stage2 的 olean 则由 stage1 编译器生成。这就是不一致的温床stage1 的lean二进制在导入 olean 时读到的是改动前stage0 时代写入的旧格式/旧信息。2.2 环境扩展Environment Extension与 olean 持久化环境扩展是 Lean 内核之上用于承载各类元数据如 notation、宏、属性、简化规则等的机制。其中与本文最相关的是PersistentEnvExtension与ScopedEnvExtensionsrc/Lean/ScopedEnvExtension.lean定义了Entryglobal/scoped、Descr等结构。Descr中包含ofOLeanEntry、toOLeanEntry、exportEntry?等字段即从 olean 读回、以及向 olean 写出的钩子。src/Lean/Environment.lean 中PersistentEnvExtension的文档约 1588 行起说明α 是存储在 .olean 文件中的条目类型exportEntriesFn负责在模块结束时把当前模块的状态序列化到 olean而getEntries用于读回模块 m 被精化时由ext.exportEntriesFn保存的数据第 1667 行附近。同时注意EnvExtension.AsyncMode文档第 1253 行附近对于持久化环境扩展写入.olean的状态总是getState (asyncMode : .sync)在主环境分支上、于文件末尾计算的结果——也就是说olean 持久化的是全部并行分支合并后的扩展状态。这一细节在涉及并行精化的模块中尤为重要。2.3 什么改动会污染 olean从上述结构可以推断以下几类改动都会改变 olean 中持久化的信息从而触发假性失败风险新增/修改/删除环境扩展含PersistentEnvExtension、ScopedEnvExtension、SimplePersistentEnvExtension见 src/Lean/EnvExtension.lean 中SimplePersistentEnvExtension的实现改变exportEntriesFn/ofOLeanEntry/toOLeanEntry的序列化内容或类型改变 olean 文件格式本身如新增字段、调整布局编译器读取 olean 的行为变化例如新增读取某个扩展状态的逻辑。这类改动常被形象地称为meta 改动它们影响的是编译器如何产生代码/olean而非普通库代码。3 问题现象stage1 的假性失败3.1 为什么 stage1 测试会假性失败把上述两节串起来就能解释 SKILL 文档描述的现象stage1 的src/含Init由stage0 编译器编译stage0 编译器缺少你的改动因此它生成的 olean 中不包含新扩展信息或仍是旧格式/旧语义stage1 的lean二进制是包含改动的编译器但它在运行测试时导入的是改动前写入的 olean于是那些依赖新 olean 信息的测试就会失败——然而这不是你的代码逻辑错误而是编译器与它读入的 olean 之间版本错配。用doc/dev/bootstrap.md中的话说当改动 .olean 格式时stage1 编译器可能无法加载自己的 stdlib——stage1 的 stdlib 使用 stage0 编译器生成的格式而 stage1 编译器期待新格式。此时就应该转向 stage2stage2 的整个 stdlib 由包含改动的 stage1 编译器编译格式与编译器自身一致。3.2 诊断要点先确认是否依赖 olean 信息面对一次 stage1 测试失败按 SKILL 文档给出的判定标准如果这次改动依赖的是改动后的 olean 信息例如新增或修改了编译器会读回的环境扩展那么相关测试必须改在stage2上运行。换句话说失败本身不足以说明问题关键在于判断失败的测试是否读取了被改动持久化的信息。若你的改动与 olean 内容无关纯库函数、普通定理、不涉及编译器的解释器/代码生成行为stage1 的失败通常就是真实回归不应贸然切换 stage2。4 实操构建 stage2 并在其上运行测试4.1 先与用户确认SKILL 文档第一条纪律构建 stage2 代价高昂切换前必须先与用户确认。这是因为 stage2 需要重新编译整个标准库与编译器自身耗时显著高于增量式 stage1 迭代。4.2 构建 stage2使用stage2-build技能中给出的命令该技能与本文档同属.claude/skills/目录make -C build/release stage2 -j$(nproc)关于增量的两个关键点均出自stage2-build/SKILL.mdstage2 不会被src/的改动自动失效这是特性而非缺陷允许你在修复某个特定文件时快速迭代但若要使已经通过 stage2 构建的文件失效或做最终验证必须手动执行make -C build/release/stage2 clean-stdlibclean-stdlib同样记载于doc/dev/bootstrap.md它删除已生成的 olean/提取产物强制重建用于观察成功模块的 olean 变化或确认没有破坏先前构建成功的模块。注意该命令只清理标准库产物不会删除构建目录仓库规则严禁手动删除build/等目录。4.3 按模块增量构建Lake当只想重建 stage2 的个别模块时直接使用 Lake在 stage2 的构建目录内构建cd build/release/stage2 lake build Init.PreludeInit.Prelude是最底层的模块几乎所有内容都依赖它——若它因 olean 格式变化而重建成功说明编译器与 olean 已达成一致。你也可以用同样的方式构建其他模块。4.4 在 stage2 上运行测试测试命令只需把-C build/release换成-C build/release/stage2其余不变。这与 tests/README.md 中特定阶段运行测试的说明一致# 全量测试stage2 CTEST_PARALLEL_LEVEL$(nproc) CTEST_OUTPUT_ON_FAILURE1 \ make -C build/release/stage2 -j $(nproc) test # 只重跑之前失败的测试 CTEST_PARALLEL_LEVEL$(nproc) CTEST_OUTPUT_ON_FAILURE1 \ make -C build/release/stage2 -j $(nproc) test ARGS--rerun-failed # 按正则挑选测试-R特殊字符需双引号 CTEST_PARALLEL_LEVEL$(nproc) CTEST_OUTPUT_ON_FAILURE1 \ make -C build/release/stage2 -j $(nproc) test ARGS-R grind_ematch注意tests/README.md提醒在build/release/stagen内手动运行 bench 套件时不要指定-j $(nproc)bench 需要串行化以保证测量可靠。测试套件的组织也值得了解tests/下的目录分测试目录含run_test.sh/run_bench.sh整个目录一个测试与测试堆每个.lean文件一个测试可用file.no_test、file.serial等辅助文件控制行为compile堆会编译后执行并核对输出elab堆只精化不执行详见 tests/README.md。5 为什么 stage2 能解决自举链的传递性回到doc/dev/bootstrap.md的标准构建流程一次普通make实际包含三步把stage0/src归档源码编译成stage0/bin/lean用它把当前库包括你的改动编译进stage1/lib把该库与src/中的当前 C 代码链接成stage1/bin/lean。可见 stage1 的二进制已包含你的改动但其 stdlib 的 olean 由旧编译器生成。而构建 stage2 时PREV_STAGE指向 stage1stage1 编译器含改动会重新编译整个库为 stage2 的 olean——编译器与 olean 首次在同一代统一。之所以 stage2 可行而不会继续传染是因为构建某阶段 stdlib 时只使用前一阶段的编译器、从不加载前一阶段的 stdlib全部是prelude。doc/dev/bootstrap.md明确指出我们不知道有任何meta-meta部分能影响超过两代编译所以 stage3 应与 stage2 完全一致仅作为健全性检查存在——这也是根目录check-stage3目标用diff比对两个二进制的原因。6 相关的自举复杂性与注意事项虽然本文聚焦 olean 持久化场景doc/dev/bootstrap.md还记录了两种相关的meta 改动特殊情形理解它们有助于避免误判6.1 引号quotations与当前阶段解析器内置解析器的改动希望立即影响引号quotation引号在当前阶段执行时捕获语法树结构并转为下一阶段的代码因此构建 Lean 时会默认设置-Dinternal.parseQuotWithCurrentStagetrue让引号通过解释器使用当前阶段的解析器但对macro/macro_rules/elab/elab_rules会强制禁用suppressInsideQuot因为这些命令保证不会在下一阶段运行正确做法是使用 stage0 解析器。还需注意解析器必须能通过import语句可达否则会静默使用前一阶段的版本且只有解析器代码Parser.fn受影响前导 token 等元数据仍取自上一阶段。6.2 非内置 meta 代码与interpreter.prefer_native对Notation.lean中非内置的notation、macro等期望改动立即影响当前文件及同阶段后续文件。为此 Lean 以-Dinterpreter.prefer_nativefalse构建否则解释器发现已有原生符号会运行上一阶段的旧代码。但某些情况下必须反向设置当解释器由上一阶段的原生代码执行时其计算值的类型必须与上一阶段 ABI 兼容例如给Macro增加参数、重排ParserDescr构造子此时需prefer_nativetrue将 meta 代码冻结在上一阶段版本且本阶段不得引入新 meta 代码下一次update-stage0后的阶段再设回false。相关标志通过修改stage0/src/stdlib_flags.h调整且下次update-stage0会用src/的原始版本覆盖重置。这些机制的共同启示是改动在哪个阶段生效是 Lean 自举开发的核心心智模型而 olean 持久化信息正是最容易触发 stage1 假性失败的一类。7 总结决策清单场景判定动作stage1 测试失败改动新增/修改了写入 olean 的信息环境扩展、序列化内容、olean 格式、编译器读取逻辑假性失败可能性高与用户确认后切 stage2make -C build/release stage2 -j$(nproc)在build/release/stage2下跑测试stage1 测试失败改动与 olean 无关真回归继续在 stage1 排查不要切 stage2需要使已构建的 stage2 文件失效含最终验证—make -C build/release/stage2 clean-stdlib后重建只重建个别 stage2 模块—cd build/release/stage2 lake build 模块校验 stage3 与 stage2 一致性—make check-stage3仓库默认目标核心结论一句话当改动影响 olean 持久化信息时stage1 测试失败是编译器与旧 olean 的版本错配所致应在 stage2 上验证而切换 stage2 前务必先与用户确认因为它需要完整重编译整个库。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考