ix catalog at corpus scale - #584
Merged
Merged
Conversation
…gates The catalog depended on importModules' *default* level for D6 "complete bodies, unconditionally". An OLeanLevel.exported env axiomizes imported proofs and drops `_private.*` constants; kernel replay accepts the axioms vacuously and `--audit` compares two identically-axiomized legs (#572 documents this shipping in #569 and hiding until tc-pins/tc-accel-diff), so no existing gate could catch a level regression. - `level := .private` is now explicit at both importModules call sites (member load in resolveLibs, toolchain base in buildCatalog). - `lake test -- catalog` now asserts on the built union that the toolchain base keeps theorem proofs (`Nat.add_comm` is a thmInfo) and its `_private.*` constants. - `lake test -- --ignored catalog-fixtures` gains a loader-level test on member A's env: imported theorem present with a closed proof, module-mode member theorem keeps its proof, `@[no_expose]` loads as a transparent defn, `_private.*` constants present. Catalog-scale plan Item 4 (acceptance I4).
A member X's import closure may reach a module of cataloged package
Y that Y's own declared roots do not reach (a provider's umbrella
need not import every module a downstream member uses — real corpus
case: a member directly importing a ProofWidgets demo module the
umbrella skips). ownershipMaps renames that module's constants, but
replay only delivers the closures of declared roots, so nothing
replays them and the kernel rejected X's first reference with a bare
`unknown constant P.Y.N`.
buildCatalog now folds a covered-module set over members in
declaration order and rejects, before any replay, a foreign cataloged
module nobody delivers — naming the member, the module, and the
owning qualifier, with the fix ("Add M to Q's roots"). A provider
listed after its consumer is distinguished as a spec ordering error.
Two catalog-fixtures tests trigger each flavor against narrowed and
misordered specs over the existing fixture pair.
Catalog-scale plan Item 5 (acceptance I5).
resolveLibs loaded every member environment up front and buildCatalog
held the whole array live through replay. A member env is the
transitive import closure of its roots, so at corpus scale (~81
members, ~40 sharing a mathlib closure) peak memory is ~40× a
mathlib env. The intended bound (plan DQ5) is: toolchain base +
growing target env + one source env at a time.
The catch: dropping an Environment does NOT release its compacted
olean regions — freeing is explicit (Environment.freeRegions) and
only sound when nothing references region memory — while
relocateExpr deliberately SHARES unchanged subterms with the source
env and kernel addDecl stores them in the target.
The replay path now stages each member through a fused rename +
total structural copy (relocExprC and friends): every object
reachable from a staged Declaration — exprs, names, levels, strings,
big literals, mdata — is rebuilt on the ordinary heap, pointer-cached
per member so the source DAG's sharing survives the copy. forEachLib
streams members in declaration order (import at .private → resolve
packages → callback → freeRegions); the toolchain base imports once
after the pass (its regions live on in BuildResult.consts); the
staged declarations kernel-replay afterwards. auditCatalog streams
the same way — its standalone-vs-catalog address comparison doubles
as a copy-fidelity gate. resolveLibs and replayLib dissolve into
forEachLib and stageLib.
Two sharp edges found as segfaults in kernel sharecommon/defeq over
freed regions, both now permanently guarded:
- The code generator eta-reduces a match arm that rebuilds a
constructor from unchanged scrutinee fields into returning the
ORIGINAL (region-resident) object. Expr.bvar, SourceInfo.synthetic,
DataValue.ofBool, ReducibilityHints.regular all bit — ofBool even
through an if/then/else rebuild. All-scalar reconstructions now
route one field through copyNat-style arithmetic the simplifier
cannot fold, and relocExprC/copyDataValue/copyMData self-check with
ptrAddrUnsafe panics, so a future codegen change fails loudly at
staging time instead of corrupting memory after the free.
- { val with … } record updates silently share boxed fields
(DefinitionVal.hints).
Under streaming the package → qualifier map is incremental
(dependencies-first makes it complete for each member's closure), so
the I5 unknown-provider diagnostic folds the uncatalogued and
misordered cases into one error; covered-module names, toolchain
module names, and PkgId keys are copied out of region memory.
Gates: catalog / catalog-qualified / import-ixe / --ignored
catalog-fixtures (C1 audit = address equality between sparse
standalone and total-copied catalog compiles) and lake build ix all
green.
Catalog-scale plan Item 1 (acceptance I1).
The CatalogReal workspace still pinned pre-v4.33 batteries/aesop revs (and v4.29 lean-toolchain files, here and in the Catalog fixture pair); batteries at the old rev no longer compiles on v4.33, so the ignored benchmark has been unbuildable since the #572 consolidation. Bump batteries and aesop to the revs mathlib v4.33.0 inherits (the same revs Benchmarks/Compile and the TruthMines corpus pin); haskell-spec already matches TruthMines. The #569-era baselines (19,584 owned / 208,583-const union / 521,723,740 B) belong to the old pins; refreshed baselines on this box: 20,117 owned constants, 18,715 replayed, 146,987-const union, 360,552,416 B at root fb0640061a61….
Benchmarks/CatalogReal (batteries + aesop + haskell-spec) exposed two more paths that rode region pointers into staged declarations — both crashed as kernel-side segfaults over freed regions, invisible to the small fixture corpus: - Array.mapM's unsafe implementation returns the INPUT array object when the array is empty, and empty `Syntax.node` args arrays are common in `DataValue.ofSyntax` mdata. copySyntax now rebuilds args with an explicit push loop. (Lists are immune — `[]` is a tagged scalar, not a heap object.) - The remaining copiers (strings, names, levels, substrings, source info, preresolved, syntax) gain the same ptrAddrUnsafe self-check panics that already guard relocExprC/copyDataValue/copyMData, so any future pass-through — compiler eta or library fast path — fails loudly at staging time instead of corrupting kernel replay. With this, `ix catalog` over the refreshed CatalogReal pins streams all three members and compiles clean: 20,117 owned constants, 18,715 replayed, 146,987-const union in 21.2 s, 360,552,416 B at root fb0640061a61….
`Qualifier=Root[,Root…]` positionals across a corpus-scale member
list make an unwieldy argv. `ix catalog --spec spec.json` takes the
same information as JSON:
{ "prefix": "TruthMines",
"libs": [ { "qualifier": "Batteries", "roots": ["Batteries"] } ] }
Parsing lives in the library (`Ix.Catalog.specFromJson`, unit-tested
in `lake test -- catalog` — CLI modules only build under the exe
build) and is fail-closed on structure: unknown keys error, and the
`groups` key is reserved for grouped loading (plan Item 2) so a
future-format spec fails loudly instead of silently flattening.
--spec is mutually exclusive with positional libs and --prefix (the
file carries the prefix); the resolved spec and the spec-file path
are echoed into --report.
Verified equivalent on Benchmarks/CatalogReal: the --spec build is
byte-identical to the positional build (root fb0640061a61…).
Catalog-scale plan Item 3 (acceptance I3).
--audit is N+1 full compiles; at corpus scale that is a multi-hour session, not a routine gate. `--audit-only Qual[,Qual…]` (implies --audit) runs the anon-address invariant on just the named members — a rotating subset keeps the gate viable — while the artifact is still built and written. Members outside the subset still stream through the loader (their packages extend the qualifier map) but skip the standalone compile and compare. Qualifiers are validated against the spec up front; the report records `auditedQualifiers` (all members, the subset, or null when no audit ran). The report also gains `peakRssBytes` — the process-tree VmHWM via the existing TracingTexray sampler (Linux-only, 0 elsewhere) — so catalog runs self-report the measurement downstream previously shelled out to `time -f %M` for, and the spine benchmark can gate on it. Fixture test: an audit restricted to member `B` checks strictly fewer constants than the full audit, with zero violations. Catalog-scale plan Items 6 and 7 (acceptance I6, I7).
The mathlib-spine benchmark OOM-panicked the streaming loader at ~112 GiB RSS (and 1M mappings — vm.max_map_count) while staging the Mathlib member. Root cause is a scaling fact, not a bug: olean compaction dedups only WITHIN a module, so cross-module pointer sharing in a member env is essentially zero (measured pointer-cache hit rate over batteries: ~16%), and a purely pointer-cached copy materializes the member's entire syntactic content — ~30M nodes for batteries, extrapolating to ~10⁹ nodes ≈ 100 GiB for mathlib. The copy is now hash-consed: children are interned before their parents, so structural equality of a candidate is SHALLOW (head constructor + pointer-equal children + equal scalars) and the cached hash fields on Expr/Level/Name make interning O(1) per node. Strings intern by value; fvar/mvar/mdata nodes are not interned (rare in kernel content, no cheap shallow form). Intern tables key on the copies themselves, never on region objects, so they survive freeEnvRegions. Footprint drops to the member's structurally-unique content, and replay gets faster (kernel sharecommon receives pre-shared input): CatalogReal build 18.6 s → 15.9 s, artifact byte-identical (root fb0640061a61…).
… hybrid, unconditional replay Three walls found by the mathlib-spine leg (a member owning 569,200 constants), each fatal on a 124 GiB box: - The source-pointer caches grew with the member's total VISITED content (~10⁹ nodes ≈ 50 GiB of 64 KiB small-object pages; the process also hit vm.max_map_count). They now reset per declaration: intra-declaration DAG sharing keeps the walk linear, and cross-declaration repeats collapse at the persistent intern tables node by node. - Even hash-consed, materializing a mathlib-scale member's owned content as heap objects measures ~10× its compacted-region form (>100 GiB peak). A member owning more than copyStageMaxOwned (default 100,000) constants is now staged SHARING its env's regions, which stay mapped (EnvDisposal.keepRegions, threaded through forEachLib) — one kept mathlib env is ~8 GiB of regions. The corpus shape is exactly the favorable case: many small-content members with heavy CLOSURES (copy + free) and a handful of heavy-content members (keep + share). Fixture test: threshold-0 (all shared) and default (all copied) builds produce identical roots; CatalogReal stays byte-identical (root fb0640061a61…). - Replay passed empty Options to Kernel.Environment.addDecl, so the default maxHeartbeats applied — mathlib's heavy proofs (WeierstrassCurve.Projective.addX_neg) were rejected with a deterministic timeout. Latent since #569: elaboration-time set_option overrides never reach the replay. Replay now runs with maxHeartbeats 0 — the declarations were already accepted once. Spine baseline leg (mathlib + its dependency spine, 590,748 owned): 119 GiB OOM panic → completes at 32.2 GiB peak — 580,510 declarations replayed into a 774,528-constant union in ~17 min, 3,332,486,766 B artifact at root 6e8bd09c14c6….
Benchmarks/CatalogSpine: mathlib's dependency spine + Mathlib + three small real-corpus mathlib dependents (BET, GibbsMeasure, KolmogorovExtension4) whose environments each contain the full mathlib closure — the shape CatalogReal cannot exhibit (its members barely share closures), and the shape that found four scaling walls in the streaming loader (see the preceding commits). Revs are the TruthMines corpus pins (Lean v4.33.0). `lake test -- --ignored catalog-spine` runs a baseline leg (mathlib + its spine) and the full-spine leg as ix subprocesses via --spec/--report (dogfooding I3/I7) and asserts the spine peakRssBytes stays under 1.6× the baseline: members sharing the already-cataloged heavy closure must stream through without multiplying the peak. Pre-streaming resolveLibs held every member env simultaneously — three extra mathlib environments put the ratio far above the gate (and pre-hybrid the leg OOM-panicked outright). Numbers on the 124 GiB box: baseline (9 members, 590,748 owned) 580,510 decls → 774,528-const union in ~17 min, 3,332,486,766 B at root 6e8bd09c14c6…, peak 32.2 GiB; full spine (12 members) 580,927 decls → 774,963-const union, 3,334,313,087 B at root 3825539457d6…, peak 35.3 GiB — ratio 1.10×. First run needs network and `lake exe cache get`; needs `lake build ix` first. Catalog-scale plan Item 8 (acceptance I8).
johnchandlerburnham
force-pushed
the
jcb/catalog-scale
branch
from
August 21, 2026 09:27
7dc6dac to
80a552a
Compare
johnchandlerburnham
enabled auto-merge
August 21, 2026 09:42
arthurpaulino
approved these changes
Aug 21, 2026
arthurpaulino
left a comment
arthurpaulino
left a comment
Member
There was a problem hiding this comment.
This can probably help us in the future: https://github.com/toon-format/toon
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Makes
ix catalogviable for its first real consumer: a Lean corpus of ~119 pinned packages (~81 building as one union, ~40 of them sharing a mathlib closure) whose entire build becomes oneix cataloginvocation. Per the plan: one memory blocker fixed, one latent correctness hole gated, a fail-closed coverage diagnostic, spec-file/audit/report ergonomics, and the in-repo benchmark that both catches the blocker and — as it turned out — found four more scaling walls.The series
catalog: pin loader imports to
OLeanLevel.private+ level-regression gates (Item 4 / I4)The catalog depended on
importModules' default level for D6 "complete bodies". An exported-level env axiomizes imported proofs and drops_private.*; kernel replay passes vacuously and--auditcompares two identically-axiomized legs (Lean v4.33.0 consolidation + module-mode full-content compile fix #572 documents this shipping in Upstream aux determinism, fail-closed compile, versioned.ixe, catalogs,import_ixefrom TruthMines #569) — no existing gate could catch a regression. Now explicit at both call sites, gated by an always-run base-env check and a loader-level fixtures test.catalog: fail closed on un-replayed cross-package roots (Item 5 / I5)
A member's closure may reach a provider module the provider's own roots don't cover; its constants were renamed but never replayed → bare kernel
unknown constant. Now a pre-replay coverage fold rejects with the member, module, owner, and the fix ("Add M to Q's roots"); misordered members are caught the same way.catalog: stream member environments — load, stage, free, one at a time (Item 1 / I1, the blocker)
resolveLibsheld every member env live; at corpus scale that is ~40× a mathlib env. Streaming requires actually freeing compacted olean regions, which requires staged declarations to share nothing with them — a fused rename + structural copy.forEachLibstreams members; the toolchain base imports once after the pass; staged declarations kernel-replay afterwards.auditCatalogstreams the same way, and its address comparison doubles as a copy-fidelity gate.Two Lean-runtime sharp edges found as segfaults and now permanently guarded: the code generator eta-reduces same-fields constructor rebuilds to the original (region-resident!) object (
.bvar,SourceInfo.synthetic,DataValue.ofBool— even through anif/elserebuild —ReducibilityHints.regular), and{ val with … }record updates silently share boxed fields. All-scalar rebuilds route one field through arithmetic the simplifier can't fold, and the copier self-checks withptrAddrUnsafepanics — a future codegen change fails loudly at staging time instead of corrupting kernel replay.bench: refresh CatalogReal member pins for Lean v4.33.0
The ignored benchmark had been unbuildable since the v4.33 consolidation (pre-4.33 batteries rev). New pins = the mathlib-v4.33.0-inherited revs (same as
Benchmarks/Compileand the downstream corpus). The Upstream aux determinism, fail-closed compile, versioned.ixe, catalogs,import_ixefrom TruthMines #569-era baselines belong to the old pins; refreshed baselines below.catalog: harden the region-evicting copier at real-library scale
Two more pass-through paths found at CatalogReal scale:
Array.mapM's unsafe implementation returns the input array object when it is empty (emptySyntax.nodeargs inofSyntaxmdata; Lists are immune —[]is a tagged scalar), and the remaining copiers gained the same self-check panics.catalog:
--specfile input (Item 3 / I3)JSON spec file, mutually exclusive with positionals;
groupsreserved for Item 2; parsed in the library (unit-tested — CLI modules only build under the exe build); resolved spec + path echoed into--report. Byte-identical to the positional build on CatalogReal.catalog:
--audit-onlysubset gating + peak RSS in--report(Items 6+7 / I6, I7)--audit-only Qual[,…]runs the §3.1 invariant on a rotating subset while still writing the artifact (the full audit is N+1 compiles — a multi-hour session at corpus scale).--reportgainspeakRssBytes(process-tree VmHWM via the existing texray sampler) andauditedQualifiers.catalog: hash-cons the region-evicting copy
First mathlib-spine wall: olean compaction dedups only within a module, so cross-module pointer sharing is ~zero (measured pointer-cache hit rate over batteries: 16%) and a purely pointer-cached copy materializes the member's entire syntactic content. The copy is now hash-consed — children intern before parents, so structural equality is shallow and the cached hash fields make it O(1) — and CatalogReal replay got faster (kernel sharecommon receives pre-shared input).
catalog: bound staging at mathlib scale — per-decl caches, copy/share hybrid, unconditional replay
Three more walls from the spine leg (Mathlib member: 569,200 owned constants): source-pointer caches grew with total visited content (~10⁹ nodes; the process hit
vm.max_map_count) → now reset per declaration; even hash-consed, heap-materializing a mathlib-scale member measures ~10× its compacted form → members owning >copyStageMaxOwned(default 100k) constants are staged sharing their env's regions, which stay mapped (EnvDisposal.keepRegions) — the corpus shape is exactly the favorable case (many small-content members with heavy closures: copy + free; a handful of heavy-content members: keep + share); and replay passed emptyOptionstoaddDecl, so defaultmaxHeartbeatsrejected mathlib's heavy proofs with a deterministic timeout (latent since Upstream aux determinism, fail-closed compile, versioned.ixe, catalogs,import_ixefrom TruthMines #569) → replay now runs unlimited — the declarations were already accepted once.bench: mathlib-spine catalog with a peak-RSS gate (Item 8 / I8)
Benchmarks/CatalogSpine: mathlib's dependency spine + Mathlib + three small real-corpus dependents (BET, GibbsMeasure, KolmogorovExtension4) whose envs each contain the full mathlib closure.lake test -- --ignored catalog-spineruns baseline and spine legs asixsubprocesses via--spec/--report(dogfooding I3/I7) and asserts the spine peak ≤ 1.6× baseline. Green.Measurements (124 GiB box, 32 cores, v4.33 pins)
fb0640061a61…--auditix check-rs realcat.ixecmp+ix diffclean, same root)--specvs positional artifact6e8bd09c14c6…; peak 32.2 GiB (was: 119 GiB OOM panic pre-hybrid; unbounded pre-streaming)3825539457d6…; peak 35.3 GiB — ratio 1.10×ix check-rson the spine artifactSpine.BET.periodicPt_mem_recurrentSetexhausts the Rust kernel'sMAX_REC_FUEL(10M); withIX_MAX_REC_FUEL=1000000000, 774,963/774,963 pass (399 s). Pre-existing checker ceiling, not a catalog defect (the Lean kernel re-accepted the declaration during replay)Trade-off note: at CatalogReal scale (three small members, overlapping closures) streaming costs more than the old hold-everything loader (5.9 → 10.6 GiB build-only peak) — the copy-out materializes union content the old code aliased from regions. The win is boundedness where it matters: N members sharing a heavy closure.
Gates
lake test -- catalog/catalog-qualified/import-ixe/--ignored catalog-fixtures(now also I4/I5/I6/hybrid tests) /--ignored catalog-spine,lake build ix— all green, run unpiped.Non-goals
Per the plan: no olean/source emission, no instance/attribute/LCNF transfer, no downstream corpus records or nix packaging, no
import_ixematerialization changes. Item 2 (grouped loading) deferred: streaming + the hybrid bring the spine into range; grouping remains available if corpus-scale import wall-clock (measured downstream) demands it.