为 Lean 4 仓库贡献代码：外部贡献指南、PR 流程与质量规范全解析-育师

为 Lean 4 仓库贡献代码：外部贡献指南、PR 流程与质量规范全解析

【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4

本指南以 Lean 4 仓库根目录的 CONTRIBUTING.md 为骨架，系统讲解外部开发者向 Lean 4 提交贡献（Issue、RFC、Pull Request）的完整流程：从提交前的准备工作、代码质量标准，到 PR 的撰写规范、评审与反馈机制，并延伸至与贡献密切相关的开发环境搭建、构建与测试纪律。读完本文，你将掌握 Lean 4 官方认可的贡献方式、优先级标签体系（P-high / P-medium / P-low）的含义，以及如何写出一份符合提交规范、能被维护者高效评审的 PR。

为什么 Lean 4 需要一份严格的贡献指南

在早期阶段，Lean 4 曾接受绝大多数外部 Pull Request。但这一做法带来了难以维护的代码、性能问题和大量 bug。为了提升代码库的质量与可维护性，Lean 4 团队（由 Lean FRO 管理）制定了严格的外部贡献指南，明确要求贡献者遵循一套标准化的流程。

这意味着：不是所有 PR 都会被合并。贡献者的每一项改动都需要经过 Issue 讨论、质量审查、测试验证与 CI 检查的多重把关。理解这套规则，是让贡献被高效接受的前提。

提交 PR 之前的准备：从 Issue 到 RFC

先用 Issue 讨论，再动手写代码

提交 PR 之前，永远先开一个 Issue，讨论你想解决的问题或想添加的功能。如果你是在提议一个新特性，请使用RFC:（request for comments，征求意见）前缀。先向其他用户征求反馈，并花时间汇总所有反馈——这能让维护者更高效地评估你的提案。

在创建 RFC 时，官方建议回答以下问题：

用户体验（User Experience）：这个功能如何改善用户体验？
受益者（Beneficiaries）：哪些 Lean 用户和项目最能从这个功能/改动中受益？
社区反馈（Community Feedback）：你是否向其他 Lean 用户征求过意见或见解？
可维护性（Maintainability）：这个改动是否会简化代码维护或代码结构？

了解项目、保持更新、从 help wanted 入手

理解项目：熟悉项目本身、已有 Issue 和最新提交，确保你的贡献与项目方向和优先级一致。
保持更新：定期从主分支fetch和merge最新改动，确保你的分支不过时、可以平滑集成。
Help wanted 标签：仓库中有标记为help wanted的 Issue，是官方推荐的外部贡献切入点。如果对某个 Issue 感兴趣，可以在其中留言、提问，并与核心开发者互动。

与贡献相关的开发环境准备

CONTRIBUTING.md指向的开发环境文档给出了完整的本地搭建流程。由于 Lean 4 是自举（bootstrapped）编译的程序——前端和编译器本身用 Lean 编写——贡献者需要理解其多阶段构建模型（详见 doc/dev/bootstrap.md）：

stage0使用仓库中检入的预编译 C 源文件构建，是一个"黑盒"引导二进制；
make默认构建stage1，用stage0/bin/lean编译含你改动的src/库，再链接成stage1/bin/lean；
修改.olean格式等"元层"代码时，需要继续构建stage2，而stage3仅作为一致性检查存在。

因此，任何可能影响 Lean 自身编译的改动（如 parser、elaborator、compiler）都必须先阅读 bootstrapping 文档，且不得直接编辑stage0目录，除非按该文档描述的特定命令操作。

推荐使用elan切换 toolchain（仓库根目录的lean-toolchain文件已配置好lean4-stage0用于src、lean4用于tests）：

elan toolchain link lean4 build/release/stage1 elan toolchain link lean4-stage0 build/release/stage0

VS Code 用户可直接在仓库根目录执行code .，仓库内置的.vscode/会配置好设置、任务与推荐扩展。另外建议安装ccache加速生成 C 代码的重新编译。

质量优先（Quality Over Quantity）

指南明确将"质量优于数量"作为核心原则，体现在三点：

专注的改动（Focused Changes）

每个 PR 应只解决一个明确界定的 Issue 或特性，避免把多个不相关的改动塞进同一个 PR。这既方便评审，也便于在出问题时定位和回滚。

写测试（Write Tests）

每个新特性或 bug 修复都应附带相关测试，以保证贡献的健壮性和可靠性。Lean 4 的测试套件结构分为两种：

测试目录（test directory）：包含run_test.sh和/或run_bench.sh脚本的目录，代表单个测试或基准测试；
测试堆（test pile）：同样包含运行脚本的目录，但目录中每个指定扩展名（通常是.lean）的文件各代表一个测试或基准测试，运行脚本会为每个测试文件各执行一次。

测试目录按用途划分：compile（编译并执行、同时走解释器验证输出）、elab（只展开不执行）、elab_fail（期望退出码为 1）、server/server_interactive（测试 LSP 请求）、lake（Lake 构建工具的测试，相对独立）等。写测试时可以借助fix_expected.py生成.out.expected文件，并用lint.py做规范检查。

更新文档（Documentation）

更新相关文档，包括代码中的注释，解释你改动的逻辑与理由。注意：Lean 自身的src/Lean子模块都使用prelude关键字（见 doc/dev/index.md），与普通 Lean 项目不同，改动Init时不会强制触发Lean的完整重建——理解这一约定有助于你正确组织导入。

编码规范（Coding Standards）

遵循代码风格（Follow the Code Style）：确保代码符合项目既有风格。仓库的代码风格约定可参考 doc/style.md 与 doc/std/style.md。
善用 Lean（Lean on Lean）：充分利用 Lean 的内置特性和标准库，避免重复造轮子。例如src/Init、src/Lean、src/Std中的既有抽象与库函数。
性能（Performance）：确保改动不引入性能回退，并尽可能针对速度和资源占用做优化。可借助 tests/bench、tests/compile_bench、tests/elab_bench等基准目录验证性能影响（TEST_BENCH环境变量用于区分测试与基准场景）。

PR 提交规范（PR Submission）

描述性标题与摘要

PR 标题应简明说明 PR 的目的；摘要需给出更详细的改动内容与原因。不允许以 Zulip 讨论串链接作为摘要——你有责任自行总结讨论内容并获得支持。

遵循提交规范（Commit Convention）

PR 采用squash merge，最终提交信息取自 PR 的标题和正文，因此二者必须遵循提交规范。该规范基于 AngularJS 项目的约定，格式为：

<type>: <subject> <空行> <body> <空行> <footer>

<type>必须是：feat（特性）、fix（bug 修复）、doc（文档）、style（格式）、refactor（重构）、test（补充测试）、chore（维护）、perf（性能优化）；
每个feat或fix提交都必须带有changelog-*标签，且提交信息以 "This PR " 开头，以便进入 changelog；
<subject>：使用祈使句、现在时（"change" 而非 "changed"/"changes"），首字母小写，结尾不加句号；
<body>：同样使用祈使句现在时，说明改动动机并与旧行为对比；若带changelog-*标签，正文必须以 "This PR " 开头；
<footer>可选，用于标注破坏性变更（Breaking changes，需描述改动、理由与迁移说明），以及引用关闭的 Issue，例如Closes #123, #456。

因为改动最终会被 squash，分支上的提交历史与提交信息无需刻意打磨；但应把不想进入最终提交信息的问题和补充信息放到首个评论中，而不是 PR 描述里。

链接相关 Issue

在 PR 中引用其解决的 Issue，为评审提供上下文。

AI 贡献声明

任何由生成式 AI 协助完成的贡献，必须在 PR 描述中注明。作者有责任在打开 PR 前手动检查这些贡献；完全由 AI 单独撰写的 PR 不受欢迎，可能被直接关闭且不做进一步说明。

保持响应（Stay Responsive）

PR 提交后要保持响应，准备好按反馈修改。超过一个月无回应或更新的 PR 将被关闭。

评审与反馈机制（Reviews and Feedback）

lean4 仓库由 Lean FRO 的triage 团队管理，目标是每周对新的 bug 报告、PR 和 RFC 提供初步反馈。反馈通常体现为给工单分配以下优先级之一：

标签	含义
`P-high`	我们会处理这个 Issue
`P-medium`	有时间的话我们可能会处理
`P-low`	我们暂不计划处理
closed	已修复、不是问题，或与项目路线图不符，不会处理也不接受外部贡献

对于bug 报告，所列优先级反映的是修复该问题的承诺，通常与处理该 bug 的外部贡献所能获得的优先级相近但不完全等同；
对于PR 和 RFC，优先级反映的是评审并将其推进到可接受状态的承诺；被接受的 RFC 会打上RFC accepted标签，随后像 bug 报告一样被分配新的"实现"优先级。

与评审互动时遵循三条原则：

保持耐心（Be Patient）：全职维护者数量有限、PR 数量大，评审可能需要一些时间；
建设性沟通（Engage Constructively）：以积极、建设性的态度对待反馈，评审是为了保证项目质量，而非针对个人；
通过 CI（Continuous Integration）：确保 PR 上所有 CI 检查通过，失败的检查会拖延评审——维护者不会检查包含失败项的 PR。

你会得到什么（What to Expect）

并非所有 PR 都会被合并：我们感谢每一份贡献，但只有与项目目标、质量标准一致的改动才会被合入；
反馈是礼物（Feedback is a Gift）：评审反馈既能改进项目，也能帮助你作为开发者成长；
社区参与（Community Involvement）：在 Lean 社区的沟通渠道中保持互动，有助于更好地协作并理解项目方向。

贡献前的自检清单

综合全文，正式提交 PR 前建议逐项确认：

已先开启 Issue 或RFC:讨论并获得反馈；
分支基于最新 master，无冲突；
改动聚焦单一问题，包含测试（tests/ 下合适的目录或测试堆）；
文档与代码注释已同步更新；
遵循代码风格、使用 Lean 内置能力、无性能回退；
PR 标题与描述符合提交规范，带changelog-*标签与 "This PR " 开头（如适用），并在 footer 中Closes #xxx；
引用了相关 Issue，AI 协助已在描述中注明；
本地 CI 全部通过，且未触碰stage0（除非按 bootstrap.md 流程操作）；
提交后保持响应，避免超过一个月无更新。

遵循以上流程，你的贡献将能以最高效的方式进入 Lean 4 这一自举编译器/证明助手的代码库，并被src/kernel、src/Lean、src/Init、tests/等目录的既有代码风格所认可。

【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4

创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考

为 Lean 4 仓库贡献代码：外部贡献指南、PR 流程与质量规范全解析