Lean Bisect

lean-bisect

> Vendor-origin skill (mirrored from vendor/leanprover-skills/skills/lean-bisect); > this override v2-wraps it so dispatch agents can route to it under the same > contract as first-party skills.

Routing

• USE FOR: running script/lean-bisect on a self-contained Lean test file to identify the Lean 4 commit or nightly that introduced a behaviour change; comparing exit-code + stdout + stderr signatures across a commit range; isolating regressions in tactic behaviour, elaborator output, panic conditions, or build success.
• DO NOT USE FOR: building any Lake project (use @lean-build); reducing a Mathlib-dependent failure to a self-contained repro (use @lean-mwe first; bisect operates on standalone files); writing the proof or repairing the failure itself (use @lean-proof); filing the upstream bug report after the culprit commit is known (use @lean-pr).
• TRIGGERS: bisect, regression, "which commit broke", "behaviour changed between nightlies", nightly bisect.

Workflow

1. Prepare — confirm the test file is self-contained (no Mathlib imports). If Mathlib-dependent, hand off to @lean-mwe first to produce a standalone repro. STOP otherwise.
2. Verify endpoints — manually run lake env lean (or bare lean for vendored toolchains) on the failing version and the known-good version. Confirm they show different behaviour before starting the bisect.
3. Bisect — script/lean-bisect /tmp/test.lean with the appropriate --timeout. Use --ignore-messages if only exit code matters; use #guard_msgs to capture exact diagnostics; use --nightly-only to keep cycles bounded across long ranges.
4. Report — record the culprit commit + signature change in a Zettelkasten note (@lean-zettelkasten) and hand to @lean-pr if upstream filing is warranted.

Recovery & STOP

• Same signature on both endpoints → STOP, the test does not discriminate; redesign before bisecting.
• Mathlib import re-appears after minimisation → STOP, route back to @lean-mwe; lean-bisect cannot test versions where the Mathlib toolchain pin doesn't match.
• Timeout exhaustion (3 consecutive --timeout increases without resolution) → STOP, the test is too slow; reduce or isolate further.
• Cache corruption signals (impossible signature, ghost regressions) → run script/lean-bisect --selftest then --clear-cache; re-attempt once before escalating.

Handoffs

• Predecessors / successors: see FM handoffs. Typical inbound: @lean-mwe (after Mathlib-free repro) or direct from @lean-proof (when the operator already has a standalone file). Typical outbound: @lean-pr (upstream report) or @lean-zettelkasten (record the pattern).
• Sister skill: @lean-mwe — usually chained before bisect.
• Source notes: vendor mirror at vendor/leanprover-skills/skills/lean-bisect/SKILL.md.

---

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
  

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:

1. Create a minimal test case
2. Use https://github.com/kim-em/mathlib-minimizer to produce a Mathlib-free version (see lean-mwe skill)
3. 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.

Host-repository context: when bisecting a regression from a downstream repository, preserve the tactic family and diagnostic shape that triggered the failure so the isolated test stays faithful. Test files must have no sorry unless testing sorry-specific elaboration behavior.

---

See also

• [../../../references/lean4-module-dependency-guide.md](../../../references/lean4-module-dependency-guide.md) — Layer discipline and cycle detection (debugging build cycles)
• [../../../references/upstream/lean-bug-report-pipeline.md](../../../references/upstream/lean-bug-report-pipeline.md) — Shared 5-stage bug-report pipeline (repro → guard → minimise → bisect → file) and lean-mwe ↔ lean-bisect hand-off contract
• [../lean-mwe/SKILL.md](../lean-mwe/SKILL.md) — Sister skill for MWE construction (typically chained before bisect)

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: r-irbe
• Source: r-irbe/proof-skills
• License: Apache-2.0
• Homepage: https://github.com/r-irbe/proof-skills

Install and usage instructions live in the source repository linked above.