lean-pr
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
ソース情報
- リポジトリ
- leanprover/skills
- ソースの最終更新活動
- 2026年2月20日 23:06
- 検出された SKILL.md の言語
- 英語
- スター
- 72
- フォーク
- 2
インストール方法
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
ソースファイルを確認
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
SKILL.md を表示中
SKILL.md
ソースの指示 · 読み取り専用プレビュー- 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.
```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
GitHubで見る