agentleFS
Sign inStart free
r-irber-irbe/proof-skills/skills/lean-pr/SKILL.md

lean-pr

Skill3 starsChanged 24 days agoApache-2.0View on GitHub

USE FOR: opening, titling, or labelling a PR against any Lean ecosystem repo (`leanprover/lean4`. DO NOT USE FOR: in-tree proof review (@lean-proof-review). TRIGGERS: PR, pull request, "open a PR", changelog label, bors.

1 other project uses a version of this.

Adopted by

Most recently taken up by

The file

Create a free account to mount
Files
SKILL.md

lean-pr

Agnostic PR-workflow contract for the whole Lean ecosystem. Upstream-specific conventions (Lean 4 core, Mathlib 4) live in references/upstream/lean4-pr.md and references/upstream/mathlib4-pr.md; this skill dispatches into them based on target repository.

Routing

  • USE FOR: any PR action against a Lean-ecosystem repo: branch-from-fork, title shaping (<type>: <subject> for Lean core, <type>(<scope>): <subject> for Mathlib), description authoring (first paragraph = changelog text), pre-flight validation (clean build, 0 sorry, 0 warnings, 0 debug probes), label selection per repo, running lake exe mk_all after Mathlib file renames, cross-linking dependent PRs via - [ ] depends on: #XXXX.
  • DO NOT USE FOR: in-tree proof review (@lean-proof-review); Mathlib-specific review checklists (references/upstream/mathlib4-review.md); writing

Workflow

  1. Pre-flight verification -- ensure local build passes cleanly via lake build. Confirm zero sorry, zero admit, zero unproven goals, and no leftover trace_state or #check probes.
  2. Pick conventions -- consult the dispatch table (Lean 4 core / Mathlib 4 / Batteries / downstream). Read the relevant references/upstream/<repo>-pr.md if unfamiliar. STOP and ask if the target repo isn't in the table.
  3. Title + description -- imperative present tense, lowercase subject, no period. First paragraph of description = changelog text, starts with "This PR ...". Skip ## Summary / ## Test plan headers -- CI and git diff carry that.

Recovery & STOP

  • Unknown target repo (not in dispatch table) -> STOP, ask which conventions apply before pushing.
  • Missing changelog-* label on Lean core feat/fix PR -> CI will block; read references/upstream/lean4-pr.md Section Changelog labels before re-pushing.
  • Mathlib CI fails after file rename -> most common cause is forgetting lake exe mk_all; re-run and amend.

Handoffs

  • Predecessors / successors: see FM handoffs. Typical inbound: @lean-build (clean local build), @lean-mwe (for upstream bug-report PRs), @lean-bisect (when filing a known-version regression), @lean-proof-review (when review green-lit a contribution). Typical outbound: @lean-proof-review (for in-tree feedback) or @lean-zettelkasten (recording PR-process lessons).
  • REDIRECT pointer: lean-pr slug routes here (preserved per Chesterton-protocol).

Detailed reference

Full encyclopedic reference, decision trees, and lookup tables live in references/lean-pr-handbook.md .

See also

  • ../../references/lean-pr-handbook.md -- Handbook Handbook
  • ../lean-gateway/SKILL.md -- Top-level skill router

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free