ix catalog at corpus scale

Benchmarks/Catalog/RelocFixtureA/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.33.0

Benchmarks/Catalog/RelocFixtureB/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.33.0

Benchmarks/Catalog/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.33.0

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}

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"

Benchmarks/CatalogReal/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.33.0

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}

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"

Benchmarks/CatalogSpine/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0