[Vilin97]

Problem

When there's no warm cache (toolchain bumps, [leanOptions] changes like #751), CI shards the whole pool across 10 runners. The planner weighted each project by Lean file count, which badly underweights certificate-heavy projects with only a few files.

In merge-queue run 42209045242 (#751, full rebuild):

shard	00	01	02	03	04	05	06	07	08	09
CPU-h (measured)	3.75	6.05	3.55	3.66	5.05	4.91	8.76	7.57	15.02	7.64
wall time	1h04	1h40	1h09	1h04	1h22	1h20	2h20	2h09	4h08	2h05

Max/mean = 2.27. Shard 08 held MovingSofa (5.8 CPU-h; its KernelOnly.PartE.Certificates.Bundle* modules take up to 865 s each) plus ConwaySoifer (4.0 CPU-h). Assemble and lint then needed ~2h more, so the run hit the 6h queue limit.

Change

• scripts/ci/build-costs.json (new): measured CPU seconds per project, the sum of Lake's ✔ … Built LeanPool.<P>… (Ns) lines from that run's 10 shard logs (329 projects, 66.0 CPU-h).
• scripts/ci/measure-build-costs.py (new, stdlib + gh): regenerates that file. Run python3 scripts/ci/measure-build-costs.py --run <id> > scripts/ci/build-costs.json on any full sharded run.
• scripts/ci/plan-build-shards.py: greedy LPT bin-packing now uses predicted cost:
  • A measured project uses its measurement.
  • An unmeasured project (new since the measurement) uses its Lean source bytes × the measured projects' aggregate seconds/byte. Estimates stay on the same scale with no constants to tune.
  • A missing or malformed cost file prints a warning to stderr and falls back to bytes. It never breaks the plan job.
  • Unchanged: shard count and the skip/single/sharded decision (still file-count based), the dirty-project path, the matrix format, and the merge-queue/mathlib-bump callers. The plan also reports shard_seconds for debugging.
• python/tests/test_build_shard_planner.py (new): log parsing (s/ms units, facet lines, single-file projects), fallback calibration, bad cost files, LPT isolating an expensive few-file project, determinism, an end-to-end cold plan on the real tree (every project exactly once, 10 shards, max ≤ 1.25× mean), and dirty-project sharded vs single.

Predicted per-shard load (current tree, cold, measured costs)

planner	per-shard CPU-h	max/mean	slowest shard (≈ CPU-h / 3.85 cores + 8 min setup)
file count (old, current tree)	5.57, 4.11, 4.24, 3.66, 13.66, 5.27, 8.28, 5.65, 7.77, 7.74	2.07	~3h40
measured cost (new)	6.61 × 9, 6.45*	1.00	~1h51

* RareSubtreePatterns merged after the measured run, so its share is estimated from size.

The 3.85 effective cores per runner and ~8 min setup are measured from the same run: each shard's summed Built seconds ÷ its build wall-clock was 3.34–3.92. A per-project critical-path check over the import graph shows no project needs longer than ~50 min end to end (HopfProblem 48 min, MovingSofa 47 min). So even the heaviest project parallelizes well within a ~1h50 shard.

Expected cold queue run: ~1h51 shards + ~2h assemble ≈ 3h55, against the 6h limit (previously 4h08 + 2h > 6h).

Why this cost source

I compared options using the measured costs as ground truth (LPT, 10 shards, current tree):

weights	max/mean
file count (old)	2.07
source bytes only	1.63
measured, bytes fallback	1.00

• Measured seconds are the only signal that sees kernel-heavy certificates. A checked-in JSON needs no network or cache access in the plan job, and since merge-queue caches aren't readable from other refs, a cache-based handoff would rarely be visible to the next cold run anyway.
• It degrades gracefully when stale. In simulation, when 10% of projects are unmeasured and fall back to bytes, the median max/mean is 1.05 (worst of 50 random draws: 1.65). At 30% unmeasured the median is 1.44. With file count as the fallback instead, the 30% case's worst draw was 2.20. Refreshing after each version bump keeps it near 1.0. That's one command, and the bump's own sharded run is a full cold build to measure from.
• I rejected the weekly profile output: /profile is per-PR, and there is no scheduled whole-pool profile.

Assemble and lint (~2h): not changed here

From the same run's finalize job:

step	time
setup + download/merge shard outputs + doc packaging	~20 min
Lint (validation_cache lint: one lake env lean --run lint-project.lean per project, sequential)	34 min
Repository quality checks (declarations/backdoors/axioms per project, sequential)	~62 min (cancelled ~2 s before finishing at the 6h mark)

Both are serial loops of single-threaded Lean processes on a 4-core runner. Running them across 3–4 workers would likely cut ~1.5h to ~30 min. That requires editing python/lean_pool/quality.py / the workflow's check steps, which CONTRIBUTING reserves for explicitly requested changes, so it's left as a follow-up. This PR alone brings cold runs within the limit.

Gates

No gate is weakened. Every project is still built in exactly one shard under the same warning check, and finalize still builds the root library and runs every check. No workflow, quality.py, linter or LeanPool/** file is touched. build-costs.json doesn't feed the build cache key (ci_cache.build_revision hashes only .lean sources), so editing it never forces a rebuild.

Testing

• uv run ruff check, uv run ruff format --check: clean.
• uv run --group test pytest: 865 passed. 4 failures (test_notice::test_repository_notice_is_current and 3 × test_proof_profile::test_stitched_logs_cannot_forge_later_file_headers) reproduce identically on unmodified main locally and are unrelated.
• No workflow changes, so actionlint wasn't needed.

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The PR appears safe to merge; no actionable new issues were found.

Summary

The PR balances CI shards using measured build times, with source-size estimates for unmeasured projects.

• Sharded builds spread projects using measured build costs.
• Operators can rebuild the cost table from CI build logs.

_{Reviews (2) · Last reviewed commit: "fix: validate shard cost inputs and pres..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "Technical source review at 61b7df1: measured weights replace file counts only for shard assignment, while the existing skip/single/sharded policy, dirty-project detection, shard-count thresholds and validation gates remain intact. I repaired malformed/nonfinite/negative and overflow handling so bad costs warn and fall back to source bytes, and made zero-cost ties preserve parallelism. Exactly two Python files changed in the repair; 23 focused tests, six end-to-end fallback probes and Ruff checks passed. Two tests requiring the full current project tree were not run locally. The checked-in table contains 329 finite positive weights; the advertised wall-time predictions and private measurement provenance are not independently established. New-head hosted CI and normal protected queue integration remain required; main is still unqualified.",
"assessment": {
"scope": "Cost-based shard scheduling, public log summarizer, measurement table and tests",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "Changes scheduling without removing build targets or checks, with safe malformed-input fallback and deterministic exact-once assignment."
},
"verdict": "approve",
"findings": []
}