`ix catalog` at corpus scale - #584

Merged

johnchandlerburnham merged 12 commits into

mainfrom

jcb/catalog-scale

Aug 21, 2026

Commits on Aug 20, 2026

catalog: pin loader imports to OLeanLevel.private + level-regression gates
johnchandlerburnham
committed
70db405
catalog: fail closed on un-replayed cross-package roots
johnchandlerburnham
committed
addf342
catalog: stream member environments — load, stage, free, one at a time
johnchandlerburnham
committed
4a615f8
bench: refresh CatalogReal member pins for Lean v4.33.0
johnchandlerburnham
committed
6f95e51
catalog: harden the region-evicting copier at real-library scale
johnchandlerburnham
committed
49c2836
catalog: `--spec` file input for ix catalog
johnchandlerburnham
committed
62cb4ad
catalog: `--audit-only` subset gating + peak RSS in `--report`
johnchandlerburnham
committed
5a95dea
catalog: hash-cons the region-evicting copy
johnchandlerburnham
committed
9bab965
catalog: bound staging at mathlib scale — per-decl caches, copy/share hybrid, unconditional replay
johnchandlerburnham
committed
1e1c68d

Commits on Aug 21, 2026

bench: mathlib-spine catalog with a peak-RSS gate
johnchandlerburnham
committed
6d90645
Merge branch 'main' into jcb/catalog-scale
johnchandlerburnham
committed
f669f9a
Merge branch 'main' into jcb/catalog-scale
johnchandlerburnham
committed
80a552a