Skip to content

chore: route submissions back to ubuntu-latest, keep chonk path dormant #483

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kim-em wants to merge 1 commit into
base: main
Choose a base branch
from
Open

chore: route submissions back to ubuntu-latest, keep chonk path dormant #483

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 10 additions & 8 deletions .github/workflows/submission.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading