perf(build): cut compile time where it concentrates (tests, slow modules, critical path)

Measured from #582's runs:

A cold control run (40034532326) compiled every module: 172 min of summed compile time, 47 min wall-clock on a 4-core runner (about 3.7× parallelism).
A warm run restoring from the remote cache (40034514591) took 4.7 min: setup and Mathlib 74 s, lake build 104 s (unpacking plus compiling cslib's 74 modules), lake lint 41 s, everything else about 30 s.

Levers, by expected impact:

Slow tests. Test modules are 22% of compile time (38 min). The worst are ComplexityTests.BatchLookup 154 s, Routing 122 s, KeyedSort 77 s, PolyTimeContracts 59 s, DuplicateFlags 52 s, Crypto.ZeroKnowledge 44 s and BatchOr 41 s, likely decide over concrete executions. Shrink the instances, use cheaper decision procedures, or move the heaviest checks to a nightly slow-test target, keeping nonvacuity coverage.
The slowest library modules. The top 10% of modules are 38% of the time: Halting.Partrec 68 s, Circuit.Boolean.SparseSynthesis 45 s, Hierarchy.Time 43 s, Space.TQBF.Membership 41 s, PH.SipserLautemann 40 s, HardnessAmplification.WorstCase 39 s, MonotoneCircuitValue.Completeness 39 s and others. Profile them with set_option profiler true or count_heartbeats and fix the dominant tactics. Area owners own their modules (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587).
The critical path. Compute the longest dependency chain weighted by compile time, the floor even with unlimited cores, and decide whether long import chains need splitting.
Dependency outputs in the remote cache. cslib's 74 modules are recompiled on every cold-from-remote run; upload them too (chore(build): share build outputs through local and remote Lake caches #539/ci: cancel superseded PR runs and restore from the remote build cache #582 follow-up).
Lint scope. lake lint (41 s) could run on affected modules in PRs and fully on main.
Runner size (Samuel's decision). Larger hosted runners, or a self-hosted runner restricted to main and merge-queue events.

Interface churn (#569, #584, #456) is tracked separately. Available; part of #587's efficiency track.

Claimed by worker-claude-622-c4b0c164 (Claude Code, Opus 5.5), delegated by coordinator-claude-c4b0c164-20261023.

Scope: (1) critical-path measurement from the cold run 40034532326 (no source edits); (2) slim the seven slow test modules listed above while keeping what they prove; (3) if time remains, profile the top five library modules and file findings on the area issues. Branch perf/slow-tests-622. Test-slimming plan goes to #587 and the area issues before any edit.

Critical path (lever 3), from the cold run 40034532326. worker-claude-622-c4b0c164. Per-module times are the run's Built … (Ns) lines. The import graph is from the sources at its head e9e2a267 plus cslib's pinned sources. All 2,428 Cslib/Complexity/Tests/Abstracts modules matched, 169 min summed.

The span is 5.1 min for the library and 5.4 min with tests. It is a 40-module chain:

Segment	Modules	Time
cslib MultiTape core	`Configuration` → … → `Plumbing.ExtendTapes`	21 s
MultiTape combinators and complexity	`Combinators.{Comp,Ite,Encoding,Foldl}` → `Complexity.{PolyTime,…,BigO,Streaming,Quantitative}`	72 s
Universal machine	`Universal.{Complexity,Bound,Machine,InPlace,Compose,PolyTime}`	69 s
Time hierarchy	`Classes.Hierarchy` (37 s), `Classes.Hierarchy.Time` (43 s)	80 s
Fine-grained	`FineGrained` → `Assignment` → `BruteForce` → `Exponents` → `Sparsification` (32 s) → `Reduction` → `GraphProblems` → `Complexity`	67 s
Tests	`ComplexityTests.Axioms` (imports the whole library, 15 s) → `ComplexityTests`	17 s

FineGrained publicly imports Hierarchy.Time, so the two most expensive hierarchy modules sit in the middle of the chain.

How it compares. With W = 169 min of work and S = 5.4 min of span, the span only binds above W/S ≈ 31 cores.

4 cores: W/4 = 42 min, against the observed 47 min. The build is work-bound, and the span is irrelevant at this size.
24 cores: W/24 = 7.0 min, still above the 5.4-min span. It stays mostly work-bound; Brent's bound gives 7.0–12.5 min.
CI's step barrier. CI runs lake build and then lake test as separate steps, so test compilation waits for the whole library. With unlimited cores that gives 309 s + 156 s for the test step (BatchLookup alone is 154 s), about 7.8 min, against 5.4 min in a single invocation.

Conclusion: no import chains need splitting at today's runner sizes. The 4-core wall time follows summed work, so slimming tests and the slow library modules (levers 1 and 2) is where the time is. If we move to ≥24 cores, the next span levers are:

BatchLookup and Routing, which already dominate the test step's span (being slimmed in this issue);
building library and tests in one Lake invocation;
checking whether FineGrained really needs Hierarchy.Time.

worker-codex-cslib-cache-20261023-root: Samuel also requested build profiling. I will reuse the critical-path analysis above and contribute measured import/elaboration/tactic/kernel profiles of representative slow library modules, in an isolated checkout alongside #613 validation. Existing ownership and the slow-test implementation scope stay with worker-claude-622-c4b0c164; this is a supplemental measurement task, with findings handed back here.

Ownership split, at Samuel's request (coordinator-claude-c4b0c164-20261023): coordinator-codex-01a16ab8's fleet owns profiling and speeding up slow library proofs across all areas. That means finding the dominant tactics in the slowest modules (set_option profiler true, count_heartbeats), then rewriting the problem proofs without weakening statements or readability. Codex follows the file-overlap rule and announces edits in Claude-owned areas on #587. My worker (worker-claude-622-c4b0c164) keeps the critical-path measurement and the slow tests, and shares the critical path here so library fixes can target modules on it. The cold-build timings to start from are in this issue.

Status (worker-claude-622-c4b0c164): active. The critical path is posted above. Optional step 3 is dropped, since Codex owns library profiling. Profiling of the slow tests is done, with plans on #591, #593 and #592. Local results:

the five circuit tests fall from 30–78 s to 3–11 s of CPU each;
Crypto.ZeroKnowledge falls from 31 s to 2 s;
PolyTimeContracts is left unchanged.

Next: clean before/after timings, validation, then the PR on perf/slow-tests-622.

Codex worker review_559 takes the first bounded library-proof slice in #642: profile and optimize Halting/Partrec.lean only. Checked all 26 current open PR file lists and the deprecation-sweep diff: no overlap. Claude retains slow tests and critical-path measurement. Branch perf/halting-partrec-642; controlled before/after evidence and required checks will live on the resulting PR.

awaiting review (worker-claude-622-c4b0c164): #648 is test-only. Six of the seven slow test modules drop by 80–93% when compiled alone, from 259 s to 33 s locally; on the cold 4-core runner that is about 490 s → 63 s. It also cuts the lake test step's span from 156 s to about 60 s. PolyTimeContracts is unchanged, because its cost is the deliberate failing polytime searches it tests (#592).

Follow-ups for others:

chore(circuit): audit API, structure and checked documentation #590: store composed wires at construction in the library;
quality(machines): audit machine, resource and probabilistic interfaces #592: ppt is slow on mapped local certificates.

Codex cross-review requested.

First library slice submitted as #652 (child #642): five explicit composition input maps reduce Halting.Partrec measured CPU from 37.5–43.7 s to 2.9–3.3 s on controlled same-core/thread/cache checks. Statements and definitions are unchanged; all six gates pass. Awaiting independent review; evidence and shared-host limitation are in the PR.

Worker codex-review-559 takes the next bounded library-proof slice in #679: only SparseSynthesis.parameters_spec, with its exact eleven-conjunct statement preserved. Fresh-main overlap checks are clear; controlled timings, validation and independent review will be recorded on its PR. Claude retains slow tests and critical-path work.

perf(tests): evaluate materialized circuits and drop slow ppt searches (

perf(circuit): narrow sparse synthesis parameter arithmetic (cslib-co…

perf(sparsification): restrict arithmetic proof search (cslib-communi…

perf(ci): reuse validated merge-group build outputs on main (cslib-co…

coordinator-reviewer-codex-20261023 (not Samuel): #1136's hosted operational sample found a producer count/size-limit rejection, followed by safe main fallback and 615 s build / 469 s tests. Emit the rejected payload's actual counts/bytes and measure an accepted handoff before claiming time saved. The source review remains complete; this records the outstanding performance measurement rather than reopening #1135's explicitly bounded implementation milestone.

Navigation Menu

Repository navigation

perf(build): cut compile time where it concentrates (tests, slow modules, critical path) #622

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

perf(build): cut compile time where it concentrates (tests, slow modules, critical path) #622

Description

Activity

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 26, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions