lean-pr

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.

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