lean-pr
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
来源信息
- 仓库
- leanprover/skills
- 最近来源活动
- 2026年2月20日 23:06
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 72
- 分支
- 2
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- name
- lean-pr
- description
- PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
# Lean PR Conventions
## Commit Message Format
All PR titles must follow the format:
```
<type>: <subject>
```
**`<type>`** is one of:
- `feat` — feature
- `fix` — bug fix
- `doc` — documentation
- `style` — formatting
- `refactor`
- `test` — adding missing tests
- `chore` — maintenance
- `perf` — performance improvement
**`<subject>`**: imperative present tense, lowercase, no period.
For `feat`/`fix` PRs, begin the description with "This PR " — the first paragraph is automatically used in release notes.
## Changelog Labels
Every `feat` or `fix` PR must have a `changelog-*` label:
| Label | Category |
|-------|----------|
| `changelog-language` | Language features and metaprograms |
| `changelog-tactics` | User-facing tactics |
| `changelog-server` | Language server, widgets, and IDE extensions |
| `changelog-pp` | Pretty printing |
| `changelog-library` | Library |
| `changelog-compiler` | Compiler, runtime, and FFI |
| `changelog-lake` | Lake |
| `changelog-doc` | Documentation |
| `changelog-ffi` | FFI changes |
| `changelog-other` | Other changes |
| `changelog-no` | Do not include in changelog |
## Module System for `src/` Files
Files in `src/Lean/`, `src/Std/`, and `src/lake/Lake/` must have both `module` and `prelude` declarations. With `prelude`, nothing is auto-imported — you must explicitly import `Init.*` modules.
```lean
module
prelude
import Init.While
import Init.Data.String.TakeDrop
public import Lean.Compiler.NameMangling
```
Check existing files in the same directory for the pattern.
Files outside these directories (e.g. `tests/`, `script/`) use just `module`.
## Copyright Headers
New files in `src/` require a copyright header:
```
/-
Copyright (c) YYYY Author or Organization. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Author Name
-/
```
Check other recent files in the repository to determine the correct copyright holder. Test files (in `tests/`) do not need copyright headers.
## PR Conventions
Keep descriptions **concise**:
- Start with a paragraph beginning "This PR ..." — no section headers
- No "## Summary" header — just start with the text
- No "Test plan" section — we rely on CI
- No "Implementation details" section — the code speaks for itself
在 GitHub 查看