Diagnose and safely expand the Lean runner root filesystem #8
No Assignees
Notifications
Due Date
No due date set.
Dependencies
No dependencies set.
Reference: Zayden-Jung/lean-bench#8
Reference in New Issue
Block a user
Delete Branch "codex/runner-storage-probe"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The cloud system disk had been expanded to 150 GiB, but partition 3 and its ext4 root filesystem still occupied about 100 GiB. The main image job therefore saw only 28 GiB free and failed its unchanged 30 GiB preflight.
Add read-only storage diagnostics to env-probe, plus a manual-only root expansion workflow guarded by an explicit confirmation string, expected hostname/device/ext4 type/partition UUID/start sector/disk capacity, and an exclusive lock. The procedure backs up the partition table before growing partition 3 and the mounted ext4 filesystem. It never formats a device or deletes images/caches. Document the authorized maintenance and backup location.
The owner explicitly approved the persistent partition/filesystem change in this chat. The read-only diagnostic run #45 (API ID 442) passed, and the authorized expansion run #46 (API ID 443) passed: partition 149.8 GiB, ext4 filesystem about 148 GiB, 75 GiB available immediately after expansion. Backup: /root/lean-bench-maintenance/20261028T121919Z/nvme0n1.sfdisk. Existing images and Mathlib cache were preserved. The failed image job in main run #43 (API ID 438) passed on attempt 3 after expansion: disk preflight, image build, real Lean smoke test and image retention all succeeded. Tags latest/main/lean4.35/sha-d9389fd are present, and older sha tags were retained.
Validation: bash syntax and git diff --check passed; both remote diagnostic/maintenance workflows completed on ubuntu24.04-x64-lean4.35 runner 7. PR CI #47 (API ID 444) passed Python and real Lean verification for commit
36fd787on the same owner-confirmed runner; the image job was skipped for this PR. No local build was performed.The server maintenance already ran under explicit owner authorization from this branch. This PR only integrates the reusable diagnostics, guarded manual workflow and record into main; it does not run the maintenance on push or PR. Future maintenance requires fresh owner authorization. Review and merge manually; no automatic merge is enabled.