docs: record authorized runner root filesystem expansion

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.