From 6a6543570239d16a65e7bc7f203fd845c5c54b2f Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Wed, 28 Oct 2026 20:13:32 +0800 Subject: [PATCH 1/3] ci: add read-only runner storage diagnostics --- .gitea/workflows/env-probe.yml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/.gitea/workflows/env-probe.yml b/.gitea/workflows/env-probe.yml index 53db227..75cf11b 100644 --- a/.gitea/workflows/env-probe.yml +++ b/.gitea/workflows/env-probe.yml @@ -29,3 +29,20 @@ jobs: (find / -maxdepth 4 \( -name 'lake-manifest.json' -o -name '.lake' \) -not -path '/proc/*' 2>/dev/null | head -20) || true (docker images 2>&1 | head -20) || true (docker ps -a 2>&1 | head -10) || true + - name: Read-only storage diagnosis + run: | + set -eu + hostname + lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS + findmnt -T /var/lib/docker + df -hT / /var/lib/docker + docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}' + docker system df + docker builder du 2>/dev/null || true + for dir in /var/lib/docker /var/lib/containerd /opt/lean-cache /var/cache /tmp /var/log; do + if [ -d "$dir" ]; then du -xhd1 "$dir" 2>/dev/null || true; fi + done + for tool in sfdisk growpart resize2fs xfs_growfs; do command -v "$tool" || true; done + if [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] && command -v growpart >/dev/null; then + growpart -N /dev/nvme0n1 3 || true + fi -- 2.52.0 From 96a176339277e77c1b2c2a16e18cb250a6f6d299 Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Wed, 28 Oct 2026 20:18:48 +0800 Subject: [PATCH 2/3] ci: add guarded manual root disk expansion for the Lean runner --- .../workflows/runner-storage-maintenance.yml | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 .gitea/workflows/runner-storage-maintenance.yml diff --git a/.gitea/workflows/runner-storage-maintenance.yml b/.gitea/workflows/runner-storage-maintenance.yml new file mode 100644 index 0000000..2fb786e --- /dev/null +++ b/.gitea/workflows/runner-storage-maintenance.yml @@ -0,0 +1,49 @@ +name: runner-storage-maintenance + +# Manual-only. Never runs on push or pull_request. +on: + workflow_dispatch: + inputs: + confirm: + description: Enter EXPAND_RUNNER_ROOT after owner approval + required: true + type: string + +jobs: + expand-root: + if: ${{ github.event_name == 'workflow_dispatch' && inputs.confirm == 'EXPAND_RUNNER_ROOT' }} + runs-on: ubuntu24.04-x64-lean4.35 + timeout-minutes: 20 + steps: + - name: Back up partition table and expand the authorized ext4 root + run: | + # Owner-authorized manual-only root partition/filesystem expansion. + set -euo pipefail + exec 9>/var/lock/lean-bench-root-maintenance.lock + flock -n 9 + [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] + [ "$(id -u)" = 0 ] + [ "$(blkid -s PARTUUID -o value /dev/nvme0n1p3 | tr A-Z a-z)" = 9b694bad-5bbb-4485-860f-e5544ae47410 ] + [ "$(findmnt -n -o SOURCE /)" = /dev/nvme0n1p3 ] + [ "$(findmnt -n -o FSTYPE /)" = ext4 ] + [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ] + [ "$(blockdev --getsize64 /dev/nvme0n1)" -ge 161061273600 ] + backup_dir="/root/lean-bench-maintenance/$(date -u +%Y%m%dT%H%M%SZ)" + install -d -m 700 "$backup_dir" + sfdisk --dump /dev/nvme0n1 > "$backup_dir/nvme0n1.sfdisk" + sync + printf 'Partition-table backup: %s\n' "$backup_dir/nvme0n1.sfdisk" + set +e + growpart -N /dev/nvme0n1 3 > "$backup_dir/growpart-dry-run.log" 2>&1 + probe_status=$? + set -e + if [ "$probe_status" = 0 ]; then + growpart /dev/nvme0n1 3 + elif ! grep -q '^NOCHANGE:' "$backup_dir/growpart-dry-run.log"; then + cat "$backup_dir/growpart-dry-run.log" + exit "$probe_status" + fi + resize2fs /dev/nvme0n1p3 + [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ] + lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS + df -hT / /var/lib/docker -- 2.52.0 From 36fd787c43439a0e2aac666c086127efe4f3f5fe Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Wed, 28 Oct 2026 20:21:48 +0800 Subject: [PATCH 3/3] docs: record authorized runner root filesystem expansion --- docs/infrastructure/runner-lean435.md | 29 ++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/docs/infrastructure/runner-lean435.md b/docs/infrastructure/runner-lean435.md index 87616f9..855db38 100644 --- a/docs/infrastructure/runner-lean435.md +++ b/docs/infrastructure/runner-lean435.md @@ -3,7 +3,7 @@ Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `ubuntu24.04-x64-lean4.35`. Both `lean-bench` and `lean-agent` CI run here; the old `gitea-cicd-server-for-CODEX` label is no longer used. ## The host -- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 99 GB disk (88 GB free at setup). +- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 150 GiB system disk (expanded from 100 GiB on 2026-10-28); the ext4 root filesystem reports about 148 GiB, with 75 GiB available immediately after expansion. - Lean 4.35.0 via elan 4.2.4 in `/root/.elan`. Python 3.12.3, git 2.43, gcc 13.3, curl, jq. - **No Node**, so `actions/checkout` and other JavaScript actions cannot run. Workflows clone with `git fetch --depth 1 origin $SHA` using `${{ github.token }}`. - Docker was not installed; the lean-bench `image` job installs `docker.io` + `docker-buildx` (Docker 29.1.3) if missing. @@ -20,3 +20,30 @@ Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label ` - Mathlib's post-update hook runs the cache fetch **inside `lake update`**, so retries placed after it never run. Set `MATHLIB_NO_CACHE_ON_UPDATE=1` for `lake update` and fetch in a retry loop. In the image the archives live in a BuildKit cache mount (`/root/.cache/mathlib`), so a retried build resumes. - Cold image build about 19 min; with layers cached about 2 min. - Gitea 1.26.1 has no cancel-run API; a person cancels in the web UI, then the API can `DELETE` the finished run. The Actions logs endpoint needs a token; the runs/jobs status endpoints work anonymously on this public repo. + +## Root capacity expansion (2026-10-28) + +The owner expanded the cloud disk to 150 GiB, but root partition `/dev/nvme0n1p3` +and its ext4 filesystem still occupied about 100 GiB. CI run number 43 (API run ID 438) +therefore continued to report 28 GiB available and failed its unchanged 30 GiB preflight. +Rerunning a failed job retains the same UI run number; its job attempt number increments. + +Read-only probe run number 45 (API run ID 442) confirmed the raw-disk/partition mismatch. +Its `growpart -N` output showed that partition 3 could extend from 209301471 to +314159071 sectors while keeping start sector 413696 and its partition UUID unchanged. +Temporary files and logs were small; Docker/containerd storage and Mathlib were the main +consumers. No tagged image, build cache or Mathlib cache was deleted for this repair. + +The owner explicitly authorized partition and filesystem expansion in the execution chat. +Manual maintenance run number 46 (API run ID 443) then backed up the partition table to +`/root/lean-bench-maintenance/20261028T121919Z/nvme0n1.sfdisk`, expanded partition 3, +and grew the mounted ext4 filesystem online. The resulting partition is 149.8 GiB; +`df` reported a 148 GiB filesystem with 75 GiB available. No reboot was required. + +`.gitea/workflows/env-probe.yml` now includes read-only storage and cache diagnostics. +`.gitea/workflows/runner-storage-maintenance.yml` is manual-only and requires the literal +confirmation `EXPAND_RUNNER_ROOT`. It validates hostname, root device, ext4 type, partition +UUID, start sector and disk size, takes a lock, and backs up the partition table before any +change. Future execution still requires explicit owner authorization for that maintenance. +It never formats a device or prunes images. The failed image job was retried after expansion; +its actual build, smoke-test and image-retention outcome is recorded in CI run number 43. -- 2.52.0