Lean bisect

Skill leanprover/skills/skills/lean-bisect

Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.From its SKILL.md

Install

npx -y skills add leanprover/skills --skill lean-bisect

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

SKILL.md

2.1 KB, as published. Nobody here has run it

Bisecting Lean Toolchains

Use the lean-bisect script (in the lean4 repo at script/lean-bisect) to find which commit introduced a behavior change.

Test File Requirements

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.

Usage

# 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

Pass/Fail Determination

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.

Test File Patterns

Using exit code

axiom G : Type
axiom op : G -> G -> G

example : ... := by
  <the failing tactic call>

Using `#guard_msgs`

/--
error: the specific error that should appear
-/
#guard_msgs in
example : ... := by ...

Options

--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/

Workflow for Mathlib Issues

When the issue requires Mathlib:

Create a minimal test case
Use https://github.com/kim-em/mathlib-minimizer to produce a Mathlib-free version (see lean-mwe skill)
Run lean-bisect on the minimized file

Tips

Verify endpoints of the range show different behavior before bisecting. Keep tests fast — each bisection step runs the full test.