diff --git a/Benchmarks/Catalog/RelocFixtureA/lean-toolchain b/Benchmarks/Catalog/RelocFixtureA/lean-toolchain index 14791d72..025e5954 100644 --- a/Benchmarks/Catalog/RelocFixtureA/lean-toolchain +++ b/Benchmarks/Catalog/RelocFixtureA/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 diff --git a/Benchmarks/Catalog/RelocFixtureB/lean-toolchain b/Benchmarks/Catalog/RelocFixtureB/lean-toolchain index 14791d72..025e5954 100644 --- a/Benchmarks/Catalog/RelocFixtureB/lean-toolchain +++ b/Benchmarks/Catalog/RelocFixtureB/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 diff --git a/Benchmarks/Catalog/lean-toolchain b/Benchmarks/Catalog/lean-toolchain index 14791d72..025e5954 100644 --- a/Benchmarks/Catalog/lean-toolchain +++ b/Benchmarks/Catalog/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 diff --git a/Benchmarks/CatalogReal/lake-manifest.json b/Benchmarks/CatalogReal/lake-manifest.json index ecaf45a6..c8971969 100644 --- a/Benchmarks/CatalogReal/lake-manifest.json +++ b/Benchmarks/CatalogReal/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/haskell-spec/haskell-spec", @@ -15,21 +15,22 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "7152850e7b216a0d409701617721b6e469d34bf6", + "inputRev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "756e3321fd3b02a85ffda19fef789916223e578c", + "inputRev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "inherited": false, "configFile": "lakefile.toml"}], "name": "CatalogReal", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/Benchmarks/CatalogReal/lakefile.toml b/Benchmarks/CatalogReal/lakefile.toml index db313da6..538ce769 100644 --- a/Benchmarks/CatalogReal/lakefile.toml +++ b/Benchmarks/CatalogReal/lakefile.toml @@ -19,12 +19,12 @@ name = "CompileHS" [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "756e3321fd3b02a85ffda19fef789916223e578c" +rev = "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d" [[require]] name = "aesop" git = "https://github.com/leanprover-community/aesop" -rev = "7152850e7b216a0d409701617721b6e469d34bf6" +rev = "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e" [[require]] name = "haskell-spec" diff --git a/Benchmarks/CatalogReal/lean-toolchain b/Benchmarks/CatalogReal/lean-toolchain index 14791d72..025e5954 100644 --- a/Benchmarks/CatalogReal/lean-toolchain +++ b/Benchmarks/CatalogReal/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 diff --git a/Benchmarks/CatalogSpine/lake-manifest.json b/Benchmarks/CatalogSpine/lake-manifest.json new file mode 100644 index 00000000..5c404165 --- /dev/null +++ b/Benchmarks/CatalogSpine/lake-manifest.json @@ -0,0 +1,136 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/RemyDegenne/kolmogorov_extension4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "7d76e184c3d2138a2741baf923b57e9a01b9cf25", + "name": "kolmogorov_extension4", + "manifestFile": "lake-manifest.json", + "inputRev": "7d76e184c3d2138a2741baf923b57e9a01b9cf25", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/YaelDillies/gibbs-measure", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2c57fb5f363f6afeb252b008f2bcedbd1b87b8cc", + "name": "GibbsMeasure", + "manifestFile": "lake-manifest.json", + "inputRev": "2c57fb5f363f6afeb252b008f2bcedbd1b87b8cc", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/mseri/BET", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e984d1b08f6c6d07fa690a78674e9ac6ef1050c2", + "name": "BET", + "manifestFile": "lake-manifest.json", + "inputRev": "e984d1b08f6c6d07fa690a78674e9ac6ef1050c2", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "16f02aa7642864af59f1ff0e384a015994db9118", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "CatalogSpine", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/Benchmarks/CatalogSpine/lakefile.toml b/Benchmarks/CatalogSpine/lakefile.toml new file mode 100644 index 00000000..b308178d --- /dev/null +++ b/Benchmarks/CatalogSpine/lakefile.toml @@ -0,0 +1,84 @@ +name = "CatalogSpine" +version = "0.1.0" + +# Mathlib-spine catalog benchmark (plan Item 8 / I8): a catalog whose +# members share one heavy closure — mathlib — so the streaming +# loader's construction-memory bound is observable. Peak RSS must be +# ~1× the heavy closure, not ~N×: before streaming (#569-shape +# `resolveLibs`), every mathlib-dependent member held its own copy of +# the mathlib environment simultaneously, which `Benchmarks/ +# CatalogReal` cannot exhibit (its members barely share closures). +# +# Members: mathlib's own dependency spine (every non-toolchain package +# in any member's import closure needs a catalog entry), Mathlib +# itself, and three small real-corpus mathlib dependents (BET, +# GibbsMeasure, kolmogorov_extension4) whose environments each contain +# the full mathlib closure. Revs are the TruthMines corpus pins +# (Lean v4.33.0). +# +# Manual-run territory like CatalogReal: needs network on first +# fetch, and run `lake exe cache get` before `lake build` to avoid a +# from-source mathlib build. Consumed by +# `lake test -- --ignored catalog-spine` (which needs +# `lake build ix` first) and by manual `ix catalog` runs with this +# directory as cwd. + +[[require]] +name = "batteries" +git = "https://github.com/leanprover-community/batteries" +rev = "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d" + +[[require]] +name = "Qq" +git = "https://github.com/leanprover-community/quote4" +rev = "92c15be17b7caf78c2ad767ec40f89052d908d81" + +[[require]] +name = "aesop" +git = "https://github.com/leanprover-community/aesop" +rev = "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e" + +[[require]] +name = "proofwidgets" +git = "https://github.com/leanprover-community/ProofWidgets4" +rev = "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957" + +[[require]] +name = "Cli" +git = "https://github.com/leanprover/lean4-cli" +rev = "6130a47896ce867c6a4a55373441e59e565bad0f" + +[[require]] +name = "importGraph" +git = "https://github.com/leanprover-community/import-graph" +rev = "16f02aa7642864af59f1ff0e384a015994db9118" + +[[require]] +name = "LeanSearchClient" +git = "https://github.com/leanprover-community/LeanSearchClient" +rev = "5f4d51b81cbd3f6b32b156bfad9056621a040404" + +[[require]] +name = "plausible" +git = "https://github.com/leanprover-community/plausible" +rev = "b7eb3304aeae834b12dda98993a37f6a41f6f0bb" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4" +rev = "db584cd6d46c92f209a44c0f1c829460d327499d" + +[[require]] +name = "BET" +git = "https://github.com/mseri/BET" +rev = "e984d1b08f6c6d07fa690a78674e9ac6ef1050c2" + +[[require]] +name = "GibbsMeasure" +git = "https://github.com/YaelDillies/gibbs-measure" +rev = "2c57fb5f363f6afeb252b008f2bcedbd1b87b8cc" + +[[require]] +name = "kolmogorov_extension4" +git = "https://github.com/RemyDegenne/kolmogorov_extension4" +rev = "7d76e184c3d2138a2741baf923b57e9a01b9cf25" diff --git a/Benchmarks/CatalogSpine/lean-toolchain b/Benchmarks/CatalogSpine/lean-toolchain new file mode 100644 index 00000000..025e5954 --- /dev/null +++ b/Benchmarks/CatalogSpine/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0 diff --git a/Ix/Catalog.lean b/Ix/Catalog.lean index af75281e..ff28bc25 100644 --- a/Ix/Catalog.lean +++ b/Ix/Catalog.lean @@ -12,20 +12,41 @@ Contract and deliberate simplifications: - **Kernel-level only.** Constants are relocated and kernel-replayed; instances, attributes, LCNF, and native code do not transfer. - - **Complete bodies, unconditionally.** Libraries load at - `OLeanLevel.private` (importModules' default), so `@[no_expose]` / - module-sealed definitions enter the catalog as ordinary transparent - definitions — Ix punches through the Lean module system (plan D6). + - **Complete bodies, unconditionally.** Member libraries and the + toolchain base load at `OLeanLevel.private` (explicit at both + importModules call sites), so `@[no_expose]` / module-sealed + definitions enter the catalog as ordinary transparent definitions — + Ix punches through the Lean module system (plan D6). The level is + load-bearing and invisible to every downstream gate: an + exported-level env axiomizes imported proofs and drops `_private.*` + constants, kernel replay accepts the axioms vacuously, and + `--audit` compares two identically-axiomized legs (#572) — so + regressions are caught by loader-level tests, not by the build. - **Ownership is Lake package identity.** A constant is owned by the package of its source module (`Environment.getModulePackageByIdx?`); toolchain modules (no package identity) form the shared unqualified base. Every non-toolchain package in any member's import closure - must be cataloged — fail closed otherwise. + must be cataloged, and every foreign cataloged module a member + reaches must lie inside its owner's declared root closure — fail + closed on both, before the kernel trips on a renamed-but-never- + replayed constant. - **Kernel replay regenerates auxiliaries.** Constructors and recursors (including nested-aux `rec_N`) are skipped and reappear when the kernel re-accepts the renamed `inductDecl`; their renamed names coincide with the renamed references because the lossless rule prefixes every owned name uniformly. + - **Construction memory is bounded** by the toolchain base, the + growing target env, one member environment at a time, and the kept + envs of heavy-content members (plan DQ5): members stream through + `forEachLib`; a member owning few constants is copy-staged out of + region memory (`stagePlan`) and its env's compacted olean regions + freed before the next member loads, while a member owning + mathlib-scale content is staged sharing its regions, which stay + mapped (`defaultCopyStageMaxOwned`). Without the copy-out, ~40 + corpus members sharing a mathlib closure would hold ~40 + fixup-dirtied copies of it simultaneously; without the keep-side, + the heavy member's content materializes as heap objects ~10× + fatter than its compacted form. Note on qualification: bare `Expr`/`Name`/`ConstantInfo` inside the `Ix` namespace resolve to ix's own mirror types, so Lean's are @@ -67,6 +88,46 @@ structure BuildResult where /-- Per-qualifier owned-constant counts (source constants, pre-replay). -/ perLib : Array (Lean.Name × Nat) +/-- Parse a catalog spec from its JSON file form (`ix catalog --spec`): + + ```json + { "prefix": "TruthMines", + "libs": [ { "qualifier": "Batteries", "roots": ["Batteries"] } ] } + ``` + + Fail-closed on structure: unknown keys are errors, and the `groups` + key is reserved for grouped loading (plan Item 2) so a spec written + for a future ix fails loudly here instead of silently flattening. -/ +def specFromJson (json : Lean.Json) : Except String CatalogSpec := do + let obj ← json.getObj? + for ⟨key, _⟩ in obj.toArray do + match key with + | "prefix" | "libs" => pure () + | "groups" => throw "`groups` is reserved for grouped loading and not yet supported" + | _ => throw s!"unknown key `{key}` in catalog spec" + let prefixStr ← (← json.getObjVal? "prefix").getStr? + if prefixStr.isEmpty then throw "empty `prefix`" + let libsArr ← (← json.getObjVal? "libs").getArr? + if libsArr.isEmpty then throw "`libs` is empty" + let mut libs : Array LibSpec := #[] + for libJson in libsArr do + let libObj ← libJson.getObj? + for ⟨key, _⟩ in libObj.toArray do + match key with + | "qualifier" | "roots" => pure () + | _ => throw s!"unknown key `{key}` in catalog spec lib entry" + let qualifier ← (← libJson.getObjVal? "qualifier").getStr? + if qualifier.isEmpty then throw "empty `qualifier` in lib entry" + let rootsArr ← (← libJson.getObjVal? "roots").getArr? + let mut roots : Array Lean.Name := #[] + for rootJson in rootsArr do + let root ← rootJson.getStr? + if root.isEmpty then throw s!"lib `{qualifier}`: empty root module name" + roots := roots.push root.toName + if roots.isEmpty then throw s!"lib `{qualifier}`: no root modules" + libs := libs.push { qualifier := qualifier.toName, roots } + return { catalogPrefix := prefixStr.toName, libs } + /-! ## Relocation core (absorbed from TruthMines `Internal.Relocate`) -/ def rename (names : Lean.NameMap Lean.Name) (name : Lean.Name) : Lean.Name := @@ -230,6 +291,417 @@ def relocateConstantInfo (names : Lean.NameMap Lean.Name) : ctor := rename names rule.ctor rhs := relocateExpr names rule.rhs } } +/-! ## Region-evicting relocation (the streaming replay path) + + `buildCatalog` frees each member environment's compacted olean + regions after staging its replay (`Environment.freeRegions`); without + the free, every member's mmapped-and-fixup-dirtied olean pages stay + resident for the life of the process, which at corpus scale means ~40 + members × a mathlib closure held simultaneously. Freeing is only + sound if nothing that survives the member references region memory, + and `relocateExpr` deliberately shares unchanged subterms with the + source env — so the replay path uses this family instead: a fused + rename + total structural copy. 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 is preserved, and hash-consed so structurally + equal content is copied ONCE per member — olean compaction dedups + only within a module, so without interning the copy materializes the + member's entire syntactic content (~100 GiB for a mathlib member; + measured pointer-cache hit rate over batteries is only ~16%). The + interpreter fallbacks of the safe wrappers are the sparse + equivalents: semantically identical, region-sharing, never used in + compiled code. -/ + +/-- Fresh heap copies of big numerals: scalars are immediate values and + need no copy; heap-allocated bignums are rebuilt (`+1-1` cannot + shortcut to its argument). Also load-bearing for the copiers below: + a match arm that rebuilds a constructor from unchanged scrutinee + fields is eta-reduced by the code generator to return the ORIGINAL + (region-resident!) object, so every all-scalar reconstruction + routes one field through this arithmetic to defeat that. -/ +private def copyNat (n : Nat) : Nat := n + 1 - 1 +private def copyInt (i : _root_.Int) : _root_.Int := i + 1 - 1 +private def copyUInt32 (u : UInt32) : UInt32 := u + 1 - 1 + +/-- Pointer equality (unsafe context only). -/ +private unsafe def peq {α : Type} (a b : α) : Bool := + ptrAddrUnsafe a == ptrAddrUnsafe b + +private unsafe def peqList {α : Type} : List α → List α → Bool + | [], [] => true + | a :: as, b :: bs => peq a b && peqList as bs + | _, _ => false + +/-! Interning wrappers: olean compaction dedups PER MODULE, so + cross-module pointer sharing in a member env is essentially zero — + a purely pointer-cached copy materializes the member's full + syntactic content (~100 GiB for a mathlib member). The copy is + therefore hash-consed: children are interned before their parents, + so structural equality of a candidate node is SHALLOW — head + constructor, pointer-equal children, equal scalars — and the + values' cached hash fields make the intern lookup O(1). The intern + tables key on the fresh COPIES (never on region objects), so they + survive `freeEnvRegions`. -/ + +private unsafe structure InternedName where + value : Lean.Name +private unsafe instance : Hashable InternedName where + hash a := a.value.hash +private unsafe instance : BEq InternedName where + beq a b := match a.value, b.value with + | .anonymous, .anonymous => true + | .str p s, .str p' s' => peq p p' && peq s s' + | .num p k, .num p' k' => peq p p' && k == k' + | _, _ => false + +private unsafe structure InternedLevel where + value : Lean.Level +private unsafe instance : Hashable InternedLevel where + hash a := a.value.hash +private unsafe instance : BEq InternedLevel where + beq a b := match a.value, b.value with + | .zero, .zero => true + | .succ x, .succ y => peq x y + | .max x y, .max x' y' => peq x x' && peq y y' + | .imax x y, .imax x' y' => peq x x' && peq y y' + | .param n, .param m => peq n m + | .mvar x, .mvar y => peq x.name y.name + | _, _ => false + +/-- Shallow equality for interning; `fvar`/`mvar`/`mdata` are never + interned (rare in kernel content, no cheap shallow form). -/ +private unsafe structure InternedExpr where + value : Lean.Expr +private unsafe instance : Hashable InternedExpr where + hash a := a.value.hash +private unsafe instance : BEq InternedExpr where + beq a b := match a.value, b.value with + | .bvar i, .bvar j => i == j + | .sort u, .sort v => peq u v + | .const n ls, .const m ms => peq n m && peqList ls ms + | .app f x, .app g y => peq f g && peq x y + | .lam n d c bi, .lam n' d' c' bi' => + peq n n' && peq d d' && peq c c' && bi == bi' + | .forallE n d c bi, .forallE n' d' c' bi' => + peq n n' && peq d d' && peq c c' && bi == bi' + | .letE n t v c nd, .letE n' t' v' c' nd' => + peq n n' && peq t t' && peq v v' && peq c c' && nd == nd' + | .lit (.natVal x), .lit (.natVal y) => x == y + | .lit (.strVal x), .lit (.strVal y) => peq x y + | .proj tn i v, .proj tn' i' v' => peq tn tn' && i == i' && peq v v' + | _, _ => false + +private unsafe structure CopyState where + /-- Value-keyed string intern; keys are the copies themselves. -/ + strings : Std.HashMap String String := {} + /-- Source-pointer → interned copy (skip re-traversal of repeats). -/ + namePtr : Lean.PtrMap Lean.Name Lean.Name := Lean.mkPtrMap + nameIntern : Std.HashMap InternedName Lean.Name := {} + levelPtr : Lean.PtrMap Lean.Level Lean.Level := Lean.mkPtrMap + levelIntern : Std.HashMap InternedLevel Lean.Level := {} + exprPtr : Lean.PtrMap Lean.Expr Lean.Expr := Lean.mkPtrMap + exprIntern : Std.HashMap InternedExpr Lean.Expr := {} + +private unsafe abbrev CopyM := StateM CopyState + +private unsafe def copyStringC (s : String) : CopyM String := do + match (← get).strings.get? s with + | some c => return c + | none => + let c := String.ofList s.toList + if ptrAddrUnsafe c == ptrAddrUnsafe s then + panic! "copyStringC returned its argument" + modify fun st => { st with strings := st.strings.insert c c } + return c + +private unsafe def copyName (n : Lean.Name) : CopyM Lean.Name := do + match n with + | .anonymous => return .anonymous + | _ => + match (← get).namePtr.find? n with + | some c => return c + | none => + let c ← match n with + | .anonymous => pure Lean.Name.anonymous + | .str p s => return .str (← copyName p) (← copyStringC s) + | .num p k => return .num (← copyName p) (copyNat k) + let c ← match (← get).nameIntern.get? ⟨c⟩ with + | some interned => pure interned + | none => + modify fun st => + { st with nameIntern := st.nameIntern.insert ⟨c⟩ c } + pure c + if ptrAddrUnsafe c == ptrAddrUnsafe n then + panic! "copyName returned its argument" + modify fun st => { st with namePtr := st.namePtr.insert n c } + return c + +private unsafe def copyLevel (l : Lean.Level) : CopyM Lean.Level := do + match l with + | .zero => return .zero + | _ => + match (← get).levelPtr.find? l with + | some c => return c + | none => + let c ← match l with + | .zero => pure Lean.Level.zero + | .succ a => return .succ (← copyLevel a) + | .max a b => return .max (← copyLevel a) (← copyLevel b) + | .imax a b => return .imax (← copyLevel a) (← copyLevel b) + | .param n => return .param (← copyName n) + | .mvar id => return .mvar ⟨← copyName id.name⟩ + let c ← match (← get).levelIntern.get? ⟨c⟩ with + | some interned => pure interned + | none => + modify fun st => + { st with levelIntern := st.levelIntern.insert ⟨c⟩ c } + pure c + if ptrAddrUnsafe c == ptrAddrUnsafe l then + panic! "copyLevel returned its argument" + modify fun st => { st with levelPtr := st.levelPtr.insert l c } + return c + +private unsafe def copySubstring (s : Substring.Raw) : CopyM Substring.Raw := do + let c : Substring.Raw := { s with str := (← copyStringC s.str) } + if ptrAddrUnsafe c == ptrAddrUnsafe s then + panic! "copySubstring returned its argument" + return c + +private unsafe def copySourceInfo (info : Lean.SourceInfo) : + CopyM Lean.SourceInfo := do + let c ← match info with + | .original leading pos trailing endPos => + pure <| Lean.SourceInfo.original (← copySubstring leading) pos + (← copySubstring trailing) endPos + | .synthetic pos endPos canonical => + pure <| Lean.SourceInfo.synthetic ⟨copyNat pos.byteIdx⟩ + ⟨copyNat endPos.byteIdx⟩ canonical + | .none => pure Lean.SourceInfo.none + if ptrAddrUnsafe c == ptrAddrUnsafe info && !(info matches .none) then + panic! "copySourceInfo returned its argument" + return c + +private unsafe def copyPreresolved (pre : Lean.Syntax.Preresolved) : + CopyM Lean.Syntax.Preresolved := do + let c ← match pre with + | .namespace ns => pure <| Lean.Syntax.Preresolved.namespace (← copyName ns) + | .decl n fields => + pure <| Lean.Syntax.Preresolved.decl (← copyName n) + (← fields.mapM copyStringC) + if ptrAddrUnsafe c == ptrAddrUnsafe pre then + panic! "copyPreresolved returned its argument" + return c + +private unsafe def copySyntax (stx : Lean.Syntax) : CopyM Lean.Syntax := do + let c ← match stx with + | .missing => pure Lean.Syntax.missing + | .node info kind args => + -- NOT `args.mapM`: `Array.mapM`'s unsafe implementation returns + -- the INPUT array object when it is empty, and empty `args` + -- arrays are common — a region-resident empty array would ride + -- through into the staged declaration. (Lists are immune: `[]` + -- is a tagged scalar, not a heap object.) + let mut argsC : Array Lean.Syntax := Array.mkEmpty args.size + for arg in args do + argsC := argsC.push (← copySyntax arg) + pure <| Lean.Syntax.node (← copySourceInfo info) (← copyName kind) argsC + | .atom info val => + pure <| Lean.Syntax.atom (← copySourceInfo info) (← copyStringC val) + | .ident info rawVal val preresolved => + pure <| Lean.Syntax.ident (← copySourceInfo info) (← copySubstring rawVal) + (← copyName val) (← preresolved.mapM copyPreresolved) + if ptrAddrUnsafe c == ptrAddrUnsafe stx && !(stx matches .missing) then + panic! "copySyntax returned its argument" + return c + +private unsafe def copyDataValue (dv : Lean.DataValue) : CopyM Lean.DataValue := do + let c ← match dv with + | .ofString s => pure <| Lean.DataValue.ofString (← copyStringC s) + | .ofBool b => pure (Lean.DataValue.ofBool (copyNat b.toNat == 1)) + | .ofName n => pure <| Lean.DataValue.ofName (← copyName n) + | .ofNat n => pure (Lean.DataValue.ofNat (copyNat n)) + | .ofInt i => pure (Lean.DataValue.ofInt (copyInt i)) + | .ofSyntax s => pure <| Lean.DataValue.ofSyntax (← copySyntax s) + -- Guard against code-generator eta (see `copyNat`): a panic here at + -- staging time beats a segfault after the regions are freed. + if ptrAddrUnsafe c == ptrAddrUnsafe dv then + let arm := match dv with + | .ofString _ => "ofString" | .ofBool _ => "ofBool" + | .ofName _ => "ofName" | .ofNat _ => "ofNat" + | .ofInt _ => "ofInt" | .ofSyntax _ => "ofSyntax" + panic! s!"copyDataValue returned its argument ({arm})" + return c + +private unsafe def copyMData (md : Lean.MData) : CopyM Lean.MData := do + let c : Lean.MData := { entries := + (← md.entries.mapM fun (k, v) => + return ((← copyName k), (← copyDataValue v))) } + if ptrAddrUnsafe c.entries == ptrAddrUnsafe md.entries && !md.entries.isEmpty then + panic! "copyMData returned its argument" + return c + +/-- The fused rename + total copy over expressions: `relocateExpr`'s + rewrite at `const`/`proj` sites, with every node — including + unchanged ones — rebuilt off region memory. -/ +private unsafe def relocExprC (names : Lean.NameMap Lean.Name) + (expr : Lean.Expr) : CopyM Lean.Expr := do + match (← get).exprPtr.find? expr with + | some c => return c + | none => + let c ← match expr with + | .bvar i => pure (Lean.Expr.bvar (copyNat i)) + | .fvar id => return .fvar ⟨← copyName id.name⟩ + | .mvar id => return .mvar ⟨← copyName id.name⟩ + | .sort u => return .sort (← copyLevel u) + | .const n ls => + return .const (← copyName (rename names n)) (← ls.mapM copyLevel) + | .app f a => return .app (← relocExprC names f) (← relocExprC names a) + | .lam n d b bi => + return .lam (← copyName n) (← relocExprC names d) + (← relocExprC names b) bi + | .forallE n d b bi => + return .forallE (← copyName n) (← relocExprC names d) + (← relocExprC names b) bi + | .letE n t v b nonDep => + return .letE (← copyName n) (← relocExprC names t) + (← relocExprC names v) (← relocExprC names b) nonDep + | .lit (.natVal n) => pure (.lit (.natVal (copyNat n))) + | .lit (.strVal s) => return .lit (.strVal (← copyStringC s)) + | .mdata md b => return .mdata (← copyMData md) (← relocExprC names b) + | .proj tn i v => + return .proj (← copyName (rename names tn)) i (← relocExprC names v) + -- Intern the candidate (skip fvar/mvar/mdata — no shallow form). + let c ← match expr with + | .fvar .. | .mvar .. | .mdata .. => pure c + | _ => + match (← get).exprIntern.get? ⟨c⟩ with + | some interned => pure interned + | none => + modify fun st => + { st with exprIntern := st.exprIntern.insert ⟨c⟩ c } + pure c + -- Guard against code-generator eta (see `copyNat`): the `.bvar` + -- arm regressed exactly this way — the rebuilt node was simplified + -- to the region-resident scrutinee. + if ptrAddrUnsafe c == ptrAddrUnsafe expr then + panic! s!"relocExprC returned its argument ({expr.ctorName})" + modify fun st => { st with exprPtr := st.exprPtr.insert expr c } + return c + +private unsafe def relocConstantValC (names : Lean.NameMap Lean.Name) + (cv : Lean.ConstantVal) : CopyM Lean.ConstantVal := + return { + name := (← copyName (rename names cv.name)) + levelParams := (← cv.levelParams.mapM copyName) + type := (← relocExprC names cv.type) } + +/-- `.regular` is a boxed constructor — a record update would share the + region-resident object. -/ +private def copyReducibilityHints : Lean.ReducibilityHints → Lean.ReducibilityHints + | .opaque => .opaque + | .abbrev => .abbrev + | .regular h => .regular (copyUInt32 h) + +private unsafe def relocDefinitionValC (names : Lean.NameMap Lean.Name) + (val : Lean.DefinitionVal) : CopyM Lean.DefinitionVal := + return { val with + toConstantVal := (← relocConstantValC names val.toConstantVal) + value := (← relocExprC names val.value) + hints := copyReducibilityHints val.hints + all := (← val.all.mapM fun n => copyName (rename names n)) } + +private unsafe def relocDeclarationC (names : Lean.NameMap Lean.Name) : + Lean.Declaration → CopyM Lean.Declaration + | .axiomDecl val => return .axiomDecl { val with + toConstantVal := (← relocConstantValC names val.toConstantVal) } + | .defnDecl val => return .defnDecl (← relocDefinitionValC names val) + | .thmDecl val => return .thmDecl { val with + toConstantVal := (← relocConstantValC names val.toConstantVal) + value := (← relocExprC names val.value) + all := (← val.all.mapM fun n => copyName (rename names n)) } + | .opaqueDecl val => return .opaqueDecl { val with + toConstantVal := (← relocConstantValC names val.toConstantVal) + value := (← relocExprC names val.value) + all := (← val.all.mapM fun n => copyName (rename names n)) } + | .mutualDefnDecl vals => + return .mutualDefnDecl (← vals.mapM (relocDefinitionValC names)) + | .inductDecl levelParams numParams types isUnsafe => + return .inductDecl (← levelParams.mapM copyName) numParams + (← types.mapM fun type => return { + name := (← copyName (rename names type.name)) + type := (← relocExprC names type.type) + ctors := (← type.ctors.mapM fun ctor => return { + name := (← copyName (rename names ctor.name)) + type := (← relocExprC names ctor.type) }) }) isUnsafe + | .quotDecl => return .quotDecl + +/-- One staged replay item: the relocated declaration plus both names + for diagnostics, all region-independent. -/ +structure StagedDecl where + source : Lean.Name + target : Lean.Name + decl : Lean.Declaration + +private unsafe def stagePlanUnsafe (names : Lean.NameMap Lean.Name) + (plan : Array (Lean.Name × Lean.Declaration)) : Array StagedDecl := + (plan.mapM fun (key, decl) => + (do + -- The source-pointer caches are reset PER DECLARATION: they + -- otherwise grow with the member's total visited content (~10⁹ + -- nodes ≈ 50 GiB of cache entries for a mathlib member). + -- Intra-declaration DAG sharing — what keeps the walk linear — + -- is preserved; cross-declaration repeats re-walk but collapse + -- at the persistent intern tables node by node. + modify fun (st : CopyState) => { st with + exprPtr := Lean.mkPtrMap + namePtr := Lean.mkPtrMap + levelPtr := Lean.mkPtrMap } + return { source := (← copyName key) + target := (← copyName (rename names key)) + decl := (← relocDeclarationC names decl) } : CopyM StagedDecl)) + |>.run' {} + +/-- Stage a replay plan SHARING the member env's regions: the sparse + relocation rewrites only renamed spines, everything else stays a + pointer into the env. Cheap and compact, but the env's regions + must then outlive the catalog (`EnvDisposal.keepRegions`). -/ +private def stageLibShared (names : Lean.NameMap Lean.Name) + (plan : Array (Lean.Name × Lean.Declaration)) : Array StagedDecl := + plan.map fun (key, decl) => + { source := key + target := rename names key + decl := relocateDeclaration names decl } + +/-- Stage one member's replay plan as region-independent copies: + rename fused with a hash-consed total copy. The staged + declarations share no memory with the member env, which makes + `freeEnvRegions` sound after staging. The reference implementation + is the region-sharing form — semantically identical, never used in + compiled code. -/ +@[implemented_by stagePlanUnsafe] +private opaque stagePlan (names : Lean.NameMap Lean.Name) + (plan : Array (Lean.Name × Lean.Declaration)) : Array StagedDecl := + stageLibShared names plan + +private unsafe def copyNameOutUnsafe (n : Lean.Name) : Lean.Name := + (copyName n).run' {} + +/-- Fresh, region-independent copy of a single name (for module names + and other scalars that outlive their member env). -/ +@[implemented_by copyNameOutUnsafe] +private opaque copyNameOut (n : Lean.Name) : Lean.Name := n + +private unsafe def freeEnvRegionsUnsafe (env : Lean.Environment) : IO Unit := + env.freeRegions + +/-- Free a member environment's compacted olean regions. Sound only + when nothing reachable from live data references the env's + imported objects — `forEachLib`'s callback contract. The reference + implementation is a no-op (leak, the pre-streaming behavior). -/ +@[implemented_by freeEnvRegionsUnsafe] +private opaque freeEnvRegions (_env : Lean.Environment) : IO Unit := pure () + /-- Accept a `DefinitionVal.all` list as unsafe-mutual grouping metadata only when every member is an owned definition carrying the same list — code-generating metaprograms may copy a recursor's `all` into @@ -431,92 +903,195 @@ private def ownershipMaps (spec : CatalogSpec) (env : Lean.Environment) owned := owned.insert name info return (renameMap, owned) -/-- Replay one library's owned constants into the growing kernel env: - build the per-env rename map, reconstruct declarations, order by - owned-reference dependencies, and `Kernel.Environment.addDecl` each - relocated declaration. Returns the updated env, the replay count, - and the owned source-constant count. -/ -private def replayLib (spec : CatalogSpec) (env : Lean.Environment) +/-- The I5 coverage gate: 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). `ownershipMaps` renames that module's + constants, but replay only ever delivers the closures of declared + roots — nothing replays them, and the kernel would reject `X`'s + first reference with a bare `unknown constant P.Y.N`. Detect it + before replay: members fold through in declaration order, + accumulating the module set each member's replay delivers; every + foreign cataloged module in `X`'s env must already be covered. + Under streaming, the qualifier map holds only members processed so + far, so a provider listed after its consumer and an uncatalogued + package surface as one unknown-provider error. Module names are + copied into `covered`: the set outlives the env. -/ +private def checkRootCoverage (lib : LibSpec) (env : Lean.Environment) (qualOfPkg : Std.HashMap Lean.PkgId Lean.Name) - (libPkgs : Std.HashSet Lean.PkgId) (kenv : Lean.Kernel.Environment) : - Except String (Lean.Kernel.Environment × Nat × Nat) := do - let (renameMap, owned) ← ownershipMaps spec env qualOfPkg libPkgs - let plan ← planDeclarations owned env.find? - let mut kenv := kenv - let mut replayed := 0 - for (key, decl) in plan do - let relocated := relocateDeclaration renameMap decl - match kenv.addDecl {} relocated with - | .ok kenv' => - kenv := kenv' - replayed := replayed + 1 - | .error e => - throw s!"kernel rejected `{rename renameMap key}` (source `{key}`): {renderKernelException e}" - return (kenv, replayed, owned.size) - -/-- Load every member library into its own environment (complete - bodies: `OLeanLevel.private` is the importModules default — so - colliding source names never meet at import time) and resolve the - package → qualifier map from each library's root modules. Shared by - `buildCatalog` and `auditCatalog`. -/ -def resolveLibs (spec : CatalogSpec) : - IO (Array Lean.Environment × Std.HashMap Lean.PkgId Lean.Name × - Array (Std.HashSet Lean.PkgId)) := do + (libPkgs : Std.HashSet Lean.PkgId) (covered : Lean.NameSet) : + Except String Lean.NameSet := do + let mut covered := covered + for moduleIdx in [0:env.header.moduleNames.size] do + match modulePackage? env moduleIdx with + | none => pure () -- toolchain base: unqualified, always present + | some pkg => + let moduleName := env.header.moduleNames[moduleIdx]! + if libPkgs.contains pkg then + covered := covered.insert (copyNameOut moduleName) + else + let some qualifier := qualOfPkg.get? pkg + | throw s!"member `{lib.qualifier}` references `{moduleName}` of \ +package `{pkg}`, which no member listed so far provides — either the \ +package is uncatalogued, or its provider is listed after \ +`{lib.qualifier}`. Every non-toolchain package in the import closure \ +needs a catalog entry, and members replay dependencies first." + unless covered.contains moduleName do + throw s!"member `{lib.qualifier}` references `{moduleName}`, \ +owned by qualifier `{qualifier}`, but `{qualifier}`'s roots do not \ +cover that module. Add `{moduleName}` to `{qualifier}`'s roots." + return covered + +/-- Members owning at most this many constants are copy-staged + (region-independent, env freed); a member owning more — a + mathlib-scale library — is staged sharing its env's regions, which + then stay mapped (`EnvDisposal.keepRegions`). Keeping one heavy + env (~8 GiB of compacted regions for mathlib) beats materializing + its content as heap objects, which measures ~10× fatter than the + compacted form even hash-consed. The corpus shape is many + small-content members whose CLOSURES are heavy (copy + free wins + there) and a handful of heavy-content members (keep + share wins + there). -/ +def defaultCopyStageMaxOwned : Nat := 100000 + +/-- The callback's verdict on a member environment's compacted + regions: `freeRegions` when everything the callback returned is + region-independent (copy-staged, or fresh strings); `keepRegions` + when the returned data deliberately shares the env's regions + (`stageLibShared`) — they then stay mapped for the life of the + process. -/ +inductive EnvDisposal where + | freeRegions + | keepRegions + +/-- Stream member libraries in declaration order: import each into its + own environment (so colliding source names never meet at import + time), resolve the member's packages from its root modules and + extend the package → qualifier map — members are declared + dependencies-first, so the map is complete for every environment by + the time its callback runs — invoke `f`, then dispose of the + environment's compacted olean regions as `f` directs. With + `.freeRegions` (the normal verdict) construction memory is bounded + by one member env at a time (plan DQ5); the callback then MUST NOT + retain the environment or anything reachable from it — copy what + survives (`stagePlan`, `copyNameOut`, or interpolation into fresh + strings). Imports are pinned to `OLeanLevel.private` — complete + bodies (D6); see the module header for why no downstream gate can + catch a level regression. Shared by `buildCatalog` and + `auditCatalog`. -/ +def forEachLib {α : Type} (spec : CatalogSpec) (init : α) + (f : α → LibSpec → Lean.Environment → + Std.HashMap Lean.PkgId Lean.Name → Std.HashSet Lean.PkgId → + IO (EnvDisposal × α)) : IO α := do if spec.libs.isEmpty then throw <| IO.userError "catalog: no member libraries" - let mut libEnvs : Array Lean.Environment := #[] + let mut qualOfPkg : Std.HashMap Lean.PkgId Lean.Name := {} + let mut acc := init for lib in spec.libs do let imports : Array Lean.Import := lib.roots.map ({ module := · }) - libEnvs := libEnvs.push (← Lean.importModules imports {}) - let mut qualOfPkg : Std.HashMap Lean.PkgId Lean.Name := {} - let mut libPkgs : Array (Std.HashSet Lean.PkgId) := #[] - for (lib, env) in spec.libs.zip libEnvs do + let env ← Lean.importModules imports {} (level := .private) let mut pkgs : Std.HashSet Lean.PkgId := {} for root in lib.roots do let some moduleIdx := env.getModuleIdx? root | throw <| IO.userError s!"catalog: root module `{root}` is not in `{lib.qualifier}`'s environment" let some pkg := modulePackage? env moduleIdx.toNat | throw <| IO.userError s!"catalog: root module `{root}` has no Lake package identity — toolchain modules cannot be cataloged" + -- `PkgId` is a region-resident string; the maps outlive the env. + let pkg : Lean.PkgId := String.ofList pkg.toList pkgs := pkgs.insert pkg match qualOfPkg.get? pkg with | some q => unless q == lib.qualifier do throw <| IO.userError s!"catalog: package `{pkg}` claimed by qualifiers `{q}` and `{lib.qualifier}`" | none => qualOfPkg := qualOfPkg.insert pkg lib.qualifier - libPkgs := libPkgs.push pkgs - return (libEnvs, qualOfPkg, libPkgs) + let (disposal, acc') ← try + f acc lib env qualOfPkg pkgs + catch e => + freeEnvRegions env + throw e + if disposal matches .freeRegions then + freeEnvRegions env + acc := acc' + return acc + +/-- Accumulator of the streaming member pass: staged replay plans (per + qualifier, with owned counts), the I5 coverage set, and the + toolchain module union — all region-independent. -/ +private structure BuildPass where + staged : Array (Lean.Name × Array StagedDecl × Nat) := #[] + covered : Lean.NameSet := {} + toolchainSeen : Lean.NameSet := {} + toolchainMods : Array Lean.Import := #[] /-- Build the catalog kernel environment for `spec`. Assumes the Lean search path already resolves every root module (CLI callers run - `initLeanSearchPath` first; in-process callers inherit theirs). -/ -def buildCatalog (spec : CatalogSpec) : IO BuildResult := do - -- 1./2. Load member envs and resolve package ownership. - let (libEnvs, qualOfPkg, libPkgs) ← resolveLibs spec - -- 3. Toolchain base: the union of toolchain modules across member - -- environments, imported once (single provider ⇒ no collisions). - let mut toolchainSeen : Lean.NameSet := {} - let mut toolchainMods : Array Lean.Import := #[] - for env in libEnvs do + `initLeanSearchPath` first; in-process callers inherit theirs). + `copyStageMaxOwned` is the copy-vs-share staging threshold (see + `defaultCopyStageMaxOwned`). -/ +def buildCatalog (spec : CatalogSpec) + (copyStageMaxOwned : Nat := defaultCopyStageMaxOwned) : + IO BuildResult := do + -- 1. Stream the members in dependency order: check root coverage + -- (I5), stage the replay, and accumulate the toolchain module + -- union. Small-content members are copy-staged and their envs + -- freed before the next loads; heavy-content members are staged + -- sharing their env's regions, which stay mapped. + let pass ← forEachLib spec ({} : BuildPass) fun pass lib env qualOfPkg pkgs => do + let covered ← match checkRootCoverage lib env qualOfPkg pkgs pass.covered with + | .ok covered => pure covered + | .error e => throw <| IO.userError s!"catalog: {e}" + let (renameMap, owned) ← match ownershipMaps spec env qualOfPkg pkgs with + | .ok maps => pure maps + | .error e => + throw <| IO.userError s!"catalog: library `{lib.qualifier}`: {e}" + let plan ← match planDeclarations owned env.find? with + | .ok plan => pure plan + | .error e => + throw <| IO.userError s!"catalog: library `{lib.qualifier}`: {e}" + let (decls, disposal) := + if owned.size ≤ copyStageMaxOwned then + (stagePlan renameMap plan, EnvDisposal.freeRegions) + else + (stageLibShared renameMap plan, EnvDisposal.keepRegions) + let ownedCount := owned.size + let mut toolchainSeen := pass.toolchainSeen + let mut toolchainMods := pass.toolchainMods for moduleIdx in [0:env.header.moduleNames.size] do - let moduleName := env.header.moduleNames[moduleIdx]! - if (modulePackage? env moduleIdx).isNone - && !toolchainSeen.contains moduleName then - toolchainSeen := toolchainSeen.insert moduleName - toolchainMods := toolchainMods.push { module := moduleName } - let baseEnv ← Lean.importModules toolchainMods {} - -- 4. Relocate + kernel-replay each library in dependency order. + if (modulePackage? env moduleIdx).isNone then + let moduleName := env.header.moduleNames[moduleIdx]! + if !toolchainSeen.contains moduleName then + let moduleName := copyNameOut moduleName + toolchainSeen := toolchainSeen.insert moduleName + toolchainMods := toolchainMods.push { module := moduleName } + return (disposal, + { staged := pass.staged.push (lib.qualifier, decls, ownedCount) + covered, toolchainSeen, toolchainMods }) + -- 2. Toolchain base: the union of toolchain modules across member + -- environments, imported once (single provider ⇒ no collisions). + -- Its regions are never freed — `consts` references them. + let baseEnv ← Lean.importModules pass.toolchainMods {} (level := .private) + -- 3. Kernel-replay the staged declarations in dependency order. let mut kenv := baseEnv.toKernelEnv let mut replayed := 0 let mut perLib : Array (Lean.Name × Nat) := #[] - for (lib, env, pkgs) in spec.libs.zip (libEnvs.zip libPkgs) do - match replayLib spec env qualOfPkg pkgs kenv with - | .ok (kenv', count, ownedCount) => - kenv := kenv' - replayed := replayed + count - perLib := perLib.push (lib.qualifier, ownedCount) - | .error e => - throw <| IO.userError s!"catalog: library `{lib.qualifier}`: {e}" - -- 5. Extract the full constant map (base + qualified + regenerated). + -- Replayed declarations were already kernel-accepted at elaboration + -- time, where per-file `set_option maxHeartbeats` overrides applied; + -- the replay must not re-impose the default budget (mathlib's heavy + -- proofs exceed it and would be rejected with a deterministic + -- timeout). + let replayOpts : Lean.Options := Lean.Options.empty.set `maxHeartbeats 0 + for (qualifier, decls, ownedCount) in pass.staged do + for staged in decls do + match kenv.addDecl replayOpts staged.decl with + | .ok kenv' => + kenv := kenv' + replayed := replayed + 1 + | .error e => + throw <| IO.userError s!"catalog: library `{qualifier}`: kernel \ +rejected `{staged.target}` (source `{staged.source}`): \ +{renderKernelException e}" + perLib := perLib.push (qualifier, ownedCount) + -- 4. Extract the full constant map (base + qualified + regenerated). let consts := kenv.constants.fold (init := #[]) fun acc name info => acc.push (name, info) return { consts, replayed, perLib } @@ -536,40 +1111,49 @@ structure AuditResult where `P.X.N`. Each member library is recompiled standalone (its own env, unqualified) and compared against one compile of the catalog — N+1 Rust compiles, so this is an opt-in gate (`ix catalog --audit`), - not part of the build. -/ + not part of the build. `only` restricts the standalone compiles and + comparison to the named qualifiers (`--audit-only`): at corpus + scale the full audit is a multi-hour session, so the invariant can + be gated on a rotating subset while the artifact still gets built. + Members outside the subset still stream through (their packages + extend the qualifier map) but skip the expensive legs. -/ def auditCatalog (spec : CatalogSpec) - (catalogConsts : Array (Lean.Name × Lean.ConstantInfo)) : + (catalogConsts : Array (Lean.Name × Lean.ConstantInfo)) + (only : Option Lean.NameSet := none) : IO AuditResult := do - let (libEnvs, qualOfPkg, libPkgs) ← resolveLibs spec let catEnv ← Ix.CompileM.rsCompileEnvOf catalogConsts.toList - let mut violations : Array String := #[] - let mut checked := 0 - for (lib, env, pkgs) in spec.libs.zip (libEnvs.zip libPkgs) do - let (renameMap, owned) ← - match ownershipMaps spec env qualOfPkg pkgs with - | .ok maps => pure maps - | .error e => - throw <| IO.userError s!"catalog audit: `{lib.qualifier}`: {e}" - let stdEnv ← Ix.CompileM.rsCompileEnvOf env.constants.toList - for (name, _) in owned do - let target := rename renameMap name - let (ixSrc, _) := (CanonM.canonName name).run {} - let (ixTgt, _) := (CanonM.canonName target).run {} - match stdEnv.named.get? ixSrc, catEnv.named.get? ixTgt with - | some src, some tgt => - checked := checked + 1 - if src.addr != tgt.addr then - violations := violations.push - s!"{lib.qualifier}: addr({name}) = {src.addr} standalone \ + forEachLib spec ({ checked := 0, violations := #[] } : AuditResult) + fun acc lib env qualOfPkg pkgs => do + if only.any (!·.contains lib.qualifier) then return (.freeRegions, acc) + let (renameMap, owned) ← + match ownershipMaps spec env qualOfPkg pkgs with + | .ok maps => pure maps + | .error e => + throw <| IO.userError s!"catalog audit: `{lib.qualifier}`: {e}" + let stdEnv ← Ix.CompileM.rsCompileEnvOf env.constants.toList + -- Only fresh strings and counts survive into the accumulator; + -- the env (and everything region-backed) dies with the callback. + let mut violations := acc.violations + let mut checked := acc.checked + for (name, _) in owned do + let target := rename renameMap name + let (ixSrc, _) := (CanonM.canonName name).run {} + let (ixTgt, _) := (CanonM.canonName target).run {} + match stdEnv.named.get? ixSrc, catEnv.named.get? ixTgt with + | some src, some tgt => + checked := checked + 1 + if src.addr != tgt.addr then + violations := violations.push + s!"{lib.qualifier}: addr({name}) = {src.addr} standalone \ but addr({target}) = {tgt.addr} in the catalog" - | none, _ => - violations := violations.push - s!"{lib.qualifier}: standalone compile has no named entry \ + | none, _ => + violations := violations.push + s!"{lib.qualifier}: standalone compile has no named entry \ for `{name}`" - | _, none => - violations := violations.push - s!"{lib.qualifier}: catalog compile has no named entry for \ + | _, none => + violations := violations.push + s!"{lib.qualifier}: catalog compile has no named entry for \ `{target}`" - return { checked, violations } + return (.freeRegions, { checked, violations }) end Ix.Catalog diff --git a/Ix/Cli/CatalogCmd.lean b/Ix/Cli/CatalogCmd.lean index bf7ea408..2e2d36aa 100644 --- a/Ix/Cli/CatalogCmd.lean +++ b/Ix/Cli/CatalogCmd.lean @@ -12,6 +12,7 @@ public import Ix.Common public import Ix.Meta public import Ix.CompileM public import Ix.Catalog +public import Ix.TracingTexray public section @@ -30,28 +31,76 @@ private def parseLibSpec (raw : String) : Except String Ix.Catalog.LibSpec := do return { qualifier := qualifier.toName, roots := rootNames.toArray } | _ => throw s!"expected `Qualifier=Root[,Root...]`, got `{raw}`" -def runCatalogCmd (p : Cli.Parsed) : IO UInt32 := do - let some prefixFlag := p.flag? "prefix" - | p.printError "error: --prefix is required (the catalog namespace, e.g. `MyCatalog`)" - return 1 - let catalogPrefix := (prefixFlag.as! String).toName +/-- Resolve the catalog spec from either `--spec file.json` (parsed by + `Ix.Catalog.specFromJson`) or the positional + `Qualifier=Root[,Root...]` form with `--prefix`. The two forms are + mutually exclusive; the spec file carries its own prefix. -/ +private def resolveSpec (p : Cli.Parsed) : + IO (Except String Ix.Catalog.CatalogSpec) := do let rawLibs := (p.variableArgsAs! String).toList - if rawLibs.isEmpty then - p.printError "error: at least one `Qualifier=Root[,Root...]` library spec is required" - return 1 - let mut libs : Array Ix.Catalog.LibSpec := #[] - for raw in rawLibs do - match parseLibSpec raw with - | .ok lib => libs := libs.push lib + match p.flag? "spec" with + | some specFlag => + if !rawLibs.isEmpty then + return .error "--spec is mutually exclusive with positional library specs" + if (p.flag? "prefix").isSome then + return .error "--spec files carry the prefix; drop --prefix" + let path := specFlag.as! String + let content ← try IO.FS.readFile path + catch e => return .error s!"cannot read --spec file `{path}`: {e}" + return do + let json ← Lean.Json.parse content + |>.mapError (s!"--spec `{path}`: invalid JSON: {·}") + Ix.Catalog.specFromJson json |>.mapError (s!"--spec `{path}`: {·}") + | none => + let some prefixFlag := p.flag? "prefix" + | return .error "--prefix is required (the catalog namespace, e.g. \ +`MyCatalog`) unless --spec is given" + let catalogPrefix := (prefixFlag.as! String).toName + if rawLibs.isEmpty then + return .error "at least one `Qualifier=Root[,Root...]` library spec \ +is required (or use --spec)" + let mut libs : Array Ix.Catalog.LibSpec := #[] + for raw in rawLibs do + match parseLibSpec raw with + | .ok lib => libs := libs.push lib + | .error e => return .error e + return .ok { catalogPrefix, libs } + +def runCatalogCmd (p : Cli.Parsed) : IO UInt32 := do + let spec ← match ← resolveSpec p with + | .ok spec => pure spec | .error e => p.printError s!"error: {e}" return 1 - let spec : Ix.Catalog.CatalogSpec := { catalogPrefix, libs } + let catalogPrefix := spec.catalogPrefix + let libs := spec.libs let outPath := (p.flag? "out").map (·.as! String) |>.getD (s!"{catalogPrefix}".toLower ++ ".ixe") + -- --audit-only: validate the subset against the spec up front. + let auditOnly? : Option (Array Lean.Name) ← + match p.flag? "audit-only" with + | none => pure none + | some flag => + let quals := ((flag.as! String).splitOn ",").filterMap fun q => + let q := q.trimAscii.toString + if q.isEmpty then none else some q.toName + if quals.isEmpty then + p.printError "error: --audit-only needs at least one qualifier" + return 1 + for q in quals do + unless spec.libs.any (·.qualifier == q) do + p.printError s!"error: --audit-only qualifier `{q}` is not a \ +member of the catalog spec" + return 1 + pure (some quals.toArray) + -- Resolve modules through the current directory's Lake workspace. initLeanSearchPath (some (← IO.currentDir)) + -- Peak-RSS accounting for --report (I7): process-tree sampler, + -- Linux-only (reads back 0 elsewhere). + TracingTexray.startSampler + TracingTexray.resetPeakTreeRss println! "Building catalog {catalogPrefix} from {libs.size} librar(ies)..." let buildStart ← IO.monoMsNow @@ -62,13 +111,19 @@ def runCatalogCmd (p : Cli.Parsed) : IO UInt32 := do println! "[catalog] replayed {result.replayed} declarations; \ {result.consts.size} constants total in {buildElapsed}ms" - if p.hasFlag "audit" then + let auditRan := p.hasFlag "audit" || auditOnly?.isSome + if auditRan then + let only := auditOnly?.map fun quals => + quals.foldl (init := ({} : Lean.NameSet)) (·.insert ·) + let scope := match auditOnly? with + | some quals => s!"members {quals}" + | none => "all members" let auditStart ← IO.monoMsNow - let audit ← Ix.Catalog.auditCatalog spec result.consts + let audit ← Ix.Catalog.auditCatalog spec result.consts only let auditElapsed := (← IO.monoMsNow) - auditStart if audit.violations.isEmpty then println! "[audit] anon-address preservation: {audit.checked} owned \ -constants verified in {auditElapsed}ms" +constants verified ({scope}) in {auditElapsed}ms" else let stderr ← IO.getStderr stderr.putStrLn s!"error: catalog audit found \ @@ -90,6 +145,7 @@ constants verified in {auditElapsed}ms" let ungroundedCount := status.ungrounded.size let failClosed := !allowPartial && ungroundedCount > 0 + let peakRssBytes ← TracingTexray.peakTreeRssBytes if let some flag := p.flag? "report" then let report := Lean.Json.mkObj [ ("schemaVersion", Lean.toJson (1 : Nat)) @@ -97,6 +153,8 @@ constants verified in {auditElapsed}ms" , ("leanToolchain", Lean.Json.str Lean.versionString) , ("ixeFormatVersion", Lean.toJson Ixon.Env.VERSION.toNat) , ("catalogPrefix", Lean.Json.str s!"{catalogPrefix}") + , ("specFile", (p.flag? "spec").map (fun f => Lean.Json.str (f.as! String)) + |>.getD Lean.Json.null) , ("libs", Lean.Json.arr <| libs.map fun lib => Lean.Json.mkObj [ ("qualifier", Lean.Json.str s!"{lib.qualifier}") , ("roots", Lean.Json.arr <| @@ -115,7 +173,15 @@ constants verified in {auditElapsed}ms" , ("written", Lean.toJson (!failClosed)) , ("bytes", Lean.toJson size) , ("buildMs", Lean.toJson buildElapsed) - , ("compileMs", Lean.toJson elapsed) ] + , ("compileMs", Lean.toJson elapsed) + -- Process-tree high-water mark (I7); 0 on non-Linux platforms. + , ("peakRssBytes", Lean.toJson peakRssBytes) + , ("auditedQualifiers", match auditRan, auditOnly? with + | false, _ => Lean.Json.null + | true, none => Lean.Json.arr <| + libs.map (Lean.Json.str s!"{·.qualifier}") + | true, some quals => Lean.Json.arr <| + quals.map (Lean.Json.str s!"{·}")) ] IO.FS.writeFile (flag.as! String) (report.pretty ++ "\n") if ungroundedCount > 0 then @@ -148,11 +214,13 @@ def catalogCmd : Cli.Cmd := `[Cli| "Build a qualified multi-library union environment (a catalog) and compile it to one .ixe. Member constants land under ..; the toolchain base stays unqualified. Kernel-level: instances, attributes, and native code do not transfer." FLAGS: - "prefix" : String; "The catalog namespace, e.g. `MyCatalog` (required)." + "prefix" : String; "The catalog namespace, e.g. `MyCatalog` (required unless --spec is given)." + spec : String; "Path to a JSON spec file `{\"prefix\": ..., \"libs\": [{\"qualifier\": ..., \"roots\": [...]}]}` — the file form of the positional specs, resolved identically and echoed into --report. Mutually exclusive with positional libs and --prefix; the `groups` key is reserved." out : String; "Output path for the serialized .ixe; defaults to the lowercased prefix with `.ixe`." "allow-partial" ; "Serialize the grounded subset and exit 0 even when some catalog constants fail to compile. Default is fail-closed: any ungrounded constant means a nonzero exit and NO output file." audit ; "Verify anon-address preservation before writing: recompile each member library standalone and require addr(..N) in the catalog to equal addr(N) standalone, for every owned constant (qualification is metadata-only). N+1 extra compiles; violations abort with no output file." - report : String; "Write a machine-readable JSON catalog report (versions, lib specs, counts, ungrounded list, canonical root) to this path — written on success, fail-closed abort, and partial publish alike." + "audit-only" : String; "Comma-separated member qualifiers: run the --audit invariant on just these members (a rotating subset keeps the gate viable at corpus scale, where the full audit is N+1 large compiles). Implies --audit; the artifact is still built and written." + report : String; "Write a machine-readable JSON catalog report (versions, lib specs, counts, ungrounded list, canonical root, peak RSS, audited qualifiers) to this path — written on success, fail-closed abort, and partial publish alike." ARGS: ...libs : String; "Member library specs `Qualifier=Root[,Root...]` in dependency order (dependencies first), e.g. `Batteries=Batteries HaskellSpec=HaskellSpec`." diff --git a/Tests/Ix/Catalog.lean b/Tests/Ix/Catalog.lean index 409678bc..805a6cb1 100644 --- a/Tests/Ix/Catalog.lean +++ b/Tests/Ix/Catalog.lean @@ -36,6 +36,17 @@ def buildTest : TestSeq := let result ← Ix.Catalog.buildCatalog spec let names : Std.HashSet Lean.Name := result.consts.foldl (fun s (n, _) => s.insert n) {} + -- I4 loader-level gate, base leg: at `OLeanLevel.private` the + -- toolchain base keeps theorem proofs and `_private.*` constants. + -- At exported level `Nat.add_comm` is a body-less axiom and the + -- privates are absent — and kernel replay still succeeds, so only + -- this check notices (see the `Ix.Catalog` module header). + let baseThmKeepsProof := + match result.consts.find? (·.1 == `Nat.add_comm) with + | some (_, .thmInfo _) => true + | _ => false + let basePrivatesPresent := + result.consts.any fun (n, _) => (`_private).isPrefixOf n let checks : List (String × Bool) := [ ("replayed something", result.replayed > 0), ("qualified LSpec.TestSeq present", @@ -47,11 +58,51 @@ def buildTest : TestSeq := ("no unqualified LSpec constants", !names.contains `LSpec.TestSeq), ("no unqualified Cli constants", !names.contains `Cli.Cmd), ("toolchain base is unqualified", names.contains `Nat), + ("base theorem keeps its proof (private-level import)", + baseThmKeepsProof), + ("base `_private.*` constants present", basePrivatesPresent), ("perLib counts populated", result.perLib.all (·.2 > 0)) ] match checks.find? (!·.2) with | some (what, _) => return (false, 0, 0, some s!"failed: {what}") | none => return (true, 0, 0, none)) .done -def suite : List TestSeq := [buildTest] +/-- I3: the `--spec` JSON file form resolves to exactly the positional + spec, and malformed specs fail closed (reserved `groups` key, + unknown keys, empty libs). Pure parsing — the CLI is a thin shell + over `specFromJson`. -/ +def specJsonTest : TestSeq := + .individualIO "catalog: --spec JSON resolves to the positional spec" none (do + let sample := "{ \"prefix\": \"TestCatalog\", \"libs\": [ + { \"qualifier\": \"Plausible\", \"roots\": [\"Plausible\"] }, + { \"qualifier\": \"LSpec\", \"roots\": [\"LSpec\"] }, + { \"qualifier\": \"Cli\", \"roots\": [\"Cli\"] } ] }" + let parsed ← match Lean.Json.parse sample |>.bind Ix.Catalog.specFromJson with + | .ok parsed => pure parsed + | .error e => return (false, 0, 0, some s!"sample spec rejected: {e}") + let sameAsPositional := parsed.catalogPrefix == spec.catalogPrefix + && parsed.libs.size == spec.libs.size + && (parsed.libs.zip spec.libs).all fun (a, b) => + a.qualifier == b.qualifier && a.roots == b.roots + let rejects (raw : String) (needle : String) : Bool := + match Lean.Json.parse raw |>.bind Ix.Catalog.specFromJson with + | .ok _ => false + | .error e => (e.splitOn needle).length > 1 + let checks : List (String × Bool) := [ + ("spec file equals positional spec", sameAsPositional), + ("groups key is reserved", + rejects "{ \"prefix\": \"X\", \"libs\": [{ \"qualifier\": \"A\", \ +\"roots\": [\"A\"] }], \"groups\": [] }" "reserved"), + ("unknown key fails closed", + rejects "{ \"prefix\": \"X\", \"libs\": [], \"extra\": 1 }" "unknown key"), + ("empty libs fails closed", + rejects "{ \"prefix\": \"X\", \"libs\": [] }" "empty"), + ("unknown lib key fails closed", + rejects "{ \"prefix\": \"X\", \"libs\": [{ \"qualifier\": \"A\", \ +\"roots\": [\"A\"], \"deps\": [] }] }" "unknown key") ] + match checks.find? (!·.2) with + | some (what, _) => return (false, 0, 0, some s!"failed: {what}") + | none => return (true, 0, 0, none)) .done + +def suite : List TestSeq := [buildTest, specJsonTest] end Tests.Ix.Catalog diff --git a/Tests/Ix/CatalogFixtures.lean b/Tests/Ix/CatalogFixtures.lean index 4a100457..5a39ca5b 100644 --- a/Tests/Ix/CatalogFixtures.lean +++ b/Tests/Ix/CatalogFixtures.lean @@ -18,6 +18,13 @@ - Owner-aware rewriting: `FixtureA.importedScore`'s relocated form references the qualified `FixtureB` constants (the unqualified source names do not exist in the catalog). + - I4 (loader olean level): member envs come in at private level — + imported theorems keep their proofs, `_private.*` constants are + present, `@[no_expose]` definitions load transparent. + - I5 (root coverage): a member reaching a provider module outside + the provider's declared roots — or a provider listed after its + consumer — fails closed with a named error before the kernel + trips on a renamed-but-never-replayed constant. Needs the fixture workspace buildable (network-free; toolchain shared), so it lives behind `--ignored`. @@ -112,6 +119,154 @@ private def fixturesTest : IO (Bool × Nat × Nat × Option String) := do | some (what, _) => return (false, 0, 0, some s!"failed: {what}") | none => return (true, audit.checked, result.consts.size, none) +/-- Pure checks over member `A`'s live env; only fresh strings and + counts escape (the env's regions are freed after the `forEachLib` + callback returns). -/ +private def checkMemberEnvA (envA : Lean.Environment) : + Bool × Nat × Nat × Option String := Id.run do + -- Imported toolchain theorem: a real proof whose references all + -- resolve in the same env (at exported level it is a body-less axiom). + match envA.constants.find? `Nat.add_comm with + | some (.thmInfo v) => + for r in v.value.getUsedConstants do + unless envA.contains r do + return (false, 0, 0, + some s!"Nat.add_comm proof ref {r} dangling — env not closed") + | some _ => return (false, 0, 0, + some "Nat.add_comm is not a theorem — exported-level trim suspected") + | none => return (false, 0, 0, some "Nat.add_comm missing from member env") + -- The member's own module-mode theorem keeps its proof. + match envA.constants.find? `FixtureA.importedScore_eq with + | some (.thmInfo _) => pure () + | some _ => return (false, 0, 0, + some "FixtureA.importedScore_eq is not a theorem") + | none => return (false, 0, 0, + some "FixtureA.importedScore_eq missing from member env") + -- `@[no_expose]` loads as a transparent definition (D6 at the loader). + match envA.constants.find? `Collision.concealedDefinition with + | some (.defnInfo _) => pure () + | some _ => return (false, 0, 0, + some "no_expose Collision.concealedDefinition did not load as a defn") + | none => return (false, 0, 0, + some "Collision.concealedDefinition missing from member env") + -- Non-exported `_private.*` constants from imports are present. + let privCount := envA.constants.toList.countP + fun (n, _) => (`_private).isPrefixOf n + if privCount == 0 then + return (false, 0, 0, + some "no `_private.*` constants — exported-level trim suspected") + return (true, privCount, envA.constants.toList.length, none) + +/-- I4 gate: the catalog loader must import at `OLeanLevel.private`. + An exported-level member env (what module-mode header processing + yields) carries imported public theorems as body-less axioms and + omits `_private.*` constants — the catalog then axiomizes proofs, + kernel replay accepts vacuously, and `--audit` compares two + identically-axiomized legs (#572). Only the loaded env itself can + witness the regression, so assert on member `A`'s env as streamed + by `forEachLib` (module-mode fixtures: `@[no_expose]`, theorems, a + cross-package import). Relies on `fixturesTest` having built the + fixture workspace. -/ +private def loaderLevelTest : IO (Bool × Nat × Nat × Option String) := do + initLeanSearchPath (some fixtureDir) + Ix.Catalog.forEachLib spec + (false, 0, 0, some "member `A` never streamed") + fun acc lib env _ _ => do + if lib.qualifier == `A then + return (.freeRegions, checkMemberEnvA env) + else + return (.freeRegions, acc) + +/-- I6: `auditCatalog` restricted to a qualifier subset checks exactly + that subset — fewer constants than the full audit, still zero + violations. -/ +private def auditOnlyTest : IO (Bool × Nat × Nat × Option String) := do + initLeanSearchPath (some fixtureDir) + let result ← Ix.Catalog.buildCatalog spec + let full ← Ix.Catalog.auditCatalog spec result.consts + let onlyB ← Ix.Catalog.auditCatalog spec result.consts + (some (({} : Lean.NameSet).insert `B)) + unless onlyB.violations.isEmpty do + return (false, 0, 0, + some s!"subset audit violation: {onlyB.violations[0]!}") + unless onlyB.checked > 0 && onlyB.checked < full.checked do + return (false, 0, 0, + some s!"subset checked {onlyB.checked}, full checked {full.checked}") + return (true, onlyB.checked, full.checked, none) + +private def containsStr (haystack needle : String) : Bool := + (haystack.splitOn needle).length > 1 + +/-- I5: a member reaching a provider module outside the provider's + declared root closure fails closed with a named, actionable error + identifying the module and its owner — not a bare kernel `unknown + constant`. `B`'s roots are narrowed to `FixtureB.Model`, so `A` + (whose `UsesB` imports `FixtureB.Base`) references a `B`-owned + module nobody would replay. -/ +private def coverageErrorTest : IO (Bool × Nat × Nat × Option String) := do + initLeanSearchPath (some fixtureDir) + let badSpec : Ix.Catalog.CatalogSpec := { + catalogPrefix := `RelocCat + libs := #[ + { qualifier := `B, roots := #[`FixtureB.Model] }, + { qualifier := `A, roots := #[`FixtureA] } ] } + try + let _ ← Ix.Catalog.buildCatalog badSpec + return (false, 0, 0, + some "narrowed-roots build succeeded; expected the I5 coverage error") + catch e => + let msg := toString e + unless containsStr msg "FixtureB.Base" do + return (false, 0, 0, + some s!"error does not name the module: {msg.take 200}") + unless containsStr msg "roots do not cover" do + return (false, 0, 0, + some s!"error is not the coverage diagnostic: {msg.take 200}") + return (true, 0, 0, none) + +/-- I5, ordering flavor: a provider listed after its consumer is + reported as a spec ordering error, not a missing root. -/ +private def orderingErrorTest : IO (Bool × Nat × Nat × Option String) := do + initLeanSearchPath (some fixtureDir) + let badSpec : Ix.Catalog.CatalogSpec := { + catalogPrefix := `RelocCat + libs := #[ + { qualifier := `A, roots := #[`FixtureA] }, + { qualifier := `B, roots := #[`FixtureB] } ] } + try + let _ ← Ix.Catalog.buildCatalog badSpec + return (false, 0, 0, + some "misordered build succeeded; expected the I5 ordering error") + catch e => + let msg := toString e + unless containsStr msg "listed after" do + return (false, 0, 0, + some s!"error is not the ordering diagnostic: {msg.take 200}") + return (true, 0, 0, none) + +/-- The copy-staged and region-shared staging paths produce identical + artifacts: build with the default threshold (fixture members are + all copy-staged) and with threshold 0 (all shared, envs kept), and + compare canonical roots. -/ +private def hybridStagingTest : IO (Bool × Nat × Nat × Option String) := do + initLeanSearchPath (some fixtureDir) + let dir ← IO.FS.createTempDir + try + let copied ← Ix.Catalog.buildCatalog spec + let sCopied ← Ix.CompileM.rsCompileEnvBytesFFI copied.consts.toList + (dir / "copied.ixe").toString false + let shared ← Ix.Catalog.buildCatalog spec (copyStageMaxOwned := 0) + let sShared ← Ix.CompileM.rsCompileEnvBytesFFI shared.consts.toList + (dir / "shared.ixe").toString false + if sCopied.root != sShared.root then + return (false, 0, 0, some s!"staging-path root drift: \ +{sCopied.root.take 12}… vs {sShared.root.take 12}…") + if sCopied.bytes != sShared.bytes then + return (false, 0, 0, some "staging-path byte-size drift") + return (true, sCopied.bytes.toNat, 0, none) + finally + IO.FS.removeDirAll dir + /-- C3: two independent build+compile passes agree on the canonical root. -/ private def determinismTest : IO (Bool × Nat × Nat × Option String) := do @@ -150,6 +305,16 @@ private def determinismTest : IO (Bool × Nat × Nat × Option String) := do def suite : List TestSeq := [ .individualIO "catalog fixtures: audit + dedup matrix (C1/C2)" none fixturesTest .done, + .individualIO "catalog fixtures: loader imports at private level (I4)" + none loaderLevelTest .done, + .individualIO "catalog fixtures: uncovered provider module fails closed (I5)" + none coverageErrorTest .done, + .individualIO "catalog fixtures: audit restricted to a subset (I6)" + none auditOnlyTest .done, + .individualIO "catalog fixtures: copy-staged ≡ region-shared staging" + none hybridStagingTest .done, + .individualIO "catalog fixtures: misordered members fail closed (I5)" + none orderingErrorTest .done, .individualIO "catalog fixtures: deterministic root + kernel check (C3/C4)" none determinismTest .done ] diff --git a/Tests/Ix/CatalogSpine.lean b/Tests/Ix/CatalogSpine.lean new file mode 100644 index 00000000..8fe7e992 --- /dev/null +++ b/Tests/Ix/CatalogSpine.lean @@ -0,0 +1,124 @@ +/- + Mathlib-spine peak-RSS gate (plan Item 8 / I8): a catalog whose + members share one heavy closure — mathlib — must build with peak RSS + ~1× that closure, not ~N×. `Benchmarks/CatalogReal` cannot exhibit + the pre-streaming failure (its members barely share closures); + `Benchmarks/CatalogSpine` adds three small real-corpus mathlib + dependents (BET, GibbsMeasure, KolmogorovExtension4) whose + environments each contain the full mathlib closure. + + Two subprocess legs of `ix catalog --spec … --report …` (dogfooding + I3/I7): a baseline over mathlib + its dependency spine, then the + full spine with the three dependents. The gate asserts the spine + peak (`peakRssBytes`, process-tree VmHWM) stays under 1.6× the + baseline — pre-streaming, each extra dependent held its own mathlib + environment and the ratio lands well above that. + + Heavy and manual (`--ignored catalog-spine`): needs `lake build ix` + first, network + `lake exe cache get` on the first workspace build, + and the RSS sampler is Linux-only (the gate fails, not skips, where + it cannot measure). +-/ +module + +public import LSpec +public import Ix.Catalog + +public section + +open LSpec + +namespace Tests.Ix.CatalogSpine + +private def spineDir : System.FilePath := "Benchmarks" / "CatalogSpine" +private def ixExe : System.FilePath := ".lake" / "build" / "bin" / "ix" + +/-- Mathlib's dependency spine, dependencies first: every non-toolchain + package in any member's import closure needs a catalog entry. -/ +private def depMembers : List (String × String) := [ + ("Batteries", "Batteries"), ("Qq", "Qq"), ("Aesop", "Aesop"), + ("ProofWidgets", "ProofWidgets"), ("Cli", "Cli"), + ("ImportGraph", "ImportGraph"), ("LeanSearchClient", "LeanSearchClient"), + ("Plausible", "Plausible"), ("Mathlib", "Mathlib") ] + +/-- The heavy dependents: small libraries whose closures each contain + all of mathlib. -/ +private def heavyDependents : List (String × String) := [ + ("BET", "BET"), ("GibbsMeasure", "GibbsMeasure"), + ("KolmogorovExtension4", "KolmogorovExtension4") ] + +private def specJson (libs : List (String × String)) : String := + (Lean.Json.mkObj [ + ("prefix", Lean.Json.str "Spine"), + ("libs", Lean.Json.arr <| libs.toArray.map fun (q, r) => + Lean.Json.mkObj [ + ("qualifier", Lean.Json.str q), + ("roots", Lean.Json.arr #[Lean.Json.str r]) ]) ]).pretty + +/-- Run one `ix catalog` leg in a temp dir and return its reported + `peakRssBytes`. -/ +private def runLeg (label : String) (libs : List (String × String)) : + IO (Except String Nat) := do + let dir ← IO.FS.createTempDir + try + let specPath := dir / s!"{label}.json" + let reportPath := dir / s!"{label}-report.json" + let outPath := dir / s!"{label}.ixe" + IO.FS.writeFile specPath (specJson libs) + let exe ← IO.FS.realPath ixExe + let out ← IO.Process.output { + cmd := exe.toString + args := #["catalog", "--spec", specPath.toString, + "--out", outPath.toString, "--report", reportPath.toString] + cwd := some spineDir } + if out.exitCode != 0 then + return .error s!"{label} leg failed ({out.exitCode}): \ +{out.stderr.take 300} … {(out.stdout.takeEnd 300).toString}" + let content ← IO.FS.readFile reportPath + return do + let json ← Lean.Json.parse content + let peak ← (← json.getObjVal? "peakRssBytes").getNat? + if peak == 0 then + throw s!"{label}: peakRssBytes is 0 — RSS sampler unavailable \ +(non-Linux?)" + return peak + finally + IO.FS.removeDirAll dir + +private def spineTest : IO (Bool × Nat × Nat × Option String) := do + unless (← ixExe.pathExists) do + return (false, 0, 0, some s!"{ixExe} missing — run `lake build ix` first") + -- Fetch + build the member libraries. First run needs network and + -- pulls the mathlib olean cache; idempotent afterwards. `cache get` + -- failure is tolerated — the build below is authoritative. + let cacheOut ← IO.Process.output { + cmd := "lake", args := #["exe", "cache", "get"], cwd := some spineDir } + let build ← IO.Process.output { + cmd := "lake" + args := #["build"] ++ (depMembers ++ heavyDependents).toArray.map (·.2) + cwd := some spineDir } + if build.exitCode != 0 then + return (false, 0, 0, some s!"spine workspace build failed \ +(cache get exit {cacheOut.exitCode}): {build.stderr.take 400}") + let basePeak ← match ← runLeg "baseline" depMembers with + | .ok peak => pure peak + | .error e => return (false, 0, 0, some e) + let spinePeak ← match ← runLeg "spine" (depMembers ++ heavyDependents) with + | .ok peak => pure peak + | .error e => return (false, 0, 0, some e) + -- The I1/I8 bound: adding members that share the already-cataloged + -- heavy closure must not multiply the peak. Pre-streaming, three + -- extra mathlib environments held simultaneously put this well + -- above 1.6×. + if spinePeak * 5 ≥ basePeak * 8 then + return (false, spinePeak, basePeak, + some s!"peak RSS {spinePeak} B vs baseline {basePeak} B — over \ +1.6×; shared closures are being held per-member") + return (true, spinePeak, basePeak, none) + +def suite : List TestSeq := [ + .individualIO + "catalog spine: shared mathlib closure peaks ~1×, not ~N× (I8)" + none spineTest .done ] + +end Tests.Ix.CatalogSpine diff --git a/Tests/Main.lean b/Tests/Main.lean index 1e82760b..4183c210 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -57,6 +57,7 @@ import Tests.Ix.Catalog import Tests.Ix.ImportIxe import Tests.Ix.CatalogFixtures import Tests.Ix.CatalogQualified +import Tests.Ix.CatalogSpine import Ix.Common import Ix.Meta import Ix.IxVM @@ -103,6 +104,7 @@ def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ ("shard-map", Tests.ShardMap.suite), ("catalog-fixtures", Tests.Ix.CatalogFixtures.suite), + ("catalog-spine", Tests.Ix.CatalogSpine.suite), ("rust-canon-roundtrip", Tests.CanonM.rustSuiteIO), ("serial-canon-roundtrip", Tests.CanonM.serialSuiteIO), ("parallel-canon-roundtrip", Tests.CanonM.parallelSuiteIO),