Skip to content

feat: add lean-bisect script for bisecting toolchain regressions #11727

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
kim-em merged 4 commits into from
Dec 21, 2025
Merged

feat: add lean-bisect script for bisecting toolchain regressions #11727

kim-em merged 4 commits into from
Dec 21, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Dec 18, 2025 •
edited
Loading

This PR adds a Python script that helps find which commit introduced a behavior change in Lean. It supports multiple bisection modes and automatically downloads CI artifacts when available.

Usage

usage: lean-bisect [-h] [--timeout SEC] [--ignore-messages] [--verbose]
                   [--selftest] [--clear-cache] [--nightly-only]
                   [file] [RANGE]

Bisect Lean toolchain versions to find where behavior changes.

positional arguments:
  file               Lean file to test (must only import Lean.* or Std.*)
  RANGE              Range to bisect: FROM..TO, FROM, or ..TO

options:
  -h, --help         show this help message and exit
  --timeout SEC      Timeout in seconds for each test run
  --ignore-messages  Compare only exit codes, ignore stdout/stderr differences
  --verbose, -v      Show stdout/stderr from each test
  --selftest         Run built-in selftest to verify lean-bisect works
  --clear-cache      Clear CI artifact cache (~600MB per commit) and exit
  --nightly-only     Stop after finding nightly range (don't bisect individual
                     commits)

Range Syntax:

  FROM..TO                Bisect between FROM and TO
  FROM                    Start from FROM, bisect to latest nightly
  ..TO                    Bisect to TO, search backwards for regression start

  If no range given, searches backwards from latest nightly to find regression.

Identifier Formats:

  nightly-YYYY-MM-DD    Nightly build date (e.g., nightly-2024-06-15)
                        Uses pre-built toolchains from leanprover/lean4-nightly.
                        Fast: downloads via elan (~30s each).

  v4.X.Y or v4.X.Y-rcN  Version tag (e.g., v4.8.0, v4.9.0-rc1)
                        Converts to equivalent nightly range.

  Commit SHA            Git commit hash (short or full, e.g., abc123def)
                        Bisects individual commits between two points.
                        Tries CI artifacts first (~30s), falls back to building (~2-5min).
                        Commits with failed CI builds are automatically skipped.
                        Artifacts cached in ~/.cache/lean-bisect/artifacts/

Bisection Modes:

  Nightly mode:   Both endpoints are nightly dates.
                  Binary search through nightlies to find the day behavior changed.
                  Then automatically continues to bisect individual commits.
                  Use --nightly-only to stop after finding the nightly range.

  Version mode:   Either endpoint is a version tag.
                  Converts to equivalent nightly range and bisects.

  Commit mode:    Both endpoints are commit SHAs.
                  Binary search through individual commits on master.
                  Output: "Behavior change introduced in commit abc123"

Examples:

  # Simplest: just provide the file, finds the regression automatically
  lean-bisect test.lean

  # Specify an endpoint if you know roughly when it broke
  lean-bisect test.lean ..nightly-2024-06-01

  # Full manual control over the range
  lean-bisect test.lean nightly-2024-01-01..nightly-2024-06-01

  # Only find the nightly range, don't continue to commit bisection
  lean-bisect test.lean nightly-2024-01-01..nightly-2024-06-01 --nightly-only

  # Add a timeout (kills slow/hanging tests)
  lean-bisect test.lean --timeout 30

  # Bisect commits directly (if you already know the commit range)
  lean-bisect test.lean abc1234..def5678

  # Only compare exit codes, ignore output differences
  lean-bisect test.lean --ignore-messages

  # Clear downloaded CI artifacts to free disk space
  lean-bisect --clear-cache

🤖 Prepared with Claude Code

@kim-em
Copy link
Collaborator Author

kim-em commented Dec 18, 2025

Sample output

$ script/lean-bisect script/lean-bisect-test.lean v4.25.2..v4.26.0 --timeout 10
From: v4.25.2 (version)
To: v4.26.0 (version)

Version v4.25.2 is on branch releases/v4.25.0
Branch releases/v4.25.0 diverged from master at 135e7e7bd390 (2025-10-20)
For FROM=v4.25.2, using nightly nightly-2025-10-20 (latest nightly before the version)
Version v4.26.0 is on branch releases/v4.26.0
Branch releases/v4.26.0 diverged from master at 8b575dcbf2a3 (2025-11-17)
For TO=v4.26.0, using nightly nightly-2025-11-18 (earliest nightly after the version)

Bisecting range: nightly-2025-10-20 .. nightly-2025-11-18 (29 nightlies)

  Testing nightly-2025-10-20... OK
  Testing nightly-2025-11-18... TIMEOUT
  Testing nightly-2025-11-03... OK

  Current range: nightly-2025-11-03 .. nightly-2025-11-18 (14 nightlies)
  Resume command: script/lean-bisect script/lean-bisect-test.lean nightly-2025-11-03...nightly-2025-11-18 --timeout 10

  Testing nightly-2025-11-11... TIMEOUT

  Current range: nightly-2025-11-03 .. nightly-2025-11-11 (7 nightlies)
  Resume command: script/lean-bisect script/lean-bisect-test.lean nightly-2025-11-03...nightly-2025-11-11 --timeout 10

  Testing nightly-2025-11-06... OK

  Current range: nightly-2025-11-06 .. nightly-2025-11-11 (4 nightlies)
  Resume command: script/lean-bisect script/lean-bisect-test.lean nightly-2025-11-06...nightly-2025-11-11 --timeout 10

  Testing nightly-2025-11-08... TIMEOUT

  Current range: nightly-2025-11-06 .. nightly-2025-11-08 (2 nightlies)
  Resume command: script/lean-bisect script/lean-bisect-test.lean nightly-2025-11-06...nightly-2025-11-08 --timeout 10

  Testing nightly-2025-11-07... TIMEOUT

  Current range: nightly-2025-11-06 .. nightly-2025-11-07 (1 nightlies)
  Resume command: script/lean-bisect script/lean-bisect-test.lean nightly-2025-11-06...nightly-2025-11-07 --timeout 10


Behavior change detected between nightly-2025-11-06 and nightly-2025-11-07

Fetching commit SHAs for these nightlies...
  nightly-2025-11-06 -> e6b1f1984c27
  nightly-2025-11-07 -> f843837bfaf4

Continuing to bisect individual commits...

Found local lean4 repo at /home/kim/lean4-2, using as reference...
Cloning to /tmp/lean-bisect-build-r4hniedl...
Cloning into '/tmp/lean-bisect-build-r4hniedl'...
remote: Enumerating objects: 34, done.
remote: Counting objects: 100% (22/22), done.
remote: Total 34 (delta 21), reused 22 (delta 21), pack-reused 12 (from 1)
Receiving objects: 100% (34/34), 6.00 KiB | 6.00 MiB/s, done.
Resolving deltas: 100% (24/24), completed with 19 local objects.
Updating files: 100% (10838/10838), done.
Found 4 commits to bisect

CI artifact download available (will try before building from source)

  Checking e6b1f1984c27... cached
    Testing e6b1f1984c27... OK
  Checking f843837bfaf4... cached
    Testing f843837bfaf4... TIMEOUT
  Checking 7459304e98ce... cached
    Testing 7459304e98ce... OK

  Current range: 7459304e98ce .. f843837bfaf4 (2 commits)
  Resume command: script/lean-bisect script/lean-bisect-test.lean 7459304e98cedfa25f7e1e1774a7bbe84ae65c00...f843837bfaf4fb64571ddced9fa4cdfde40c8610 --timeout 10

  Checking d41f39fb1066... cached
    Testing d41f39fb1066... TIMEOUT

  Current range: 7459304e98ce .. d41f39fb1066 (1 commits)
  Resume command: script/lean-bisect script/lean-bisect-test.lean 7459304e98cedfa25f7e1e1774a7bbe84ae65c00...d41f39fb1066a79c23e8c18113518c7a2bdae1e8 --timeout 10


Behavior change introduced in commit d41f39fb1066

  d41f39fb10 perf: sparse case splitting in match compilation (#10823)

  Full SHA: d41f39fb1066a79c23e8c18113518c7a2bdae1e8
  View on GitHub: https://github.com/leanprover/lean4/commit/d41f39fb1066a79c23e8c18113518c7a2bdae1e8

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 18, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 18, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4e656ea8e9273833b7cb06c720bdefbb5b9dbc87 --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-18 07:29:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 34d619bf9324e1835a3e9471b40d00a7520ada8f --onto 4e656ea8e9273833b7cb06c720bdefbb5b9dbc87. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-19 02:38:30)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 18, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4e656ea8e9273833b7cb06c720bdefbb5b9dbc87 --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force reference manual CI using the force-manual-ci label. (2025-12-18 07:29:39)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 34d619bf9324e1835a3e9471b40d00a7520ada8f --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force reference manual CI using the force-manual-ci label. (2025-12-19 02:38:32)

@kim-em kim-em changed the base branch from master to feat/build-artifact December 19, 2025 00:53
@kim-em @claude
feat: add build_artifact.py for downloading CI artifacts
2c939a4 
This script downloads pre-built CI artifacts for Lean commits from GitHub Actions.
It supports:
- Downloading artifacts for current HEAD or specified commit (--sha)
- Caching in ~/.cache/lean-bisect/artifacts/
- Platform detection (Linux/macOS, x86_64/aarch64)

This is extracted from lean-bisect to allow standalone use.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@kim-em kim-em force-pushed the feat/build-artifact branch from 68db0a3 to 2c939a4 Compare December 19, 2025 01:27
kim-em and others added 2 commits December 19, 2025 01:27
@kim-em @claude
feat: add build_artifact.py for downloading CI artifacts
593383c 
This script downloads pre-built CI artifacts for Lean commits from GitHub Actions.
It supports:
- Downloading artifacts for current HEAD or specified commit (--sha)
- Caching in ~/.cache/lean-bisect/artifacts/
- Platform detection (Linux/macOS, x86_64/aarch64)

This is extracted from lean-bisect to allow standalone use.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@kim-em @claude
feat: add lean-bisect script for bisecting toolchain regressions
a609c9a 
This adds a Python script that helps find which commit introduced a
behavior change in Lean. It supports multiple modes:

- Auto-discovery: Just provide a file and it searches backwards
- Nightly bisection: Binary search through nightly builds
- Version ranges: Convert v4.X.Y tags to nightly ranges
- Commit bisection: Search individual commits with CI artifact caching

Key features:
- Downloads pre-built CI artifacts when available (~30s vs 2-5min build)
- Caches artifacts in ~/.cache/lean-bisect/artifacts/
- Skips commits with failed CI builds automatically
- Supports short or full commit SHAs

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@kim-em kim-em changed the base branch from feat/build-artifact to master December 21, 2025 19:52
@kim-em kim-em enabled auto-merge December 21, 2025 19:58
@kim-em kim-em added this pull request to the merge queue Dec 21, 2025
Merged via the queue into master with commit b87d2c0 Dec 21, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@kim-em @leanprover-community-bot @leanprover-bot