evaluate OOMs on 16 GB hosted runners for memory-heavy submissions (exit 143, misleading failure comment)

[Vilin97]

Summary

evaluate on GitHub-hosted runners (16 GB) cannot complete memory-heavy submissions: the build is SIGTERM-killed (exit 143) mid-build with no Lean error, and the notify bot then closes the submission with the misleading hint that Submission.lean failed to compile. The workflow already documents this failure mode and its manual remedy in the comment above runs-on: (flip to [self-hosted, chonk], as was done for #467), but there is currently no discoverable path for a submitter to request it, and the failure message points the wrong way.

Concrete case

e8_irrep_tensor_square_decomp, submitted twice:

• [submission] e8_irrep_tensor_square_decomp — Fable-5 #1030 (run 31898182549): exit 143 at build job 8804/9423, ~2 h in.
• [submission] e8_irrep_tensor_square_decomp — Fable-5 #1077 (run 31962529479): exit 143 at build job 8762/9423, ~90 min in — after the tree had already been restructured to halve its memory peak.

Exact resource profile of the #1077 tree, measured locally on the official pin (Lean 4.33.0, cgroup MemoryMax=39 GB, swap disabled): 9,422 jobs, 4 h 13 min wall, 5 h 13 min CPU, 17.81 GB aggregate peak RSS, zero swap/OOM events, zero warnings, axioms exactly {propext, Classical.choice, Quot.sound}. That peak is irreducibly above 16 GB (single-module elaborations of large kernel-certificate files dominate it) but fits chonk and the 360-minute job cap with wide margin.

Asks

1. A supported route for memory-heavy submissions — any of: a maintainer-applied label that reruns evaluate on chonk; memory-aware routing; or documented guidance in the submission docs on how to request the big runner.
2. A more accurate failure comment when the evaluate process dies by signal (exit 143/137): distinguish "killed (likely resources)" from "Lean compile error" — the current message sends submitters down the wrong path.
3. If possible, applying the [submission] Erdős unit distance counterexample with exponent strictly greater than 1 #467 procedure to [submission] e8_irrep_tensor_square_decomp — Fable-5 #1077, which is otherwise fully green.

Happy to provide any further measurements. Thank you!

[kim-em]

Status on the three asks, after spending today on this.

1. A supported route for memory-heavy submissions. Half done. #1118 replaces the global runs-on edit with a per-issue opt-in: label an issue chonk and its evaluate job goes to the self-hosted pool, with the job timeout lifted to 720 minutes there since GitHub's 360-minute ceiling is a hosted-runner property. Labels are maintainer-only in practice, so this is a maintainer-applied label rather than something a submitter can set, which was one of the forms you suggested. The catch is that the pool it routes to is currently out of commission: a job queued against it this morning went 1 h 20 min unclaimed. So the mechanism exists and there is nothing behind it yet. I am going to look at provisioning runners with more memory.

2. A more accurate failure comment on exit 143/137. Not done, and I agree it should be. The current message sent you down the wrong path twice, which is a real cost.

3. Applying the #467 procedure to #1077. Attempted twice today, blocked both times. Details on that issue.

Worth recording here since it is the load-bearing fact: this org's ubuntu-latest-large is not a larger machine. Measured on two separate instances, it reports 4 cores, 15 GiB RAM and 3.0 GiB swap, byte-for-byte what ubuntu-latest reports. That is why #467 was killed there in June, and it means there is no hosted middle step between the default runner and self-hosted. The measurement is now recorded in the comment above runs-on so nobody repeats the experiment.

Your OOM diagnosis holds up in full. Both runs on #1077 ended at exit 143 with "the runner has received a shutdown signal", at 8804/9423 and 8762/9423 modules, around two hours into the cap, and neither log contains a Lean error, a sorry outside the benchmark's own stubs, or a disk-space failure. A memory kill takes the VM down before it can log the kill, so that signature plus your 17.81 GB measurement is as close to proof as the platform allows.