Repository navigation
P0: Lean/leanchecker must not overload lambda — narrow Mathlib imports, lake build vs leanchecker tiers, thread cap, no heavy kernel decide #4348
Description
Operator, verbatim, 2026-09-25: "yes to all, p0" (answering the cop's 4 proposals below). Context, verbatim: "remember this host must be able to do other work, so never let it get overloaded"
Measured 2026-09-25 07:34Z on lambda:
leanchecker ProvableContracts(pvl-a, PID 614236) used 51 threads, about 9 cores, and 58 to 60 GB RSS.- Host load was 79 on 48 cores; memory was 99 of 125 GB.
- Cause: the project does
require mathlib(5.4 GB of compiled .olean files). leanchecker reloads and re-checks the whole imported environment. Our own 237.leanfiles are a small share of that.
P0 — all four:
- Narrow the imports: no
import Mathlib. Import only the specific Mathlib modules each file needs. Receipt: RSS and wall time before and after. - Split the check tiers:
- Day to day:
lake build, which trusts Mathlib's compiled files and checks only our files. - Release gate only:
leanchecker, run undersystemd-run --user --scope -p MemoryMax=24G -p CPUQuota=800%, or on gx10 after checking disk space. - The
pv discharge check --leancheckercall sites and CI must follow this split.
- Day to day:
- Cap threads: at most 8 threads for Lean and leanchecker (
-j8/LEAN_NUM_THREADS=8or its equivalent). Make it the default in the pv wrapper. - Keep computation out of the kernel: for PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them #4347 (the NF4 table and the others), prefer
norm_num,simporrfllemmas over heavydecide. Never usenative_decide, because it adds an axiom.
Done when: a full pv discharge check --leanchecker runs within 24G and 800% CPU on lambda, and a regression guard fails if an unscoped leanchecker invocation appears in scripts or CI.
Folded sub-tickets (TRIAGE-100, 2026-10-14)
These open sub-tickets were folded here as checklist rows and closed as not planned so the open count stays at or under 100. Reopen one when its work resumes; an open PR for it reopens it.
- pv discharge run: the Lean comparator arm is not memory-capped (51-72 GB RSS, OOM kills runners) #4638 — pv discharge run: the Lean comparator arm is not memory-capped (51-72 GB RSS, OOM kills runners) (branch:
fix/4638-lean-arms-scoped)
Activity
fix(pvl): leanchecker capped by default -- <=8 threads in a 24G/800% …
fix(guard): check_leanchecker_scoped judged its own case table once t…
Merge fix/4347-prove-nf4-f16 (guard self-exclusion, #4348) into GH-4347…
fix(pvl): the leanchecker caps are ceilings -- threads/MemoryMax/CPUQ…
Merge fix/4347-prove-nf4-f16 (leanchecker caps are ceilings, #4348) i…
fold(B3): #4347 NF4+f16+DPO proofs, #4348 leanchecker caps, #4244 orp…
noahgift commentedon Sep 25, 2026
Already implemented on B3 (
fold/b3-contracts-ont-docs, PR #4317): c2efb7f, 0a79b45 (the caps are ceilings: can be lowered, never raised) and 1498cf9 (guard self-exclusion), folded at 41488ee.All four asks are covered, per c2efb7f:
import Mathlib.pv discharge check --leancheckerandrundefault toLEAN_NUM_THREADS=8inside asystemd-run --scope --slice=agent.slice -p MemoryMax=24G -p CPUQuota=800%scope.build.shrunslake buildwith 8 threads.decide +kernelwas measured light (2.15 s, 2.7 GB);native_decideis not used.Guard:
scripts/check_leanchecker_scoped.sh(a 23-row case table).Done-when receipt: full-tree
pv discharge check --leancheckerexits 0 in 162 s, with scope memory peak at the 24G cap and at most 11 threads. Before: 51 threads, 58–71 GB.Closes when #4317 lands. It carries no
Fixes #4348.docs(audit): #4348 impl receipt (car-applicable half)
roadmap: PMAT-4348 entry (car half of #4348)
docs(#4348): receipt — HeadMapping before/after + guard_tree discover…
docs(#4348): quorum 3/3 PASS @c2abfedab
3 remaining items
fix(pv): every Lean arm of `pv discharge` runs in the leanchecker's m…
noahgift commentedon Oct 12, 2026
Receipt on
main@ 03d4af1: the done-when is met, and the fix is already on main. It landed through the B3 fold (#4655) after #4317 was closed.What is on main
pv discharge check --leancheckercaps the run at 8 threads (LEAN_NUM_THREADS) inside a user scope:MemoryMax=24G,CPUQuota=800%,agent.slice. The defaults are also the ceilings.build.shexportsLEAN_NUM_THREADS=8.import Mathlibis left. The imports are narrowed to modules such asMathlib.Data.Real.Basic.scripts/check_leanchecker_scoped.shis wired throughci/sections.yml. It passes 27/27 case-table rows and scans 492 files with 0 unscoped.Measured run on the 48-core host, with the tree checked out at that sha:
build.shin aMemoryMax=24G CPUQuota=800%scope finished with rc 0 in 37.25 s, 4903 jobs, peak memory 3933M.pv discharge check crates/aprender-contracts-staging/lean --leanchecker --leanchecker-timeout 1500finished with exit 0 in 1:41.80 wall time. It printedok lake env leanchecker ProvableContracts (timeout 1500s, 8 threads, scope MemoryMax=24G CPUQuota=800%).memory.peakreached 24576M againstmemory.max25769803776, so the cap held at its ceiling.cpu.maxread800000 100000.No code is owed. Leaving the issue open for the closure call.
🤖 Generated with Claude Code
noahgift commentedon Oct 14, 2026
Done-when evidence, re-read on
main@8c3b19c8c1(2026-10-14).main@03d4af19f0. In it,pv discharge check --leancheckerexited 0 in 1:41.80. The run used 8 threads inside aMemoryMax=24G CPUQuota=800%scope. The scope'smemory.peakreached the 24G ceiling, so the cap held. The highest 1-minute load was 16.01 on 48 cores..leanfiles have 0 bareimport Mathliblines.scripts/check_leanchecker_scoped.shis still wired inci/sections.yml, with its self-test and a bare run (2 lines).Axioms.leanarms ofpv discharge runhave only a wall-clock timeout and no memory cap. The fix is onfix/4638-lean-arms-scopedand has no PR yet. It is queued for a pull-request slot.This lane does not close the issue.
🤖 Generated with Claude Code
noahgift commentedon Oct 14, 2026
Closing on evidence (cop batch call, 2026-10-14): fix landed on main through the B3 fold, PR #4655 (merged 2026-10-02, 989cb01). Done-when is met per the measured receipt on main @ 03d4af1 (2026-10-12):
pv discharge check --leancheckerexit 0 in 1:41.80, 8 threads, MemoryMax=24G CPUQuota=800% scope. Regression guardscripts/check_leanchecker_scoped.shis wired in CI; 0 bareimport Mathliblines (re-read on main @ 8c3b19c). Folded row #4638 (comparator/Axioms arms, no memory cap) is tracked in its own issue and reopens with its PR. Evidence by laya-train comments above.