lean-pr
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
Source facts
- Repository
- leanprover/skills
- Last source activity
- February 20, 2026 at 23:06
- Detected SKILL.md language
- English
- Stars
- 72
- Forks
- 2
Install options
The review-first prompt is selected by default. You can switch to a direct command or download a local copy.
Review the source files
Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.
Showing SKILL.md
SKILL.md
Source instructions · Read-only preview- 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
View on GitHub