lean-bisect

name	lean-bisect
description	Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.

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