// PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
Set up a lean4 repository clone with proper elan toolchains.
Building Mathlib
PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions.
| 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. |
All PR titles must follow the format:
<type>: <subject>
<type> is one of:
feat — featurefix — bug fixdoc — documentationstyle — formattingrefactortest — adding missing testschore — maintenanceperf — 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.
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 |
src/ FilesFiles 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.
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.
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.
Keep descriptions concise: