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, 99 GB disk (88 GB free at setup).
• 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.