# Lean Bisect

> |

- **Type:** Skill
- **Install:** `agentstack add skill-r-irbe-proof-skills-lean-bisect`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [r-irbe](https://agentstack.voostack.com/s/r-irbe)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [r-irbe](https://github.com/r-irbe)
- **Source:** https://github.com/r-irbe/proof-skills/tree/main/skills/_overrides/lean-bisect
- **Website:** https://github.com/r-irbe/proof-skills

## Install

```sh
agentstack add skill-r-irbe-proof-skills-lean-bisect
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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

```bash
# 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

```lean
axiom G : Type
axiom op : G -> G -> G

example : ... := by
  
```

### Using `#guard_msgs`

```lean
/--
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](https://github.com/r-irbe)
- **Source:** [r-irbe/proof-skills](https://github.com/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.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-r-irbe-proof-skills-lean-bisect
- Seller: https://agentstack.voostack.com/s/r-irbe
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.