PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions.
PR titles follow <type>(<scope>): <subject>.
Types: feat, fix, doc, style, refactor, test, chore, perf, ci
Scope is the module path with the Mathlib/ prefix stripped — e.g. Data/Nat/Basic, Topology/Constructions.
Subject uses imperative present tense, no capitalized first letter, no trailing period.
Full conventions: https://leanprover-community.github.io/contribute/commit.html
lake exe mk_all when adding or removing files (updates the import root).- [ ] depends on: #XXXX!bench on a PR to trigger performance benchmarking.Labels are added/removed via GitHub comments.
Author-managed:
awaiting-author — reviewer feedback needs addressingWIP — work in progresseasy — trivial PRs (single lemma, typo fix, <25 line diff)help-wanted, please-adopt — requesting helpTopic: t-topology, t-algebra, t-combinatorics, etc.
Downstream projects: carleson, FLT, etc.
Automated: merge-conflict is added/removed automatically when conflicts are detected or resolved.
maintainer-mergeready-to-mergeFor delegated PRs (maintainer trusts author to finalize): the author comments bors merge to trigger the merge.
The review queue is at https://leanprover-community.github.io/queueboard/ — PRs with merge conflicts or pending CI don't appear there.
Before submitting, read the relevant guides — these are the authoritative references: