Lean 4 构建基准测试build benchmark完全指南指标体系、采集链路与运行机制【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4导读tests/bench/build是 Lean 4 仓库中一个特殊的基准测试它不测当前 stage 的编译器有多快而是用 stage2 编译器完整构建一遍 stage3 标准库并在构建过程中采集全局与逐模块的性能指标。本文将基于仓库中的 README 与其配套实现run_bench.sh、lean_wrapper.py、lakeprof_measurements.py、lakeprof_report_upload.py展开说明它与其他基准的区别、五类指标的含义与来源、逐模块指标如何通过包装器采集、以及LAKEPROF_UPLOAD_URL报告上传机制。读完本文你将能读懂该基准输出的measurements.jsonl文件并理解每一条指标背后的采集链路。build 基准与其他基准的本质区别在阅读指标之前必须先理解这个基准的定位。原文档明确指出This benchmark executes a complete build of the stage3 stdlib from stage2 and collects global and per-module metrics. This is different from most other benchmarks, which benchmark the stage the bench suite is being executed in.即大多数其他基准是在测试套件当前所处的 stage上运行测的是当前编译器本身的性能而 build 基准是用 stage2 编译器完整构建 stage3 标准库度量的是编译器把整个标准库构建出来这一过程的整体开销——包括解析、类型检查、编译、以及 Lean 前端与 Lake 构建系统之间的交互开销。这一设计在 run_bench.sh 中体现为对STAGE环境变量的显式依赖STAGE_THISstage$STAGE STAGE_NEXTstage$((STAGE 1)) BUILD_ROOT$(realpath $BUILD_DIR/..) BUILD_THIS$(realpath $BUILD_ROOT/$STAGE_THIS) BUILD_NEXT$(realpath $BUILD_ROOT/$STAGE_NEXT)随后脚本按stage$((STAGE 1))-configure目标配置下一 stage并在$BUILD_NEXT中执行make clean-stdlib清空标准库产物确保每次测量都是干净的完整构建而不是增量构建。三类全局指标perf 统计、leanc 报告与 lakeprof 报告1. 构建全过程包装器采集的指标在 README 中第一组指标由包裹整个构建过程的包装器即 tests/measure.py采集指标含义build//cycles整个构建消耗的 CPU 周期数perf stat -e cycles:ubuild//instructions整个构建执行的指令数perf stat -e instructions:ubuild//maxrss峰值常驻内存来自getrusage的ru_maxrssbuild//task-clockperf 报告的 task-clock 时间build//wall-clock墙钟时间perf 的duration_time这些指标的定义可在 tests/measure.py 中找到。其中maxrss在 Linux 上以 KiB 为单位通过 factor 1000 换算成字节task-clock与wall-clock则分别对应 perf 事件task-clock与duration_time单位换算为秒。底层采集方式是基于 Linuxperf stat -j的 JSON 输出tests/measure.py并特意设置了LC_ALLC以避免 perf 输出非法 JSON。2. leanc 的 profile 与 stat 指标第二组指标来自每次leanc调用的--profile和--stat输出并跨所有模块求和READMEbuild/profile/name//wall-clock某编译阶段如 elaborator、type checker 等的耗时单位秒build/stat/name//amount某项计数如imported declarations的总量build/stat/name//bytes某项字节统计的总量。注意这里的关键细节--profile与--stat实际上是传给lean编译器的而该基准通过 lean_wrapper.py 把真正的lean二进制替换成了包装器。在 lean_wrapper.py 中def run_lean(module: str) - None: stdout, stderr measure.main( cmd[ lean, *(--profile, -Dprofiler.threshold9999999), --stat, *sys.argv[1:], ], ... )其中-Dprofiler.threshold9999999将 profiler 输出阈值设得极大目的是输出所有 profiling 阶段而不只是超过默认阈值的阶段。--profile输出格式的解析逻辑对应lean --profile的打印格式其来源是 src/util/timeit.cpp当单次耗时小于 1 秒时输出xxx.xxxms否则输出xxx.xxx s。包装器用正则\t(.*) ([\d.])(m?s)匹配该输出并将ms统一换算为秒lean_wrapper.py。--stat输出则匹配number of (imported .*):\s(\d)$格式的正则lean_wrapper.py把number of imported ...这类统计按名字求和其中以 bytes 结尾的归入//bytes指标单位 B其余归入//amount。3. lakeprof 报告指标第三组指标来自lakeprof report命令READMEbuild/lakeprof/longest build path//wall-clock构建关键路径最长构建路径的墙钟时间build/lakeprof/longest rebuild path//wall-clock重建关键路径的墙钟时间build/lakeprof/longest build path//instructions与.../rebuild path//instructions上述两条路径对应的指令数。其中 wall-clock 指标直接取自lakeprof report -p/-r输出的累计时间rows[-1].cum_time单位 s而instructions 指标则是由 lakeprof 报告的模块列表与本基准自己测得的逐模块指令数合并计算的lakeprof_measurements.pyfor flag, name in [(-p, longest build path), (-r, longest rebuild path)]: rows lakeprof_report(flag) save_measurement(out, fbuild/lakeprof/{name}//wall-clock, rows[-1].cum_time, s) total_instructions sum(instructions.get(row.module, 0) for row in rows) save_measurement(out, fbuild/lakeprof/{name}//instructions, total_instructions)这里的instructions字典来自对已写入measurements.jsonl的build/module/name//instructions指标做反向索引lakeprof_measurements.py——这正是组合采集的含义。逐模块指标包装器如何逐个度量每个标准库模块第四组指标针对每个模块单独采集READMEbuild/module/name//lines模块的源码行数build/module/name//cycles与build/module/name//instructions该模块编译时的 CPU 周期数与指令数build/module/name//bytes .ilean.ilean文件字节数build/module/name//bytes .olean.olean文件字节数build/module/name//bytes .olean.server与build/module/name//bytes .olean.private.olean的 server / private 变体字节数。这些指标全部由 lean_wrapper.py 完成。包装器的核心思路是Lake 在构建每个模块时调用的lean并不是真正的编译器而是这个 Python 脚本见 run_bench.sh 中通过LAKE_OVERRIDE_LEANtrue LEAN$(realpath fake_root/bin/lean) WRAPPER_PREFIX... WRAPPER_OUT...注入环境变量。其工作流程lean_wrapper.py通过--setup参数指定的 setup 文件读取模块名json.load(f)[name]见 get_modulecount_lines统计lean二进制路径对应源文件的行数lean_wrapper.pyrun_lean用--profile与--stat重新执行lean并用measure.main以instructions与cycles两个 perf 事件测量单模块编译lean_wrapper.py若 Lake 传入了--iilean 输出与--oolean 输出路径则分别统计.ilean、.olean、.olean.server、.olean.private的文件大小count_bytes。需要注意的是count_bytes对文件不存在的情况做了静默跳过except FileNotFoundError: return因此并非每个模块都会产出全部字节指标。指标输出格式measurements.jsonl所有指标都通过save_measurement以JSON Lines格式追加写入统一输出文件measurements.jsonl每行一个 JSON 对象data {metric: metric, value: value} if unit is not None: data[unit] unit即每一行形如{metric: build/module/Init//instructions, value: 1234567}若存在单位则额外携带unit字段如秒写作s、字节写作B。这一格式贯穿 tests/measure.py、lean_wrapper.py 与 lakeprof_measurements.py 三处写入点是全套指标的统一承载格式。运行流程与 lakeprof 数据的前置条件run_bench.sh 将整个基准串成三步配置下一 stagemake -C $BUILD_ROOT -j$(nproc) $STAGE_NEXT-configure记录式构建先make -C $BUILD_NEXT clean-stdlib清空旧产物再用lakeprof record -- ...包裹make -j$(nproc) make_stdlib命令其中通过LAKE_EXTRA_ARGS显式指定需要构建的标准库目标Init:olean Std:olean Lean:olean Lake:olean LakeMain:olean LeanIR:olean Leanc:olean LeanChecker:olean分析 lakeprof 数据将lakeprof.log移动到$SRC_DIR后在 src 目录下执行lakeprof report -prc lakeprof_report.txt再运行 lakeprof_measurements.py 计算与补写 lakeprof 相关指标。脚本注释特别说明了为什么要进入 src 目录run_bench.shlakeprof 会通过在其当前工作目录调用lake来获取元数据因此必须从 src 目录执行 report。同样lakeprof_measurements.py 的文档字符串也强调 Must be run from the src dir so that lakeprof can collect the metadata it needs。另外lakeprof 的 report 命令以-j输出 JSON 供脚本解析lakeprof_measurements.py返回的每一行按(time, time_frac, cum_time, cum_time_frac, module)五个字段解包成Row数据结构。LAKEPROF_UPLOAD_URL可选的报告上传机制如果设置了LAKEPROF_UPLOAD_URL环境变量基准运行结束后会把 lakeprof 报告上传到该 URL 前缀README。具体实现见 lakeprof_report_upload.py未设置该变量时脚本直接退出sys.exit(0)这是默认行为上传地址为${upload_url}/${git_sha}其中git_sha由git rev-parse 在 src 目录中取得lakeprof_report_upload.py将lakeprof_report.txt的内容嵌入 lakeprof_report_template.html 模板替换__BASE_URL__与__LAKEPROF_REPORT__占位符生成index.html通过curl -fT依次上传index.html、lakeprof.log、lakeprof.trace_event三个文件lakeprof_report_upload.py。小结build 基准是 Lean 4 仓库中以编译器构建自身标准库的整体性能度量build//*描述整次构建的全局开销周期、指令、内存、时间build/profile/*与build/stat/*描述编译器各阶段的耗时与统计build/lakeprof/*描述构建系统视角下的关键路径build/module/*则逐模块刻画每个标准库文件的编译成本与产物体积。五类指标在 lean_wrapper.py、lakeprof_measurements.py 与 tests/measure.py 三个组件的配合下统一汇入measurements.jsonl形成一份可供上游持续跟踪的标准库构建性能画像。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考