lean-pr

# 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