From 52416cc2155bee1fccdf1c0458cec980b5fc61ec Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Jun 2026 12:55:44 +0000 Subject: [PATCH] chore: route submissions back to ubuntu-latest, keep chonk path dormant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue #467 (the memory-heavy Erdős unit-distance proof) is solved and recorded, so revert the temporary all-submissions-on-chonk routing back to the default hosted runner. This unblocks the pipeline from chonk availability and keeps untrusted Lean off self-hosted hardware. The chonk path stays fully wired but dormant: every self-hosted step is guarded by `runner.environment != 'github-hosted'`, so switching back is a one-line `runs-on` flip to `[self-hosted, chonk]` (documented inline). Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/submission.yml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/.github/workflows/submission.yml b/.github/workflows/submission.yml index bd2d4e5..d950735 100644 --- a/.github/workflows/submission.yml +++ b/.github/workflows/submission.yml @@ -43,14 +43,16 @@ concurrency: jobs: evaluate: if: github.event.label.name == 'submission' - # TEMPORARY: self-hosted chonk pool. Even ubuntu-latest-large (64 GB) - # SIGTERM'd (exit 143) at ~99% of issue #467's multi-hour build, hitting - # the hosted per-job memory cap. chonk has the memory headroom to finish. - # This routes UNTRUSTED submission Lean onto self-hosted hardware; it is - # acceptable only because the comparator runs inside the landrun sandbox - # (--ro /, verified by the "Probe sandbox is engaged" step). Revert to a - # GitHub-hosted runner once #467 is through. See docs/audit-archive.md. - runs-on: [self-hosted, chonk] + # Default: GitHub-hosted runner. The self-hosted chonk path is fully + # wired and dormant — every chonk-specific step is guarded by + # `runner.environment != 'github-hosted'`, so it activates automatically + # when this runs on chonk. To run a memory-heavy submission that OOMs on + # hosted runners (as issue #467's ~10k-module build did, even on + # ubuntu-latest-large, SIGTERM exit 143 at ~99%), flip THIS ONE LINE to: + # runs-on: [self-hosted, chonk] + # chonk has the memory headroom; the comparator still runs inside the + # landrun sandbox there. See docs/audit-archive.md. + runs-on: ubuntu-latest # 360 minutes is GitHub's per-job ceiling for hosted runners; set it # explicitly so genuinely long proofs run to the platform limit rather # than being cut off, and so the intended cap stays visible here.