From lean
Bisects Lean 4 toolchain commits to identify regressions or behavior changes using self-contained test file signatures. Useful for Lean 4 debugging.
npx claudepluginhub leanprover/skills --plugin leanThis skill uses the workspace's default tool permissions.
Use the `lean-bisect` script (in the lean4 repo at `script/lean-bisect`) to find which commit introduced a behavior change.
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`.
Use the lean-bisect script (in the lean4 repo at script/lean-bisect) to find which commit introduced a behavior change.
Test files must be self-contained with no Mathlib imports (Mathlib is pinned to specific toolchains and will fail on most versions tested). See the minimization skill if you need to reduce a Mathlib test case to a standalone one.
# Auto-find regression
script/lean-bisect /tmp/test.lean
# Bisect up to a given nightly
script/lean-bisect /tmp/test.lean ..nightly-2024-06-01
# Between nightlies
script/lean-bisect /tmp/test.lean nightly-2024-01-01..nightly-2024-06-01
# Between commits
script/lean-bisect /tmp/test.lean abc1234..def5678
# With timeout
script/lean-bisect /tmp/test.lean --timeout 30
The script compares a "signature" of exit code + stdout + stderr. It bisects to find where this signature changes. Use --ignore-messages to only consider exit code.
axiom G : Type
axiom op : G -> G -> G
example : ... := by
<the failing tactic call>
#guard_msgs/--
error: the specific error that should appear
-/
#guard_msgs in
example : ... := by ...
--timeout N: Timeout in seconds per test--ignore-messages: Only compare exit codes--nightly-only: Only test nightly releases when bisecting commits--selftest: Verify the script works--clear-cache: Clear ~/.cache/lean_build_artifact/When the issue requires Mathlib:
lean-mwe skill)Verify endpoints of the range show different behavior before bisecting. Keep tests fast — each bisection step runs the full test.