# Leanbump M1 pilot: repairing real Lean projects across a Mathlib bump Eight public Lean 4 projects, each pinned to an older Mathlib, each bumped to a newer `v4.X.0` tag and repaired until `lake build` exits 0. Every number in `results.json` is produced by the compiler; every repair is a diff in `runs///`. Failures are published too. Read the result first: `python3 -I bench/results.py` prints the G1 numbers and rewrites `results.json`. ## Layout | path | what | |---|---| | `cases.json` | the 8 cases: repo, from_rev, from_tag, target tag, intermediate tags (hops), why chosen | | `lbbench.py` | harness, no model calls: `setup`, `build`, `finish` | | `env.sh` | puts elan/lake on PATH, points Mathlib clones at a local bare mirror | | `pins.py` | finds the commit of a project whose `lake-manifest.json` pins a given Mathlib tag | | `armb_context.py` | builds the "grounded context" given to arm B (enclosing declaration of each error, same-name candidates) | | `results.py` | aggregates `runs/` into `results.json` | | `runs///` | raw `errors.json`, gzipped build logs, `arm*.diff`, `arm*.json` (changes labelled rename / signature change / reproof) | | `owners.json` | public contact route of each project's maintainers | ## Arms - **A**: a plain agent session that also diagnosed the case (not blind). - **A2**: a fresh agent given only the compiler output (blind). - **B**: a fresh agent given the compiler output plus `armb_context.py` output. All arms stop at the same rule: the last `lake build` exits 0. An iteration is one rebuild after an edit batch. Repair minutes are agent session wall-clock estimates, not instrumented and not a maintainer's hours. ## Re-run one case Needs a Lean toolchain via elan (`$HOLDCO_TOOLCHAINS/elan`, see `env.sh`) and about 10 GB of disk for Mathlib caches. ```bash source bench/env.sh python3 bench/lbbench.py setup primecert # clone at from_rev, bump the Mathlib pin to the target tag python3 bench/lbbench.py build primecert # cache get + lake build; writes runs/primecert/v4.35.0/errors.json (the raw errors) cd bench/work/primecert/proj && lake build # then repair by hand or with an agent; rebuild until exit 0 cd ../../../.. python3 bench/lbbench.py finish primecert --arm A --iters 2 --minutes 12 --notes "..." # final build + diff vs from_rev python3 -I bench/results.py ``` To replay a recorded repair instead of repairing: after `setup`, run `git -C bench/work/primecert/proj apply ../../../runs/primecert/v4.35.0/armA.diff` then `python3 bench/lbbench.py build primecert --pass replay`. A green replay prints `build rc=0`. Per-tag (stepwise) runs: `setup --tag ` then `build --tag ` for each tag in the case's `hops`. ## Caveats - Raw error counts are a lower bound: Lean stops a failing module, so its dependents surface only after it is fixed. - The alias baseline counts an error as alias-fixable only if it names a deprecated declaration that has a replacement (computed by `alias_audit.py` from `api/data/alias_map.json` into `alias_audit.json`). - `diffscan.py` flags statement-text changes and deleted declarations from the diff text (lower bound: only the diff's 3 context lines are seen); each flag is classified by hand in `statement_audit.json`; unlisted flags show as `unaudited`. - Eight cases is a pilot: results are stated as "N of M", never as a rate. ## Recurring release run and case list (LEA-27) - `rerun.py [--extra] [--prune]`: model-free baseline over every case at a new Mathlib release (setup, cache, build, parse, alias join), saved after each case, written to `results..json` plus `results..diff.json` against the previous tag. Trigger: a new `v4.X.0` tag on mathlib4, checked monthly. `--prune` deletes each project's `.lake` after its result is saved (bench/work reached 60 GB). Verified on PersistentDecomp at v4.35.0 (0 errors, 9 deprecation warnings, 6 with a replacement in the map: the same as `alias_audit.json`). The full 17-case run is not done yet. - `widen.py `: the written rule for widening the list: every project the downstream-reports dashboard lists as incompatible, in the dashboard's list order, until 20 cases; none skipped. On 2026-11-07 the dashboard lists 12 incompatible projects, 3 of them already pilot cases, so the rule yields 17 cases (`cases_extra.json`, each with an owner route: the GitHub issues page; 0 verified emails). It reaches 20 when the dashboard lists more. - `humanproxy.py` -> `human_proxy.json`: for the 7 failing projects, days between a Mathlib tag release and the first project commit pinning it (46 pins, median 7 days, 12 of them 30 days or more). Elapsed days until the maintainer's repair landed, not hours of work: a proxy, not the baseline MARKET TODO 1 asks for. - `lbbench.py begin/finish` now write `ledger.jsonl` (UTC timestamps for setup, build, begin, finish), measured wall minutes, build count and, with `--tokens`, agent tokens. Runs before 2026-11-07 have none of it. - The unknown-identifier regex was wrong before 2026-11-07 (expected lowercase and quotes), so earlier `errors.json` files have `ident: null` for those errors; `alias_audit.py` classifies them by message, new runs parse them. - `pin_check.py` (LEA-29): for every pilot project commit whose Mathlib rev is a master commit (not a release tag), compares the scan's pin detection with the newest release tag that is an ancestor of that rev in the Mathlib mirror (release tags only, `v4.N.0`, not rc). Result: 179 of 179 exact (all through the lean-toolchain fallback) across 8 projects. Before the fix, a patch toolchain (v4.33.1) raised `pin_not_found` on 3 pins; `detectPin` now reads v4.N.P as release N. - `scan_vs_actual.py` (LEA-29): production matcher over each project's source at its pinned commit against the compiler's error and warning lines: flags 0 of 145 error lines, 45 of 58 deprecation warnings; 11 of 56 flagged lines in built files carry neither.