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:

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.

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