[Amaury Chamayou (achamayou)]

Summary

Now that the Lean packages no longer depend on Mathlib (#8702), the Lean jobs that do not build CCF no longer need 1ES VMSS runners for disk space or download size. This PR moves them to GitHub-hosted ubuntu-26.04 runners, running directly on the runner image rather than in an ubuntu:26.04 container:

• the five Lean package checks (lean-package.yml, previously on gha-vmss-d16av7-ci)
• the three trace replay jobs in lean.yml (previously on gha-vmss-d16av7-ci-b)
• the Mathlib equivalence check (lean-mathlib-equivalence.yml, previously on gha-vmss-d16av7-ci)

The three trace capture jobs build CCF, so they stay on gha-vmss-d16av7-ci-c in Azure Linux containers.

Performance of the final setup, in short:

• Package checks take about 22% longer in total (1176s against 964s), because the hosted runners have 4 vCPUs instead of 16. The longest job, the consensus package check, goes from 286s to 408s.
• Replays take about the same time (111s against 97s in total).
• VMSS demand drops. Each Lean workflow run uses 8 fewer VMSS jobs, about 1060 runner-seconds, plus the Mathlib equivalence job (about 230s) when it runs. Only the 3 trace captures still use VMSS.

Results

"Hosted" is this PR, rebased on main after #8702: run 42898835830, attempt 1 (cold dependency cache) and the median of attempts 2-4 (warm). "VMSS" is the median of the 9 successful Lean runs on other PRs between #8702 merging (17:30 UTC on 10 November) and 19:00 UTC, which use main's Mathlib-free workflow through the merge ref: 42878771730, 42877971914, 42875441255, 42873405288, 42872326595, 42869599660, 42868679979, 42868511259 and 42868249176. A 10th run in that window, 42874335802, is excluded because its merge ref still included Mathlib.

All times below are job run times, from the job starting on a runner to it completing.

Run time per moved job

Job	VMSS	Hosted, cold	Hosted, warm	Warm vs VMSS
Lean package (common)	150s	210s	166s	+11%
Lean package (consensus)	286s	488s	408s	+43%
Lean package (consistency)	161s	263s	190s	+18%
Lean package (disaster-recovery)	190s	276s	232s	+22%
Lean package (kv)	177s	330s	180s	+2%
Package jobs, total	964s	1567s	1176s	+22%
Replay native CCF consensus traces	34s	34s	39s	+15%
Replay KV traces	35s	37s	38s	+9%
Replay consistency traces	28s	30s	34s	+21%
Replay jobs, total	97s	101s	111s	+14%
All moved jobs	1061s	1668s	1287s	+21%

The VMSS runs are each PR's first run, so some started with a cold dependency cache. Their "Check formatting" step, which builds leanfmt when it is not cached, took a median of 23-28s, against 5-19s on hosted warm runs and 45-60s on the hosted cold run.

The trace capture jobs, which stay on VMSS, took 132-256s on this PR and 140-284s in the VMSS runs.

Where the time goes

The package checks are slower because lake check, which builds the package and then re-checks its whole import closure in the kernel, gets fewer cores. Medians of "Build, kernel and axiom check":

Package	VMSS	Hosted, warm
common	123s	137s
consensus	229s	356s
consistency	109s	143s
disaster-recovery	114s	157s
kv	111s	130s

Setup costs about the same. The hosted runner image already has Git, a C toolchain, curl, jq and zstd, so the jobs only apt-get install elan (plus python3-jsonschema for the package checks), in 6-16s. On VMSS, the container prerequisites took 11-15s, plus container start and stop. Installing the Lean toolchain takes 11-16s on hosted runners.

Mathlib equivalence

This job runs only when the Mathlib replacements or the equivalence package change, so there are no recent VMSS runs to compare with. The VMSS figures are from #8702 (run 42703294871), which ran the same workflow.

Run	Run time	Build, kernel and axiom check
VMSS, cold (#8702, attempt 1)	275s	156s
VMSS, warm (#8702, attempt 2)	230s	158s
Hosted, cold (run 42898836306, attempt 1)	370s	204s
Hosted, warm (attempt 2)	320s	218s

Mathlib's dependency checkouts and build cache fit on the hosted runner's disk.

Changes

• lean-package.yml, lean-mathlib-equivalence.yml and the three replay jobs in lean.yml use runs-on: ubuntu-26.04 with no container, and install elan with sudo apt-get. They no longer set ELAN_HOME or safe.directory, which were only needed when running as root in a container.
• The dependency cache keys change from lean-deps-v2-vmss-ubuntu-26.04-... to lean-deps-v3-ubuntu-26.04-..., so hosted runs do not restore caches built in the containers.
• .github/workflows/README.md describes which Lean jobs use VMSS and which use hosted runners.

No Lean sources, C++ or test logic change.

Validation

• Lean workflow, run 42898835830: attempts 1 (cold) to 4 all passed.
• Lean Mathlib equivalence, run 42898836306: attempts 1 (cold) and 2 (warm) passed.
• prettier --check on the changed workflows passed, and the changed files are ASCII-only.

[Copilot]

🟢 Approval recommended

No active review issues block the Lean runner migration.

No open issues 🎉

What changed in this PR

Moves Lean jobs that do not build CCF to GitHub-hosted Ubuntu 26.04 runners, building on the Mathlib dependency removal in #8702 to reduce VMSS usage.

Changes:

• Runs package checks, trace replays, and Mathlib equivalence checks directly on hosted runners; CCF trace capture stays on VMSS.
• Simplifies prerequisite installation, removes container-only setup, and versions dependency caches for the new environment.
• Updates workflow documentation to describe the runner split.

Custom instructions used

Applied the CCF repository instructions supplied in the review context; no additional instruction files were loaded.

File	Description
.github/​workflows/​README.md	Documents hosted Lean jobs and retained VMSS trace capture jobs.
.github/​workflows/​lean.yml	Moves three trace replay jobs to hosted runners and simplifies setup.
.github/​workflows/​lean-package.yml	Migrates reusable package checks and updates their dependency cache key.
.github/​workflows/​lean-mathlib-equivalence.yml	Migrates equivalence checks and updates their dependency cache key.

_{Review effort: Balanced}