[Vilin97]

Problem

The LLM review workflow dies on very large PRs: on #278 (73k-line import) lean_pool.review.request_review crashed with

openai.BadRequestError: Input tokens exceed the configured limit of 922000 tokens.
Your messages resulted in 1556823 tokens

so the PR's review gate never ran. #124 hit the same failure earlier. review.py sent the whole diff unconditionally.

Fix

review.py now fits the diff to a token budget before calling the model, and degrades gracefully instead of crashing:

• Upfront estimate at 2.0 chars/token — the worst density actually measured (computed from Import Erdos97ConvexOctagon: convex-octagon case of Erdős Problem 97 #278's own rejection: 3,112,190 chars ÷ 1,556,823 tokens ≈ 2.0; its machine-generated interval arithmetic tokenizes ~2× denser than ordinary Lean) — against an 800k-token budget under the observed 922k limit.
• Largest-first elision: over budget, the biggest per-file patch bodies are replaced with [elided by lean-pool llm-review: N of M patch lines omitted …] markers, keeping every file's path, patch line counts, and opening lines (for added Lean files that's the copyright header, module docstring, and imports — the most review-relevant part). If eliding everything still overflows it refits with minimal heads, then hard-cuts the tail as a guaranteed last resort.
• Truncation is disclosed twice: a ## Diff size notice section tells the model what was elided (and to say so in its summary), and the posted comment gets a deterministic > ⚠️ Partial review — diff exceeded the size budget banner.
• Shrink-and-retry: the estimate is approximate by nature, so if the API still rejects the input as too large, the diff budget is halved and the request refitted and retried (up to 2 times) rather than failing the run. Non-overflow 400s still raise.

Contract intact: sticky <!-- lean-pool-llm-review --> marker, comment format (unchanged byte-for-byte when no truncation), and **Reviewed head:** SHA keying are untouched; no gating semantics change and .github/workflows/llm-review.yml is not modified. Infra-only — touches python/ exclusively.

Validation

Replayed the production fit on #278's actual diff: 43 of 317 file bodies elided, 3.11M → 1.57M chars, projecting to ~789k input tokens at that PR's measured density — under the 922k limit, with the other 274 files still reviewed in full and all 317 paths visible.

Tests: 7 new pytest cases (untouched-under-budget, largest-first elision with path/head/count preservation, hard-truncate backstop, overflow→refit retry against a fake client, unrelated-400 re-raise, comment banner, no banner when untruncated). Enabling them surfaced that tests/test_review.py and tests/aggregator/test_triage.py each registered a competing openai stub via sys.modules.setdefault — whichever loaded first won, and the triage one lacked BadRequestError — so the stub is consolidated into one canonical tests/conftest.py mirroring the real exception hierarchy.

uv run ruff check, uv run ruff format, and uv run --group test pytest all pass (186 tests).

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.