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 leanThis skill uses the workspace's default tool permissions.
All PR titles must follow the format:
Searches, retrieves, and installs Agent Skills from prompts.chat registry using MCP tools like search_skills and get_skill. Activates for finding skills, browsing catalogs, or extending Claude.
Searches prompts.chat for AI prompt templates by keyword or category, retrieves by ID with variable handling, and improves prompts via AI. Use for discovering or enhancing prompts.
Checks Next.js compilation errors using a running Turbopack dev server after code edits. Fixes actionable issues before reporting complete. Replaces `next build`.
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: