refactor: single-source reducibility hints in Env::anon_hints by samuelburnham · Pull Request #489 · argumentcomputer/ix

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham · 2026-07-13T20:08:53Z

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.

samuelburnham · 2026-07-13T20:09:42Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:12:31Z

❌ benchmark run failed

Workflow logs

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.

samuelburnham · 2026-07-13T20:26:31Z

!benchmark compile BENCH_ENVS=InitStd,Lean,FLT,Mathlib

argument-ci-bot · 2026-07-13T20:43:22Z

`!benchmark` — main vs `5c619ba`

backends: compile · envs: InitStd,Lean,FLT,Mathlib · set: primary · shard: 0

`compile` · `FLT` — main from: base run @ `83867c8` (not on bencher)

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`	46.252 s	44.438 s	-3.9% 🟢	11.04K	11.49K	+4.1% 🟢	12.39 GiB	12.39 GiB	-0.0%	1.72 GiB	1.72 GiB	-0.0%	510,687	510,687	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `InitStd` — main from: base run @ `83867c8` (not on bencher)

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`	4.356 s	4.019 s	-7.7% (1.08× faster) 🟢	24.22K	26.25K	+8.4% (1.08× faster) 🟢	3.67 GiB	3.70 GiB	+0.7%	309.16 MiB	309.05 MiB	-0.0%	105,492	105,492	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Lean` — main from: base run @ `83867c8` (not on bencher)

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`	7.539 s	7.309 s	-3.1% 🟢	25.07K	25.86K	+3.1% 🟢	4.90 GiB	4.93 GiB	+0.6%	462.76 MiB	462.55 MiB	-0.0%	188,999	188,999	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

`compile` · `Mathlib` — main from: base run @ `83867c8` (not on bencher)

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`	52.618 s	45.647 s	-13.2% (1.15× faster) 🟢	14.00K	16.14K	+15.3% (1.15× faster) 🟢	18.27 GiB	18.44 GiB	+0.9%	2.99 GiB	2.99 GiB	-0.0%	736,618	736,618	+0.0%

1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).

Workflow logs

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.

samuelburnham force-pushed the sb/anon-hints branch from 8074d1b to 97f970fCompare July 13, 2026 20:17

samuelburnham force-pushed the sb/anon-hints branch from 97f970f to 5c619baCompare July 13, 2026 20:20

samuelburnham marked this pull request as ready for review July 13, 2026 20:44

samuelburnham requested a review from johnchandlerburnham July 13, 2026 20:44

samuelburnham merged commit 46a7673 into jcb/ixe-improvementsJul 13, 2026
14 of 15 checks passed

samuelburnham deleted the sb/anon-hints branch July 13, 2026 21:13