lean-bench/docs/infrastructure/runner-lean435.md

Runner ubuntu24.04-x64-lean4.35 (set up 2026-10-21)

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, 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.
• Runner capacity appears to be 1: jobs from both repos queue behind each other.

What CI does

• lean-agent (.gitea/workflows/ci.yml): unit tests with the real Lean verifier, a CLI end-to-end run with a scripted provider, and a Mathlib task against lean-bench's host cache (skips if the cache is not ready).
• lean-bench (.gitea/workflows/ci.yml): python (ruff + pytest) -> lean (host Mathlib cache + docker/smoke.py with real Lean) -> image (build, smoke inside the image, keep). Triggers: push to main and ci/**, pull requests, manual. image is skipped for pull requests.
• Image kept on the host: lean-bench:latest, :main, :lean4.35, :sha-<short> (about 15 GB). latest/main are tagged only from main. Nothing prunes old sha-* tags.
• Mathlib host cache: /opt/lean-cache/leanbench-<hash of lean-toolchain+lakefile> with a .ready marker, created by .gitea/scripts/prepare-mathlib.sh under a flock. import Mathlib elaborates in about 4 s there.

Lessons

• lake exe cache get regularly drops a few of about 9,031 files ("Broken pipe" / "Connection reset"), and the same files can fail twice in a row. Retries fix it.
• 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.