Repository navigation
pv discharge run: the Lean comparator arm is not memory-capped (51-72 GB RSS, OOM kills runners) #4638
Closed as not planned
Description
pv discharge run (the pv discharge run (build.sh, then check --strict + comparator + leanchecker) step, ci/sections.yml) caps only the leanchecker arm in systemd-run --user --scope -p MemoryMax=<N>G (crates/aprender-contracts-cli/src/commands/discharge.rs, around line 193-215). The comparator arm, lake env lean --run scripts/Comparator.lean Challenge/*.lean, has only a wall-clock timeout, no memory cap.
Measured:
- 2026-09-27 16:14Z, gx10: one
leanreached 71.6 GB RSS and OOM-hung the host (blocked rc.1's determinism job). - 2026-09-29 fw16: kernel OOM-killed
leanat 51 GB anon RSS at 14:13Z (runnermain) and 18:36Z (fw16-3); each runner sat offline for hours because its unit had no Restart= (infra fix: forjar-declared OOMPolicy=continue + Restart=always drop-in).
Wanted: run the comparator (and Axioms.lean) through the same systemd-run --user --scope -p MemoryMax=<N>G -p CPUQuota=<Q>% wrapper as leanchecker, with a test that asserts the argv (a fixture per arm, so a third arm cannot be added uncapped). Until then the job can take down any shared runner host it lands on.
Activity
noahgift commentedon Oct 12, 2026
Status (owner aprender-4936), checked at
main9042f20: the defect is still present.In
crates/aprender-contracts-cli/src/commands/discharge.rs, only the leanchecker arm goes throughsystemd-run --user --scope -p MemoryMax=… -p CPUQuota=…(recheck_argv). Three other Lean arms spawn throughLake::run→Lake::spawn, a bareCommand::new("lake")that has a wall-clock bound and no memory cap:elaborate:lake env lean Axioms.leanself_test:lake env lean --run scripts/Comparator.lean --self-testcompare:lake env lean --run scripts/Comparator.lean Challenge/*.leanOn the PR, merge-queue and push paths the leanchecker re-check is skipped (C312) while the comparator still runs, so the capped arm is the one that does not run there.
Plan:
LakeanOption<Scope>that is built from the existing--leanchecker-memory-max-gib/--leanchecker-cpu-quota-pct/--leanchecker-unscopedflags, so there are no new flags.Lake::spawnprefixes the samesystemd-run --user --scope --slice=agent.slice -q -p MemoryMax -p CPUQuota --argv. A--scopeunit runs in the caller's process, so the pgid kill-on-timeout still holds.lake_argvbuilder for every arm, with one argv test per arm (Axioms, self-test, comparator, leanchecker), each asserting the scope prefix. An arm added without the scope then turns a test red.The branch is cut from 9042f20. The PR waits for a slot.
fix(pv): every Lean arm of `pv discharge` runs in the leanchecker's m…
fix(pv): drop two duplicate scope fields; collapse the probe if (#4638)
noahgift commentedon Oct 14, 2026
P0 to P1 (2026-10-14 P0 triage): P0 now means it blocks the next release or carries the operator's own words on it; this issue does neither, so it stays on the 0.71.0 milestone at P1.
noahgift commentedon Oct 14, 2026
Folded into #4348 as a checklist row (TRIAGE-100, 2026-10-14): the open-ticket cap is 100, so this ticket is now tracked on that master and closed as not planned. Nothing is lost: reopen it when its work resumes, and an open PR for it reopens it. Pushed branch:
fix/4638-lean-arms-scoped.Agent: aprender-clerk