Stats
Actions
Tags
Help us improve
Share bugs, ideas, or general feedback.
From lean
Enforces PR conventions for leanprover/lean4 including commit message formats, changelog labels, module declarations, copyright headers, and description guidelines. Use for Lean contributions.
npx claudepluginhub leanprover/skills --plugin leanHow this skill is triggered — by the user, by Claude, or both
Slash command
/lean:lean-prThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
All PR titles must follow the format:
Guides Mathlib4 pull request conventions for leanprover-community/mathlib4, covering commit messages, workflows, labels, merge processes, and style rules. Use for PR creation and management.
Open-source pull request creation: PR descriptions, titles, fork workflows, and contribution compliance. Invoke whenever task involves any interaction with pull requests for external repositories — contributing code, opening PRs from forks, writing PR descriptions, or preparing changes for upstream submission.
Writes AI-optimized docs like README, CLAUDE.md, AGENTS.md, commit messages, PR descriptions using tables, checklists, absolute paths, invariants for cold project starts.
Share bugs, ideas, or general feedback.
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: