SK-30: Mathlib PR (REDIRECT)
This skill no longer hosts content. The generic PR workflow and the
Mathlib-specific conventions are now separated cleanly: the agnostic
workflow lives in lean-pr, and the
Mathlib-only deltas (commit format with (<scope>), labels, merge
process via bors, lake exe mk_all) live in the upstream reference.
| Old section | New home |
|---|---|
Commit message format (<type>(<scope>): <subject>) |
references/upstream/mathlib4-pr.md §Commit message format |
Workflow (forks, mk_all, depends-on, !bench) |
Same reference §Workflow |
| Labels (author-managed / topic / downstream / automated) | Same reference §Labels |
Merge process (maintainer-merge → ready-to-merge → bors) |
Same reference §Merge process |
| Style and naming URLs | Same reference §Style and naming |
| Generic agnostic PR workflow (dispatch, title shape, common ecosystem rules) | ../lean-pr/SKILL.md |
Existing inbound links to "SK-30 / mathlib-pr" should resolve here
and then follow the table above. lean-gateway/REFERENCE.md registry
row continues to resolve to this stub. Do not add new content to this
file — author it in references/upstream/mathlib4-pr.md (Mathlib-
specific) or _overrides/lean-pr/SKILL.md (generic) instead.
See also
../lean-pr/SKILL.md— agnostic Lean-ecosystem PR SKILL (parent)../../../references/upstream/mathlib4-pr.md— full Mathlib-specific content../../../references/upstream/lean4-pr.md— Lean 4 core sister reference../../../references/upstream/mathlib4-review.md— Mathlib PR review standards (sister W4 Wave 1)