Recover Ixon v3 compilation and anonymous kernel-check performance - #639
Conversation
|
!benchmark fresh |
|
!benchmark compile fresh |
|
!benchmark ooc fresh |
|
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
7.044 s | 7.167 s | +1.7% | 58.508 s | 47.448 s | -18.9% (1.23× faster) 🟢 | 47.430 | 58.480 | +23.3% (1.23× faster) 🟢 | 69.32 GiB | 69.38 GiB | +0.1% | 4.98 MiB | 4.98 MiB | +0.0% | 26.5 ms | 27.1 ms | +2.3% | 126.40B | 126.40B | +0.0% |
Char.ofOrdinal_le_of_le |
4.981 s | 5.292 s | +6.2% (1.06× slower) |
38.954 s | 39.201 s | +0.6% | 70.930 | 70.480 | -0.6% | 59.82 GiB | 59.85 GiB | +0.0% | 4.95 MiB | 4.95 MiB | +0.0% | 26.3 ms | 25.5 ms | -2.8% | 90.44B | 90.44B | +0.0% |
Array.extract_append |
5.060 s | 6.434 s | +27.1% (1.27× slower) |
35.576 s | 36.825 s | +3.5% |
45.140 | 43.610 | -3.4% |
51.54 GiB | 51.58 GiB | +0.1% | 4.82 MiB | 4.82 MiB | +0.0% | 26.2 ms | 24.7 ms | -5.7% (1.06× faster) 🟢 | 92.32B | 92.32B | +0.0% |
Std.HashMap |
3.098 s | 3.981 s | +28.5% (1.29× slower) |
23.047 s | 24.013 s | +4.2% |
88.600 | 85.040 | -4.0% |
34.79 GiB | 34.72 GiB | -0.2% | 4.89 MiB | 4.89 MiB | +0.0% | 25.3 ms | 25.7 ms | +1.7% | 57.73B | 57.73B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
2.808 s | 2.838 s | +1.1% | 22.049 s | 21.976 s | -0.3% | 84.670 | 84.960 | +0.3% | 33.57 GiB | 33.49 GiB | -0.2% | 4.86 MiB | 4.86 MiB | +0.0% | 25.6 ms | 25.8 ms | +0.9% | 52.70B | 52.70B | +0.0% |
String.append |
459.8 ms | 445.3 ms | -3.2% 🟢 | 2.673 s | 2.677 s | +0.2% | 122.330 | 122.130 | -0.2% | 5.76 GiB | 5.80 GiB | +0.7% | 4.62 MiB | 4.62 MiB | +0.0% | 23.3 ms | 23.1 ms | -0.9% | 3.22B | 3.22B | +0.0% |
Nat.add_comm |
286.6 ms | 361.4 ms | +26.1% (1.26× slower) |
1.059 s | 1.019 s | -3.8% 🟢 | 43.450 | 45.160 | +3.9% 🟢 | 4.07 GiB | 4.42 GiB | +8.6% (1.09× larger) |
4.43 MiB | 4.43 MiB | +0.0% | 23.8 ms | 24.6 ms | +3.7% |
286.99M | 286.99M | +0.0% |
FRI verifier on FRI (7 constants)
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
2.193 s | 2.373 s | +8.2% (1.08× slower) |
31.861 s | 32.016 s | +0.5% | 87.100 | 86.670 | -0.5% | 51.74 GiB | 51.51 GiB | -0.4% | 2.01 MiB | 2.01 MiB | +0.0% | 10.7 ms | 10.6 ms | -1.1% | 91.59B | 91.59B | +0.0% |
Char.ofOrdinal_le_of_le |
2.180 s | 2.198 s | +0.8% | 31.341 s | 31.667 s | +1.0% | 88.160 | 87.250 | -1.0% | 51.42 GiB | 51.49 GiB | +0.1% | 2.02 MiB | 2.02 MiB | +0.0% | 11.3 ms | 10.8 ms | -4.7% 🟢 | 90.08B | 90.08B | +0.0% |
Array.extract_append |
2.255 s | 2.301 s | +2.0% | 30.789 s | 30.922 s | +0.4% | 52.160 | 51.940 | -0.4% | 49.02 GiB | 49.07 GiB | +0.1% | 2.00 MiB | 2.00 MiB | +0.0% | 10.8 ms | 10.9 ms | +0.7% | 87.98B | 87.98B | +0.0% |
Std.HashMap |
2.322 s | 2.196 s | -5.4% (1.06× faster) 🟢 | 31.553 s | 31.452 s | -0.3% | 64.720 | 64.920 | +0.3% | 49.38 GiB | 50.11 GiB | +1.5% | 2.00 MiB | 2.00 MiB | +0.0% | 10.5 ms | 10.4 ms | -0.9% | 89.59B | 89.59B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
2.290 s | 2.178 s | -4.9% (1.05× faster) 🟢 | 31.127 s | 31.161 s | +0.1% | 59.980 | 59.910 | -0.1% | 49.09 GiB | 49.84 GiB | +1.5% | 2.01 MiB | 2.01 MiB | +0.0% | 11.5 ms | 11.3 ms | -2.1% | 89.14B | 89.14B | +0.0% |
String.append |
2.126 s | 2.174 s | +2.2% | 30.112 s | 30.266 s | +0.5% | 10.860 | 10.800 | -0.6% | 46.32 GiB | 45.90 GiB | -0.9% | 2.01 MiB | 2.01 MiB | +0.0% | 11.2 ms | 10.9 ms | -2.1% | 81.80B | 81.80B | +0.0% |
Nat.add_comm |
1.872 s | 1.877 s | +0.2% | 29.803 s | 29.804 s | +0.0% | 1.540 | 1.540 | +0.0% | 45.19 GiB | 44.74 GiB | -1.0% | 2.01 MiB | 2.01 MiB | +0.0% | 11.0 ms | 10.6 ms | -3.7% 🟢 | 74.30B | 74.30B | +0.0% |
Aggregate flat join (7 constants)
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Char.ofOrdinal_le_of_le |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Array.extract_append |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Std.HashMap |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
String.append |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Nat.add_comm |
n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a | n/a |
Pipeline total (7 constants)
| constant | total-time (main) | total-time (PR) | Δ% | pipeline-throughput (const/s) (main) | pipeline-throughput (const/s) (PR) | Δ% | pipeline-peak-ram (main) | pipeline-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
1m 30.4s | 1m 19.5s | -12.1% (1.14× faster) 🟢 | 30.710 | 34.920 | +13.7% (1.14× faster) 🟢 | 69.32 GiB | 69.38 GiB | +0.1% |
Char.ofOrdinal_le_of_le |
1m 10.3s | 1m 10.9s | +0.8% | 39.310 | 38.990 | -0.8% | 59.82 GiB | 59.85 GiB | +0.0% |
Array.extract_append |
1m 6.4s | 1m 7.7s | +2.1% | 24.200 | 23.710 | -2.0% | 51.54 GiB | 51.58 GiB | +0.1% |
Std.HashMap |
54.599 s | 55.465 s | +1.6% | 37.400 | 36.820 | -1.6% | 49.38 GiB | 50.11 GiB | +1.5% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
53.176 s | 53.137 s | -0.1% | 35.110 | 35.140 | +0.1% | 49.09 GiB | 49.84 GiB | +1.5% |
String.append |
32.785 s | 32.944 s | +0.5% | 9.970 | 9.930 | -0.4% | 46.32 GiB | 45.90 GiB | -0.9% |
Nat.add_comm |
30.862 s | 30.822 s | -0.1% | 1.490 | 1.490 | +0.0% | 45.19 GiB | 44.74 GiB | -1.0% |
|
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ISLB |
37.366 s | 19.547 s | -47.7% (1.91× faster) 🟢 | 5.80K | 11.09K | +91.2% (1.91× faster) 🟢 | 5.37 GiB | 5.37 GiB | -0.0% | 515.85 MiB | 515.85 MiB | +0.0% | 216,785 | 216,785 | +0.0% |
compile · InitStd — main from: base run @ bcc6995 (fresh — bencher bypassed)
1 env · 1 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
InitStd |
24.985 s | 12.684 s | -49.2% (1.97× faster) 🟢 | 4.69K | 9.23K | +97.0% (1.97× faster) 🟢 | 3.84 GiB | 3.96 GiB | +3.1% |
326.91 MiB | 326.91 MiB | +0.0% | 117,084 | 117,084 | +0.0% |
compile · Lean — main from: base run @ bcc6995 (fresh — bencher bypassed)
1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean |
37.480 s | 20.991 s | -44.0% (1.79× faster) 🟢 | 5.51K | 9.84K | +78.6% (1.79× faster) 🟢 | 5.23 GiB | 5.24 GiB | +0.3% | 484.38 MiB | 484.38 MiB | +0.0% | 206,647 | 206,647 | +0.0% |
compile · Mathlib — main from: base run @ bcc6995 (fresh — bencher bypassed)
1 env · 0 with regressions · 1 with improvements (|Δ| > 3.0% on any metric).
| env | compile-time (main) | compile-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | env-size (main) | env-size (PR) | Δ% | constants (main) | constants (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib |
3m 30.3s | 1m 26.3s | -58.9% (2.44× faster) 🟢 | 3.67K | 8.93K | +143.5% (2.44× faster) 🟢 | 19.09 GiB | 18.94 GiB | -0.8% | 3.11 GiB | 3.11 GiB | +0.0% | 771,129 | 771,129 | +0.0% |
|
| env/constant | check-time (main) | check-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|
InitStd |
12m 53.8s | 8.190 s | -98.9% (94.48× faster) 🟢 | 127.670 | 12.06K | +9348.5% (94.48× faster) 🟢 | 7.62 GiB | 1.75 GiB | -77.1% (4.36× smaller) 🟢 |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
2.531 s | 538.1 ms | -78.7% (4.70× faster) 🟢 | 1.10K | 5.17K | +370.3% (4.70× faster) 🟢 | 3.40 GiB | 3.68 GiB | +8.1% (1.08× larger) |
Array.extract_append |
768.7 ms | 516.2 ms | -32.9% (1.49× faster) 🟢 | 2.10K | 3.12K | +48.9% (1.49× faster) 🟢 | 3.65 GiB | 3.68 GiB | +0.6% |
Char.ofOrdinal_le_of_le |
1.023 s | 272.4 ms | -73.4% (3.76× faster) 🟢 | 2.71K | 10.19K | +275.6% (3.76× faster) 🟢 | 2.86 GiB | 2.94 GiB | +2.6% |
Std.HashMap |
767.5 ms | 266.0 ms | -65.3% (2.89× faster) 🟢 | 2.70K | 7.79K | +188.6% (2.89× faster) 🟢 | 2.58 GiB | 2.94 GiB | +14.0% (1.14× larger) |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
765.7 ms | 264.4 ms | -65.5% (2.90× faster) 🟢 | 2.45K | 7.08K | +189.6% (2.90× faster) 🟢 | 2.61 GiB | 2.94 GiB | +12.7% (1.13× larger) |
Nat.add_comm |
253.4 ms | 253.4 ms | +0.0% | 181.550 | 181.500 | -0.0% | 3.65 GiB | 3.65 GiB | +0.1% |
String.append |
253.6 ms | 253.4 ms | -0.1% | 1.30K | 1.30K | +0.1% | 3.65 GiB | 3.66 GiB | +0.1% |
per-constant drill-down — Σ check 21926.09s → 230.60s (-98.9%), Σ cost -92.9%; 72189 cost mover(s), 220 time-only mover(s)
Each entry is one constant's own check within the whole-env run (deps ingress lazily; each dep is checked in its own entry; entries sum to the env) — not the full-closure scope of the headline --consts measurements.
Cost improvements (counter-backed)
| constant | main | PR | Δtime | Δcost (Zisk) | driver |
|---|---|---|---|---|---|
String.Iterator.next |
542ms | 0.1ms | -100.0% (7899.02× faster) 🟢 | -100.0% (11256.36× fewer) 🟢 | intern -100.0% |
Substring.Raw.Internal.frontImpl |
546ms | 0.1ms | -100.0% (8730.21× faster) 🟢 | -100.0% (10998.49× fewer) 🟢 | intern -100.0% |
String.Iterator.curr |
560ms | 0.1ms | -100.0% (7621.71× faster) 🟢 | -100.0% (10177.90× fewer) 🟢 | intern -100.0% |
String.Internal.frontImpl |
728ms | 0.1ms | -100.0% (11354.75× faster) 🟢 | -100.0% (9929.91× fewer) 🟢 | intern -100.0% |
Substring.Raw.Internal.toStringImpl |
549ms | 0.1ms | -100.0% (6387.48× faster) 🟢 | -100.0% (9293.28× fewer) 🟢 | intern -100.0% |
String.Slice.trim |
751ms | 0.1ms | -100.0% (10845.59× faster) 🟢 | -100.0% (9283.49× fewer) 🟢 | intern -100.0% |
String.Slice.trimRight |
641ms | 0.1ms | -100.0% (9557.68× faster) 🟢 | -100.0% (8165.04× fewer) 🟢 | intern -100.0% |
String.Slice.trimLeft |
646ms | 0.1ms | -100.0% (9918.61× faster) 🟢 | -100.0% (8147.27× fewer) 🟢 | intern -100.0% |
Std.Http.instInhabitedTrailer |
1.74s | 0.1ms | -100.0% (20925.45× faster) 🟢 | -100.0% (8130.46× fewer) 🟢 | intern -100.0% |
Std.Http.Headers.instUnion |
1.03s | 0.1ms | -100.0% (10882.55× faster) 🟢 | -100.0% (7697.71× fewer) 🟢 | intern -100.0% |
Time-only movers (cost flat — scheduling/locality noise)
| constant | main | PR | Δtime | Δcost (Zisk) | driver |
|---|---|---|---|---|---|
Std.DTreeMap.Internal.Zipper.ctorElim |
2.3ms | 53ms | +2220.7% (23.21× slower) |
-7.4% (1.08× fewer) 🟢 | intern -13.8% |
Int.add_one_le_of_lt |
5.1ms | 60ms | +1072.6% (11.73× slower) |
-1.1% | — |
Int.le.dest |
30ms | 60ms | +98.1% (1.98× slower) |
-11.6% (1.13× fewer) 🟢 | intern -33.6% |
Std.DHashMap.recOn |
18ms | 0.6ms | -96.7% (30.04× faster) 🟢 | +0.0% | — |
_private.Init.Data.List.Basic.0.List.range'_eq_range'TR.go._f |
21ms | 2.2ms | -89.7% (9.75× faster) 🟢 | -3.8% 🟢 | intern -10.8% |
The Ixon v3 changes in #636 added repeated declaration preparation and decoding to compilation. The definition-dependency guard in #637 also made anonymous kernel checking traverse each safe definition's complete dependency closure. Whole-environment checks consequently materialized and scanned the same external declarations many times, even when those declarations were unnecessary for checking the current item.
This PR shares compiler preparation work and establishes an explicit checking boundary around decoded Ixon environments. Local definition cycles are rejected during kernel ingress, allowing anonymous checking to preserve lazy external dependencies. In local runs with the default memory admission policy, Mathlib compilation falls from 289.171 seconds to 65.323 seconds, and Init + Std checking falls from 836.832 seconds to 8.459 seconds. A separate pre-v3 comparison puts Mathlib back near its earlier compilation time.
Compiler changes
Reuse the parallel setup decode for semantic validation
Previously,
compile_env_with_profiledecoded every declaration in a serial semantic-contract validation pass. The existing parallel setup scan then decoded every declaration again to build the reference graph, determine immediate groundedness, and collect inductive groups.Semantic-contract validation now runs inside that setup scan, using the declaration already decoded for the other setup work. The scan returns both the semantic declaration set and any validation error. Invalid semantic contracts still stop compilation before scheduling begins; removing the separate pass does not bypass validation.
Avoid contract resolution and decoration for ordinary declarations
The Lean frontend now checks both reserved metadata namespaces in one shared-expression traversal. It also checks selected source-contract registrations and measure hints. When none are present, preparation returns the original declaration list directly.
Large inputs are scanned in batches of 1,024 declarations on Lean's worker pool. Each batch only reads immutable declarations and returns a presence flag. Small inputs run directly. This avoids a serial scan of every expression before the parallel Rust compiler starts; complete source-contract preparation now takes about 1.3–1.4 seconds for Mathlib. Verbose compilation reports that phase separately.
The fast path retains declaration-name and uniqueness checks and examines declaration types, bodies, and recursor-rule bodies. A registration or reserved metadata marker selects the full resolution, validation, and decoration path, including malformed-marker rejection.
Kernel changes
Make decoded Ixon ingress the checking boundary
IxonCheckeraccepts an already decodedixon::Envand owns a private anonymousKEnv. The data path is:Callers cannot insert arbitrary kernel declarations into this worker. Anonymous FFI checking, profiling, resource validation, and the Zisk and SP1 guest callers now use this interface. Fuel accounting, profiling, diagnostics, and the existing cache-clearing policies remain available through the wrapper.
Validate local recursion before admitting a block
Ixon represents external dependencies with content addresses and local recursion with
Recslots. Ingress now collectsRecedges while converting definition types and values. Before publishing a standalone definition or any member of a mutual block, it rejects local cycles reachable from safe definitions.This includes references encountered through shared expressions. Acyclic forward references remain valid, and the existing treatment of unsafe and partial definitions is preserved. A rejected block publishes no declarations or block entries.
LazyConstant::get_atexplicitly verifies the binding between a constant's bytes and its environment map key. Anonymous ingress applies it to standalone constants, mutual blocks, and every projection admitted with a block. This also covers environments assembled in memory and prevents an address-verification result from being reused for a different key.With those bindings established, a cycle between distinct serialized blocks would require solving a cryptographic hash preimage problem. The remaining representable back edges are the local
Recedges checked during ingress.IxonCheckercan therefore skip the repeated traversal of external definition closures.The general
TypeCheckerAPI still performs the defensive dependency traversal for raw, mutableKEnvcallers. Checking an individual Ixon item also retains the existing claim semantics: referenced declarations are assumptions until their own work items are checked. Certifying a complete environment still requires checking every work item.Performance
These are local measurements on the same Ryzen 9 7950X3D machine, using release builds, Lean 4.33.1, cached imports, and 32 workers. The following table uses the default adaptive memory admission policy. The baseline is
bcc69954b9b177752e70611d895b81046aa49db1, which already includes both regressions. Compile times cover declaration preparation, Rust compilation, and file writing; initial import loading is outside the CLI's compile timer.Init + Std checking peak RSS falls from 6.355 GB to 1.794 GB.
Compiled outputs are byte-for-byte identical to the baseline: 342,786,227 bytes for Init + Std and 3,343,274,312 bytes for Mathlib. All 672,981 Mathlib kernel constants also pass checking.
A separate comparison against the pre-v3 revision,
cf77c957e50d64a5ed42330d3ae8c176296e7d1d, checks how much of the original performance is recovered:IX_COMPILE_ADAPTIVE=0)The fixed-worker range contains two runs. These are individual local measurements, not a statistical benchmark campaign. Fixed admission was used to isolate compiler work from scheduler pauses; the PR retains the default admission policy. The optimized v3 outputs match the v3 baseline byte for byte, while the pre-v3 output remains its original v2 encoding.
A separate Mathlib kernel comparison used clean release binaries, each version's matching
.ixe, and 32 workers, with no concurrent builds or benchmarks:All 672,981 constants passed in every run. Normal checks were run in reverse order relative to the profiled pair. The profiles contain 663,254 work items each; aggregate heartbeats, substitution nodes, reduction calls, equality calls, arithmetic work, and intern visits differ by less than 0.001%. These measurements do not reproduce the historical large Mathlib checking slowdown, though the small timing differences are insufficient to establish or exclude a minor regression.
Validation
parallel,net, andtest-ffienabled. Formatting and whitespace checks passed.To reproduce the primary measurements in each checkout, prepare the cached import artifacts and retain separate output files:
Compare each pair of compiled environments with
cmpto verify byte equality.