npx claudepluginhub leanprover/skills --plugin leanThis skill uses the workspace's default tool permissions.
Lean 4 publishes nightly toolchain builds from `master`. Batteries and Mathlib each have a `nightly-testing` branch that tracks these nightlies and runs CI against them. When CI passes, a `nightly-testing-YYYY-MM-DD` tag is created. When it fails, fixes are needed before the new toolchain can be adopted.
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`.
Lean 4 publishes nightly toolchain builds from master. Batteries and Mathlib each have a nightly-testing branch that tracks these nightlies and runs CI against them. When CI passes, a nightly-testing-YYYY-MM-DD tag is created. When it fails, fixes are needed before the new toolchain can be adopted.
Mathlib's nightly testing lives in a separate fork: leanprover-community/mathlib4-nightly-testing, not on the main leanprover-community/mathlib4 repo. This keeps experimental toolchain branches out of the main repository. When Lean PRs affect Mathlib, lean-pr-testing-NNNN branches are created here automatically.
nightly-testing — tracks the latest Lean nightly. CI runs here determine whether a nightly is usable.nightly-with-mathlib — points to the latest nightly that passes Mathlib CI. Lean PRs that may affect downstream should base off this branch.bump/v4.X.Y — accumulates reviewed adaptations for an upcoming Lean release. Adaptation PRs merge nightly-testing changes into this branch, and master is regularly merged in during release cycles.lean-pr-testing-NNNN — created automatically to test specific Lean PRs against Mathlib.https://leanprover.zulipchat.com/#narrow/channel/nightly-testing has up-to-date status on nightly builds, failures, and adaptation work.
The canonical reference for branch and tag conventions across lean4, Batteries, and Mathlib is: https://leanprover-community.github.io/contribute/tags_and_branches.html. If you are asked to work on nightly-testing, or lean-pr-testing-NNNN branches, you should read that page.