# 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.