Uh oh!
There was an error while loading. Please reload this page.
Ixon: .ixe bundle format and diff tool - #474
Merged
Merged
Conversation
johnchandlerburnhamforce-pushed
the
jcb/ixe-improvements
branch
3 times, most recently
from
July 13, 2026 15:55
683ed55 to
359aeabComparesamuelburnham
previously approved these changes
Jul 13, 2026
Uh oh!
There was an error while loading. Please reload this page.
johnchandlerburnhamforce-pushed
the
jcb/ixe-improvements
branch
from
July 13, 2026 17:03
359aeab to
83867c8Comparejohnchandlerburnham
commented
Jul 13, 2026
MemberAuthor
!benchmark compile |
johnchandlerburnham
enabled auto-merge (squash)
July 13, 2026 17:05
Contributor
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 3.936 s | 4.486 s | +14.0% (1.14× slower) | 26.80K | 23.52K | -12.3% (1.14× slower) | 3.64 GiB | 3.59 GiB | -1.3% | 306.43 MiB | 309.16 MiB | +0.9% | 105,492 | 105,492 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
samuelburnham
commented
Jul 13, 2026
Member
!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib |
Contributor
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT | 42.726 s | 47.188 s | +10.4% (1.10× slower) | 11.95K | 10.82K | -9.5% (1.10× slower) | 12.33 GiB | 12.50 GiB | +1.4% | 1.70 GiB | 1.72 GiB | +0.8% | 510,687 | 510,687 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · InitStd — main from: bencher @ c8b5e47
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 3.936 s | 4.486 s | +14.0% (1.14× slower) | 26.80K | 23.52K | -12.3% (1.14× slower) | 3.64 GiB | 3.59 GiB | -1.3% | 306.43 MiB | 309.16 MiB | +0.9% | 105,492 | 105,492 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · Lean — main from: bencher @ c8b5e47
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean | 6.929 s | 7.290 s | +5.2% (1.05× slower) | 27.28K | 25.93K | -5.0% (1.05× slower) | 4.97 GiB | 4.96 GiB | -0.1% | 458.03 MiB | 462.76 MiB | +1.0% | 188,999 | 188,999 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · Mathlib — main from: bencher @ c8b5e47
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 48.420 s | 49.268 s | +1.8% | 15.21K | 14.95K | -1.7% | 18.34 GiB | 18.40 GiB | +0.3% | 2.97 GiB | 2.99 GiB | +0.6% | 736,618 | 736,618 | +0.0% |
1 env · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
samuelburnham
commented
Jul 13, 2026
Member
!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib |
Contributor
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT | 44.314 s | 45.559 s | +2.8% | 11.52K | 11.21K | -2.7% | 12.57 GiB | 12.43 GiB | -1.1% | 1.70 GiB | 1.72 GiB | +0.7% | 510,687 | 510,687 | +0.0% |
1 env · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · InitStd — main from: bencher @ 3a0817f
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 3.916 s | 4.033 s | +3.0% | 26.94K | 26.16K | -2.9% | 3.68 GiB | 3.62 GiB | -1.6% | 306.43 MiB | 309.05 MiB | +0.9% | 105,492 | 105,492 | +0.0% |
1 env · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · Lean — main from: bencher @ 3a0817f
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean | 6.558 s | 6.927 s | +5.6% (1.06× slower) | 28.82K | 27.28K | -5.3% (1.06× slower) | 4.91 GiB | 4.85 GiB | -1.3% | 458.03 MiB | 462.55 MiB | +1.0% | 188,999 | 188,999 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
compile · Mathlib — main from: bencher @ 3a0817f
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 45.269 s | 51.564 s | +13.9% (1.14× slower) | 16.27K | 14.29K | -12.2% (1.14× slower) | 18.74 GiB | 18.49 GiB | -1.3% | 2.97 GiB | 2.99 GiB | +0.6% | 736,618 | 736,618 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
…tions, blob integrity Evolves .ixe in place (Tag4(0xE,0) kept, pre-alpha) so a single env file can pin one Lean value as a self-contained bundle: - Header gains main : Option Address (bundle root; writers and all readers enforce main ∈ consts) and a strictly-ascending assumptions list (thin-bundle trust boundary; merkle_root_canonical over the leaves reproduces Claim.assumptions roots). - Sections reordered hot-first: blobs, consts, anon_hints, names, named, comms. get_anon/get_anon_mmap stop after §3 (no metadata parse-and-discard); parse_lazy_index stops after §5; the full readers reject trailing bytes. - anon_hints promoted from optional trailer to an always-written §3, derived from Named Def metadata when the map is empty; read-time hint harvesting removed (EnvHandle::from_bytes post-pass dropped). - Blob entries are hash-verified in every reader on both sides (a swapped blob silently changed a Nat/String literal before); Lean getEnv also gains the const hash check it was missing. - New Env::bfs_closure follows all three edge kinds (Constant.refs, Prj→block, Muts→member/ctor projections — a refs-only walk returns just the root for projections); prune_to_closure builds bundles (value closure + named-metadata pruning: name parent chains and string blobs, DataValue payload blobs, meta_refs edges, aux_gen originals, per-const hints); validate_closed is the receiver check. kernel::anon_work::closure_addrs now delegates to bfs_closure. - Lean topologicalSortNames emits the anonymous name at index 0, matching Rust: serEnv and rsSerEnv are now byte-identical (verified byte-exact on a 505 MB whole-stdlib env) and the putIdx getD-0 fallback now resolves to anon instead of colliding with the first real name. - FFI mirrors: RawEnv carries main/assumptions/anonHints (ctor arity 5→8), RawEnvLazy carries main/assumptions (3→5); the manual RawEnv builders in ffi compile.rs populate the new slots via set_raw_env_bundle_fields. - Generators/fixtures content-address blobs and exercise the bundle fields; tampering tests compute offsets programmatically instead of hardcoding the header layout; docs/Ixon.md spec updated.
lake exe ix diff <old.ixe> <new.ixe> [--anon|--meta] [--verbose] compares two serialized environments and exits 0/1/2 (GNU diff convention). Engine (crates/ixon/src/diff.rs, host-gated like prune_to_closure): - diff_envs(a, b, meta): named join on Name (added/removed/changed/ meta-only), consts/blobs set diffs, comms join, main/assumptions, hints joined on shared consts. Deterministic ordering. - exprs_equal: iterative lockstep walk resolving Share/Sort/Ref/Str/ Nat/Prj indices through each side's own Constant tables (same bytes + different tables => different; permuted tables with equal resolution => equal), pointer-pair memoized, cycle-guarded. - Per-kind field classification (type/value/lvls/safety/rules[i].rhs/ ctors[j].*, ...); kind changes label "kind"; representation-only address churn labels "encoding". Projections descend one level into their Muts block: changed member => block.* labels, untouched member => "block-siblings". - Default anon mode compares only anonymous structure (hints included: they live in anon §3); meta mode also compares ConstantMeta/original per component. FFI: rs_diff_envs (ByteArray -> ByteArray -> Bool -> Except String EnvDiff) parses both inputs with the full reader (Named.original participates) and marshals EnvStats/NamedDiff/EnvDiff (lean.rs layouts num_64:4 / num_obj:7 / num_obj:17); names cross pre-rendered and pre-sorted, addresses raw. Tests: 15 engine unit tests (refs-shift guard, share-vs-inline, univ-table shift, memo-clearing regression, block descent, ...) and 12 Lean FFI tests incl. self-diff-empty properties over genRawEnv in both modes.
diff_envs_with adds a JoinProgress callback (fires every 100k named-join entries and once at completion); diff_envs delegates with a no-op. rs_diff_envs reports phases to stderr ([rs_diff_envs] ..., the rs_compile_env idiom): per-env parse timings with reader label and live join progress — emitted only when an input is >= 100 MB, so unit tests, property tests, and small bundles stay silent. Anon mode (the default) now loads both envs via parse_lazy_index + Env::from_lazy_index — constant byte-windows, name->addr, verbatim §3 hints, §6 comms — never materializing ConstantMeta. Two full-reader mathlib envs OOM a 124 GiB machine; the lazy path diffs two 3.2 GB mathlib envs in ~62 s at 54 GiB peak with identical output (locked by a lazy/full parity test). --meta keeps the full reader, since Named.meta/original are the point of that mode. parse_lazy_index now carries §3 hints and §6 comms verbatim on LazyIndex (both tiny) and, since it consumes every section, enforces EOF exactly like Env::get. Mathlib-scale validation (v4.29.0 tag vs 8850ed93, 5 days of master): 3763 added / 1522 removed / 143528 changed names over 744k joined, exit 1, deterministic — zero [encoding] entries; 5 genuine kind changes and 1 hint change surface above the content-address ripple.
`lake exe ix pack <env.ixe> <name>` prunes a serialized env to the self-contained bundle pinning one named constant and writes it as a standalone .ixe — the first production consumer of Env::prune_to_closure (sets main, records reached cut-points in assumptions, carries display metadata to fixpoint) followed by the receiver-side Env::validate_closed. - New FFI rs_pack_env (crates/ffi/src/lean_ixon/pack.rs), mirroring the rs_env_extract read→resolve→write shape: full reader, displayed name→address resolution over env.named, --assume entries resolving as names first then 64-hex addresses. - New Ix/Cli/PackCmd.lean: --assume/--assume-file (ConstsFile.gather), --out (default <name>.ixe), --verbose; exit 0/1. - Tests/FFI/Ixon.lean: six directed IO tests over a temp-file fixture (closure bundle, removals-only diff subset, name and hex assume cuts, unknown-root and main-assumed errors). The fixture stores name-string blobs via addNameComponentsWithBlobs — the compiler convention prune_to_closure recreates via carry_name. - docs/Ixon.md: pack workflow in the bundle section. E2E: Nat.add out of the 324 MB stdlib env → 13 KB closed bundle (17 consts, 43 blobs) in ~4 s; --assume Nat drops the cut constant and records 1 assumption.
One edited constant re-addresses its whole reverse-dependency cone, so
a content-addressed diff drowns the human edits in transitive
re-addressings. Every changed row now carries a verdict: after the
named join, pass 2 re-classifies each changed pair under a quotient
where an (old, new) address pair compares equal when some changed name
maps old→new. Rows whose residual labels are all "encoding" /
"block-siblings" are rippled (fully explained by dependency
re-addressing); the rest are roots. A single-level map is complete
because expression comparison only consults immediate-dependency
addresses — composition happens through per-row verdicts.
Engine (ixon::diff): set-valued AddrMap built in the join loop (kind
and encoding rows included; tolerates name splits); ExprCmp/classify
parameterized by Option<&AddrMap> at the three address sites
(Ref/Str+Nat/Prj-expr); classify_prj block short-circuit stays strict
== and always descends (blocks are unnamed — a mapped shortcut would
hide block-internal roots); pass-2 verdict cache keyed on the (old,
new) pair so alias rows share one computation; constants re-parse
rather than stash (LazyConstant no-cache policy keeps peak RSS flat).
JoinProgress gains DiffPhase {NamedJoin, RippleClassify} with a 10k
ripple stride. NamedChange.rippled crosses the FFI as a num_8 scalar
(fresh scalar region; obj slots untouched).
CLI: the counts line reports "(N roots, M rippled)"; the default
listing shows roots only (plus, under --meta, rippled rows carrying
metadata edits — namedMetaOnly only covers same-addr rows); --verbose
lists rippled rows with a " (rippled)" suffix.
Documented semantic edges: induced re-elaboration (a dependency
universe/arity change alters dependents beyond addresses) verdicts
root; an intrinsically edited block member with no named projection
has no root row; the "block" fallback on assumption-cut bundles
verdicts root — all fail-safe over-reports.
Tests: 14 new engine tests (two-hop chain, block-ctor edit descent,
name splits, kind-row mapping, univ-arity root, renamed dep, literal
root, encoding ripple, alias cache, Prj-expr site, cidx root, …);
join-progress test now asserts per-phase; Lean FFI marshaling tests
pin the num_8 slot.
Mathlib validation (v4.29.0 ↔ 8850ed93, 744k joined names): 143,528
changed → 4,516 roots / 139,012 rippled (96.9% explained). All 5 kind
changes, all 245 lvls signature changes, and 8 genuine ctor-type edits
surface as roots; 605 induced block.ctor.type rows correctly ripple;
zero rippled rows carry scalar labels; deterministic across runs.
Ripple pass +16.5s (compute 30.8s vs 14.3s), peak RSS unchanged at
54 GiB.…diff
--meta at mathlib scale previously OOM'd a 124 GiB machine (the full
reader materializes every ConstantMeta on both sides). It now runs in
8 GiB peak / 67 s on the 744k-name mathlib pair.
Streaming §5 sweep: both modes load via the lazy index; meta mode
additionally merge-joins the two files' §5 named sections with a pair
of streaming cursors (NamedMetaCursor), parsing each side's entry
against its own §4 reverse index, comparing, and dropping — resident
metadata is O(1) instead of everything-at-once. Raw §5 byte windows
are NOT comparable across files (metadata name references are
file-relative §4 indices; identical metadata serializes to different
bytes over different name tables), so the sweep compares parsed,
Address-valued ConstantMeta — pinned by a §4 index-shift soundness
regression test and full-reader parity tests. §5 arrives in ascending
name-hash order in both files (exactly Name's Ord), which makes the
lockstep merge-join sound. LazyIndex now records the §5 offset and
retains the §4 reverse index (~32 B/name); parse_lazy_index is
otherwise unchanged.
Engine API: diff_env_bytes (bytes-level, both modes lazy) and
diff_envs_lazy over LazySide {env, index, data}; diff_envs/
diff_envs_with keep the in-env metadata path for materialized envs.
DiffPhase gains MetaSweep (progress: "meta sweep: N/M (K differing)").
Mmap path FFI: rs_diff_env_files mmaps both files
(Env::from_lazy_index_mmap keeps constant windows as zero-copy mmap
slices via store_const_lazy_mmap) and rs_ixe_files_equal does the
byte-equal fast path (metadata length check, then mmap memcmp). The
CLI no longer reads files into Lean ByteArrays at all. The
ByteArray-based rs_diff_envs stays for property tests, now also on
the lazy path in both modes.
Mathlib validation (v4.29.0 ↔ 8850ed93): --meta completes at 8 GiB
peak / 67 s wall (sweep finds 7,998 differing names → 867
metadata-only rows + 7,131 changed rows with meta labels; structural
counts identical to anon: 143,528 changed, 4,516 roots). Anon through
the path FFI: 8 GiB peak (was 54 GiB heap-resident), report
byte-identical to the ByteArray-path baseline. Identical-file fast
path on a 3 GB input: 1.5 s.
docs/Ixon.md gains a "Diffing environments" section (semantics,
root/rippled, memory model).Pack no longer uses the full reader. The source env is memory-mapped and lazily loaded (constant windows stay zero-copy mmap slices), and display metadata is carried by re-streaming §5 with a NamedMetaCursor once per prune fixpoint round, materializing Named entries only for carried constants — resident metadata is O(survivors) instead of O(env). Packing Euclid out of the 3.2 GB mathlib env: 22 s / 5.3 GiB peak (was ~60 s at full-reader tens-of-GiB), output byte-identical to the full-reader bundle. Engine: prune_to_closure refactored into prune_init + prune_value_pass + carry_named_entry (the named-pass body, parameterized over name/blob resolvers) — prune_to_closure_streaming shares it verbatim, so the in-memory and streaming paths cannot drift; a byte-identity test (with an aux-original fixture forcing a second fixpoint round, a §4-resolved binder name, and a meta_refs blob) locks it. parse_lazy_index_with_names returns the §4 Address→Name lookup the walk already builds (the plain variant keeps dropping it). --anon packs only anonymous structure via prune_to_closure_anon: value closure + §3 hints, empty §4/§5 — the minimal artifact a receiver needs to typecheck/evaluate the pinned value (validate_closed checks the value pin only). Anon Euclid: 2.5 MB vs 13 MB (3,138 consts, 89 value blobs vs 9,504 with name strings), 13.6 s. FFI rs_pack_env: mmap + lazy load, gains the anon flag (arity 5→6); mmap_file shared with the diff module. CLI: ix pack --anon. Tests: streaming/full byte parity (+ assumed-cut variant), anon value-only contents + roundtrip, Lean FFI anon-bundle fixture; 249 ixon tests, workspace + ffi/ixon suites green.
Remove the hints field from ConstantMeta::Def (Rust, Lean, the FFI constructor slots, and the .ixe named-section encoding). Reducibility hints now live only in the env-level anon_hints map, keyed by constant address. - The compiler is the sole producer: compile_definition records each definition's hints per name (CompileState::def_hints), and finalize_hints resolves them through the registered Named entries into env.anon_hints via Env::register_hint once addresses are final. The Lean compiler mirror (BlockState.defHints + Ixon.mergeHints) does the same. Alias collisions merge order-independently (min by (tag, height)), so parallel workers and both mirrors agree byte-for-byte. - Writers serialize the map directly; the derive-from-Named fallback is deleted from Env::put / put_file / serialized_size_breakdown and both Lean writers. This removes the serial full-decode of every demoted Named entry that regressed ix compile by 5-14%: the derivation loop called Named::meta() per entry, which re-decodes demoted metadata (the IX_COMPILE_DEMOTE default) on every call. - Kernel ingress reads hints from anon_hints in both anon and meta modes; the hints_override parameter threading is gone. Decompile (both languages) and the IxVM claim harness look hints up by address. The lazy check path transports the hints section on RawEnvLazy instead of fabricating per-name Def metas (RawNamedLite.toConstMeta is removed). - anon_hints becomes an IxonMap like the other env maps; Env now derives Clone (the riscv64 IxonMap wrapper gained Clone, replacing the manual per-map Clone impl). Format change (pre-alpha, no compat shims): Def metadata loses its hints byte in the named sections, so every hint is stored once instead of two or three times (hints section + named meta + aux originals) — the whole-stdlib env shrinks by ~232 KB. InitStd compile-time returns to its pre-hints-section cost (median 7.3s -> 5.7s locally vs the derivation code), with byte-exact Lean/Rust writer parity at 505,674,085 bytes on the whole-stdlib env. Behavior note: a hint-only change now reports as a pure hintsChanged row in ix diff; it previously also surfaced as a Def metadata diff.
samuelburnhamforce-pushed
the
jcb/ixe-improvements
branch
from
July 13, 2026 21:43
46a7673 to
250277dComparesamuelburnham
commented
Jul 13, 2026
Member
!benchmark compile BENCH_ENVS=InitStd,Mathlib |
Contributor
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd | 3.916 s | 3.694 s | -5.7% (1.06× faster) 🟢 | 26.94K | 28.56K | +6.0% (1.06× faster) 🟢 | 3.68 GiB | 3.64 GiB | -0.9% | 306.43 MiB | 309.05 MiB | +0.9% | 105,492 | 105,492 | +0.0% |
1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
compile · Mathlib — main from: bencher @ 3a0817f
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (main) | throughput (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib | 45.269 s | 46.926 s | +3.7% | 16.27K | 15.70K | -3.5% | 18.74 GiB | 18.59 GiB | -0.8% | 2.97 GiB | 2.99 GiB | +0.6% | 736,618 | 736,618 | +0.0% |
1 env · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
arthurpaulino
approved these changes
Jul 14, 2026
Uh oh!
There was an error while loading. Please reload this page.
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 freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
Two related changes
.ixebundle format (a single env file that pins one Lean value as a self-contained, verifiable unit — the groundwork for Ixon as a client/server interchange format), plus its first producer CLI,ix packix diff— a structured, content-address-aware diff of two.ixeenvironments, with ripple root-causing (separating intrinsic edits from the content-address ripple) and a memory-lean--meta, validated at mathlib scale.Part 1 —
.ixebundle formatEvolves the format in place (pre-alpha, Tag4(0xE,0) kept, no compat shims). A constant's address already pins its entire dependency DAG (refs tables are content addresses, recursively); this adds the transport half: a distinguished root, an explicit trust boundary for thin bundles, and closure helpers to produce/validate them.
get_anon/get_anon_mmapread §1–§3 and stop — no more parse-and-discard of names/named/comms; the full readers reject trailing bytes.merkle_root_canonical(assumptions)reproducesClaim.assumptionsroots, so claim interop is derivable, not stored.getEnvalso gains the per-const hash check it was missing.Env::bfs_closure(3-edge traversal: refs, projection →Mutsblock, block → member/ctor projection addresses),Env::prune_to_closure(main, assumed)(minimal closed bundle incl. display metadata),Env::validate_closed()(receiver check).kernel::anon_work::closure_addrsnow delegates tobfs_closure.putIdxgetD 0collision). Now locked by strictserEnv == rsSerEnvtests — byte-exact at 505,759,024 bytes on the whole-stdlib env.ix pack— producing bundlesThe first production consumer of
prune_to_closure: resolves<name>(displayed form) against the env'snamedtable, prunes to the self-contained closure —mainset, reached cut points recorded inassumptions, display metadata carried to fixpoint — re-validates withvalidate_closed, and writes the bundle (default<name>.ixe).--assumeentries (names or 64-hex constant addresses) declare thin-bundle trust boundaries. Euclid's theorem out of the 3.2 GB mathlib env:3,138 constants (0.5% of mathlib), 13 MB, closed by construction —
main's 32 bytes alone pin the value. (ix shard extractremains the non-bundle sibling: a general sub-env for the kernel-check pipeline, nomainroot.) Pack v1 reads with the full reader so metadata survives the prune; the 3.2 GB parse dominates its runtime — a leaner selective-metadata pack is future work on the §5 streaming machinery from Part 2.Part 2 —
ix diffContent-addressing frames the semantics: a name "changed" ⇔ its constant address changed, and value-equality coincides with address-equality — so the interesting work is saying what changed, honestly.
Exit codes follow GNU diff: 0 = no difference (in the selected mode), 1 = differences, 2 = error. Byte-equal files short-circuit to
identicalwithout parsing (mmap memcmp; 1.5 s on a 3 GB input).Modes
--anon(default): compares only anonymous structure — name→addr changes with per-field classification, consts/blobs set differences, comms,main/assumptions, and reducibility hints (they live in anon §3 and drive kernel unfolding). Names are join/display keys only.--meta: additionally comparesNamedmetadata per component (meta.infowith kind transitions,meta.sharing/refs/univs,original.added/removed/addr/meta) — a same-addr metadata-only change is its own report category.Field-level classification (Rust engine,
ixon::diff)exprs_equalis an iterative lockstep walk that resolvesShare/Sort/Ref/Str/Nat/Prjindices through each side's own constant tables: identical expr bytes over different refs tables compare different; permuted tables with equal resolution compare equal. Pointer-pair memoized (shared subterms don't re-walk),Share-cycle-guarded, no recursion (kernel terms nest thousands deep).type,value,lvls,safety,rules[i].rhs,ctors[j].type, …). Kind changes reportkind; an address change with no detected semantic difference reportsencoding(representation churn) — never an empty list.Mutsblocks behind projections, so "block changed" alone would gut the tool. Same-kind projections with a changed block descend one level: changed member →block.*labels; untouched member →block-siblings(the block hash moved because a sibling changed — the common, most informative case).Ripple root-causing (root vs rippled)
One edited constant re-addresses its whole reverse-dependency cone, so a content-addressed diff drowns the human edits in transitive re-addressings. Every changed row now carries a verdict: after the join, a second pass re-classifies each changed pair under a quotient where an (old, new) address pair compares equal when some changed name maps old→new. Rows whose residual labels are all
encoding/block-siblingsare rippled — fully explained by their dependencies' re-addressing; the rest are roots (intrinsic edits). A single-level map is complete because expression comparison only ever consults immediate-dependency addresses — composition across the DAG happens through the per-row verdicts, neverM∘M.fieldskeeps the strict classification;rippled : Boolis the orthogonal verdict. The default listing shows roots (plus, under--meta, rippled rows carrying metadata edits);--verboselists everything.iprj→defnrefactor's dependents still ripple.block.ctor.type), its untouched siblings ripple, and blocks themselves (unnamed) never enter the map — descent is mandatory or block-internal roots would vanish.blockfallback on assumption-cut bundles verdicts root.LazyConstantno-cache policy keeps memory flat). The pass costs ~one extra classify sweep (+16 s at mathlib scale).Memory:
--metawithout the OOM, and an mmap fast pathThe first
--metadesign read both envs with the full reader — at mathlib scale that materializes everyConstantMetatwice and OOM'd a 124 GiB machine. Both modes now load via the lazy index, and meta mode compares metadata by streaming both files' §5 named sections in a lockstep merge-join (§5 is written in ascending name-hash order — exactlyName'sOrd— in every file): parse one entry per side against its own §4 reverse index, compare, drop. Resident metadata is O(1) instead of everything-at-once.Raw §5 byte windows are not comparable across files — metadata name references are file-relative §4 indices, so identical metadata serializes to different bytes over different name tables. The sweep therefore compares parsed, Address-valued
ConstantMeta(index-independent), pinned by a §4 index-shift soundness regression test and full-reader parity tests.The CLI also stopped reading files into Lean
ByteArrays entirely:rs_diff_env_filesmmaps both inputs (constant windows stay zero-copy mmap slices backed by the OS page cache) andrs_ixe_files_equaldoes the byte-equal fast path. Anon mode dropped from 54 GiB heap-resident to 8 GiB peak with a byte-identical report.Progress reporting
Large inputs (≥ 100 MB) stream progress to stderr (stdout stays clean for piping): per-env parse timings, then live per-phase events — meta sweep (meta mode), named join, ripple pass:
Mathlib-scale validation
Diffed the
v4.29.0tag env against8850ed93(the last mathlib master commit on the v4.29.0 toolchain — 5 days of master; theBenchmarks/Compilepin is bumped accordingly): two 3.2 GB envs, 744k named join. **Anon: 65 s wall, 8 GiB peak.--meta: 67 s, 8 GiB[type, value]+ 15,834[value]pure re-addressings.CategoryTheory.Classifier/HasClassifieriprj→defn,OmegaCompletePartialOrder.Chaindefn→iprj,RecursiveIn/.oracledestructured), all 245 universe-signature changes ([lvls, type, value]), and 8 genuine constructor edits (e.g.LinearPMap.mkgainingblock.ctor.lvls/params/type). The 613block.ctor.typerows the strict classifier had surfaced turn out to be 8 real edits + 605 induced re-addressings — exactly the noise/signal split the verdict exists for.--metaadditionally finds 7,998 names with differing metadata: 867 metadata-only rows (same address — binder/arena edits like…._proof_1 [meta.info]) and 7,131 changed rows with meta labels.[encoding]entries — compilation is deterministic end-to-end.abbrev → regular(2)) on an otherwise-unchanged constant, correctly absent from the named rows (hints live in §3 and don't re-address constants).Breaking change
All existing
.ixefiles are stale — regenerate withix compile(readers emit a "pre-bundle-format .ixe; recompile it" hint). FFIRawEnvctor arity is 5→8,RawEnvLazy3→5;NamedDiffgains arippled : Boolscalar field.Verification
--all-featuresclean.ixonat 247 tests; the diff engine alone carries 34 (refs-shift guard, share-vs-inline, univ-table shift, memo-clearing regression, block descent, lazy/full parity, per-phase progress totals, 14 ripple-verdict tests incl. two-hop chains / name splits / renamed deps / induced re-elaboration, §5-sweep parity vs the full reader, the §4 index-shift soundness regression, mmap-side parity).lake testgreen; FFI tests incl. self-diff-empty properties over generated envs in both modes (pins marshaling slot order), a ripple-verdict marshaling test (pins thenum_8slot), file-based-vs-bytes-based diff parity, and sixix packfixtures (closure bundle, removals-only diff subset, name/hex--assumecuts, error paths).ix check-rs60,601/60,601 (meta) and 51,681/51,681 (anon);bench-typecheckexecutes and proves over the new format.Follow-ups
prune_to_closurerescansenv.namedper fixpoint round — worth a reverse index if bulk pruning against mathlib-scale envs becomes common; the same §5 streaming machinery would also letix packskip the full-reader parse.