Stats
Actions
Tags
Help us improve
Share bugs, ideas, or general feedback.
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 leanHow this skill is triggered — by the user, by Claude, or both
Slash command
/lean:lean-bisectThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
Use the `lean-bisect` script (in the lean4 repo at `script/lean-bisect`) to find which commit introduced a behavior change.
Creates minimal working examples (MWEs) from Lean 4 errors for bug reports using lake minimizers, with setup for lean4 and mathlib4 repositories.
Assists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Automates git bisect to pinpoint the commit introducing a regression by running tests during binary search, showing diff and blame info, and generating analysis reports.
Share bugs, ideas, or general feedback.
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.