chore: Update Lean to v4.33.0 - #554
Closed
argument-ci-bot[bot] wants to merge 20 commits into
Closed
Conversation
samuelburnham
force-pushed
the
update/lean-v4.33.0
branch
2 times, most recently
from
August 18, 2026 19:03
11f59a6 to
e4f88a1
Compare
Toolchain and dependencies bumped by lean-update.
`pr: true` opens the update PR on any outcome and skips the updater's validation build by default; the PR's own CI is the authority on whether the update builds.
Carries the v4.31 adaptation work forward: Std.HashMap `find?` renames to `get?` (including call sites added on main since), the ByteArray FFI helpers removed on the Lean and Rust sides, and assorted API fixes. Dependency pins move to v4.33.0: Cli and batteries by tag, LSpec to the merge commit of its v4.33.0 bump, and Blake3 to its v4.33.0 bump commit — the manifest entry for Blake3 still needs `lake update Blake3` once that commit is reachable on the remote. Benchmarks/Compile moves to the v4.33.0 toolchain with mathlib and FLT at their v4.33.0 tags.
Upstream lean4-nix stops at Lean v4.32.0 and builds toolchains from source
behind an overlay; the fork provides released toolchains as plain
derivations and removed the overlay API. The overlay block is replaced by
`lib.${system}.fromToolchainFile`, and the Lean sysroot for bindgen, the
Lake build inputs, the binary wrappers, and the dev shell take the
toolchain derivation directly.
The dev shell and the crane-side derivations evaluate now. The Lake
packages remain blocked on the `blake3-lean` input: it follows this flake's
lean4-nix, so Blake3.lean's own fork migration must be pushed and merged,
after which `nix flake update blake3-lean` and `lake update Blake3`
complete the move.
Formatting-only, plus the formatter declaration itself; nixfmt-tree wraps nixfmt so `nix fmt .` can still take a directory.
Lean v4.33.0 fixed two kernel soundness bugs (leanprover/lean4#14613, leanprover/lean4#14615) where a sort spelled e.g. `Sort (imax 1 0)` was not recognized as `Prop` because the zero test was syntactic; a non-proof field could then be projected out of a proof, and the inductive checker could misclassify Prop-only elimination and K-like reduction. Both ix kernels had the same syntactic test. `KUniv.isSemanticZero` / `KUniv::is_semantic_zero` decide `u ≡ 0` through the existing Géran normal form (zero normalizes to empty entries only, and norm-level equality already ignores empty entries), and replace the syntactic test at the four affected sites, in lockstep across both kernels: - proof-irrelevance Prop classification (Tc/DefEq, kernel/def_eq) - the struct-eta H3 Prop-major guard (Tc/Whnf, kernel/whnf) - the A4 field-universe Prop exemption (Tc/Inductive, kernel/inductive) - recursor-generation isProp/isLarge (AuxGen/Recursor; compile-side, Lean only) The IxVM kernel model retains the syntactic test and needs the same treatment separately.
Fallout of the v4.29 -> v4.33 bump that the skipped updater validation never surfaced: - batteries retired the `Batteries.Data.RBMap` umbrella module and moved the type to `RBTree.RBMap` in `Batteries.Recycling.RBTree`; ix keeps the recycled structure (the Verify layer proves theorems about it) rather than migrating `NormLevel`/`CNorm` to `Std.TreeMap`. - Two `groups`/`atoms` lookups in IxonUniv were RBMap sites caught in the earlier `Std.HashMap` `find?` -> `get?` rename; RBMap kept `find?`. - `do match` arms are non-dependent since v4.32 (leanprover/lean4#13305); the ShardMap size-invariant proofs need `match (dependent := true)`. - `Environment.addDeclCore` gained a `maxRecDepth` parameter (leanprover/lean4#13956); pass Lean's default. - The Canonicity alias fixtures need `@[expose]` under the module system's cross-module compilation-type check.
`Lean.Int` is in the compiler's `builtinRuntimeTypes`, so at runtime it shares `Nat`'s representation — a tagged scalar or a GMP mpz object; `Int.ofNat` compiles to the identity `lean_nat_to_int` and no ctor cell ever exists. The mdata `DataValue.ofInt` decode path nevertheless read it through the `LeanIxInt` ctor layout, dereferencing a tagged scalar (or reading mpz limbs as ctor fields) whenever an `Expr.mdata` KVMap carried an integer. Decode by value instead: arithmetic-shift the tagged scalar to recover the signed payload, and for mpz objects take the sign from `lean_int_dec_lt` and the magnitude from `lean_nat_abs`. `LeanIxInt` remains in use for `Ix.Int`, a genuine two-ctor inductive. Pre-existing bug surfaced by the v4.33 FFI layout audit, which found no other divergence between the hardcoded layouts and Lean v4.33.0.
Records the lean4lean integration steps and their verification queue, the open kernel-semantics divergences from upstream (theorem opacity, the IxVM syntactic zero test, the deliberately-unenforced mutual universe uniformity, missing regression fixtures), the divergences considered and cleared during the audit, and the non-blocking follow-ups (FFI pointer liveness, benchmark re-baselining, thread-pool stack ordering, OpenSSL link watch, setup-file JSON parsing).
lean4lean 5e5bb767 -> 4844eda4. The old pin predated the v4.32.1 kernel soundness fix (leanprover/lean4#14498): its `addOpaque` never called `checkNoMVarNoFVar` on the opaque's value, so it accepted the axiom-free `False` construction from #14484 -- reachable from ix via `Benchmarks/Lean4Lean.lean:209`. The new pin also builds `--wfail` clean, which the ix lint gate needs, since 785 linter warnings and the 16 frontier sorries were cleared upstream in PR #5. Blake3 is pinned to the unmerged `native-decide-dynlib` branch: it builds `blake3-rs` as a cdylib and exposes `blake3_rs_shared`, which `ix_native_decide_dynlib` needs to supply the BLAKE3 backend to Lean's native evaluator, and that dynlib gates every `IxTcVerify` module. Move to Blake3 main once that branch merges.
v4.33 routes a `return` inside a `try` block through the early-return transformer, which buries the plain `EStateM.tryCatch` this reduces to and that `Ix/Tc/Verify/Whnf/Iota/ConstructorSynthesis.lean` reasons about. Spelled with `tryCatch`/`pure` instead. Both spellings denote the same function; `lake build Ix` confirms nothing downstream depended on the old elaboration.
v4.33 deprecates `Lean.RBTree` in favour of `Std.TreeSet`, which fails the `--wfail` lint gate. `Bytecode.MemSizes` was the only Lean-side use; the API is identical except `fold` -> `foldl`. The `Batteries.Recycling.RBTree` uses in `Ix/Tc/Level.lean` and `Ix/IxonUniv.lean` are a different, non-deprecated type and are untouched.
`BRecOn`'s `rtc` rebind after `popLocals` is dead -- nothing reads it past that point -- but the call must still run to balance the TC-side local context, so the value is discarded rather than the call removed. `wfTwoEqDef` stays a `def`: the fixture exists to pin the prop-valued-`def` constant class metaprograms emit, so `linter.defProp` is silenced at that declaration rather than obeyed.
v4.33 removed `String.Slice.Pattern.Model.NoPrefixForwardPatternModel`. `NoPrefixPatternModel` is the surviving class of the same shape -- a `Prop` class over a single forall-typed field -- which is what the entry exists to drive: it is the regression driver for `is_rec_field`'s per-peel whnf (#510). The FFT cost is still the removed constant's measurement and needs a re-baseline.
The manifests are exact-match, so a *shrinking* trust boundary fails them too. Three movements at the new pin: `Lean4Lean.TrProj` no longer uses `sorryAx`, dropping it from 15 roots' `sorryOrigins`; ~56 roots no longer reach the `ctxAddrForLbrUncached` native axiom; and `canonicalAuxOrder`'s native axiom is `ax_9` rather than `ax_15`, that index being a count of `native_decide` sites in `Ix/Tc/Inductive.lean`. Both audits pass: 1796 roots in `Completed`, 7 in `Statements`.
Nothing downstream of lean4lean compiled under the old pin, so all of this only surfaced once the dependency built. All 438 modules build, sorry-free. Recurring causes: v4.33 elaborator. A pure `let` in `do` is a term-level `have`, not `pure _ >>= _`, so `run_pure_bind`/`ReaderT.run_pure`/`pure_bind` steps and the matching `WF.bind (WF.pure ..)` proof layers became no-ops. `do` loops carry state as a `Prod`, not an `MProd`. Guard `if`s survive as `if false = true then ..`. v4.33 simp. `simpa [f] using h` closes with reducible transparency, so it now fails where the goal and `h` differ only by delta/iota on a plain `def` (`TcM.runRec`, `StepWFAtOn`, `BlockCatalog.Contains`, `KExpr.addr` on a literal); `exact` unfolds at default transparency and succeeds. Relatedly, `runRec`'s equation lemma is eta-expanded, so naming it in a simp set does nothing against an unapplied `runRec y`. simp also stopped unfolding semireducible definitions while matching, hence `KVLCtx` is now an `abbrev`. Core/batteries. `Nat.imax` moved into the `Lean` namespace; `Batteries.RBNode.cmpLT_iff` became `RBTree.RBNode.cmpLT_iff`; `Except` has no `DecidableEq`, so `Driver/Enumeration.lean` defines one for the `native_decide` fixtures. lean4lean API. `VEnv` gained `structEtas`; `VDecl.block` became `mutualDef`; `Checked` gained `kTarget`/`kTarget_eq`; `fieldsR`/`recArgsR`/ `resultIndicesR` gained an `ElimMode` argument; `instL_lamN`/`instN_lamN` are now upstream and the local copies are deleted. Two spec decisions where the new lean4lean models both elimination modes: `SingletonRecursor` is generalized to `generation.recUvars`, while `SingletonEnumeration` gains an explicit `largeElimination` field, since its proofs are built around the fresh motive universe. `PropositionClassifierContext` gains a `universes` field bounding the size of universes the run support covers. This is needed because the classifier now splits on `u.isSemanticZero` to match production, whose positive branch routes through `Level.normalizeLevel_eval` and its `size < UInt64.size` side condition. The structure is only ever a hypothesis, so this ADDS an assumption the eventual instantiation must discharge; it mirrors the convention in `DefEq/StructuralCongruence.lean` and `DefEq/SameHeadSpine.lean`.
samuelburnham
force-pushed
the
update/lean-v4.33.0
branch
from
August 18, 2026 20:20
e4f88a1 to
c377597
Compare
Member
|
!benchmark compile decompile |
Member
|
!benchmark ooc |
Member
|
!benchmark aiur |
Author
|
| 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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT |
36.262 s | 51.161 s | +41.1% (1.41× slower) |
14.08K | 15.26K | +8.4% (1.08× faster) 🟢 | 12.39 GiB | 19.89 GiB | +60.6% (1.61× larger) |
1.68 GiB | 3.20 GiB | +90.5% (1.90× larger) |
510,687 | 780,906 | +52.9% (1.53× more) |
compile · InitStd — main from: base run @ e45ff02 (not on bencher)
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 |
4.032 s | 4.111 s | +2.0% | 26.16K | 28.48K | +8.9% (1.09× faster) 🟢 | 3.58 GiB | 3.92 GiB | +9.6% (1.10× larger) |
301.20 MiB | 324.60 MiB | +7.8% (1.08× larger) |
105,492 | 117,084 | +11.0% (1.11× more) |
compile · Lean — main from: base run @ e45ff02 (not on bencher)
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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Lean |
7.229 s | 7.557 s | +4.5% |
26.14K | 27.35K | +4.6% 🟢 | 5.02 GiB | 5.33 GiB | +6.1% (1.06× larger) |
448.62 MiB | 481.12 MiB | +7.2% (1.07× larger) |
188,999 | 206,647 | +9.3% (1.09× more) |
compile · Mathlib — main from: base run @ e45ff02 (not on bencher)
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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Mathlib |
54.425 s | 50.569 s | -7.1% (1.08× faster) 🟢 | 13.53K | 15.25K | +12.7% (1.13× faster) 🟢 | 18.82 GiB | 19.00 GiB | +0.9% | 2.94 GiB | 3.10 GiB | +5.4% (1.05× larger) |
736,618 | 771,129 | +4.7% |
decompile · FLT — main from: base run @ e45ff02 (not on bencher)
1 constant · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-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) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
FLT |
1m 10.9s | 4m 37.3s | +291.2% (3.91× slower) |
7.20K | 2.82K | -60.9% (2.56× slower) |
18.87 GiB | 33.70 GiB | +78.5% (1.79× larger) |
1.68 GiB | 3.20 GiB | +90.5% (1.90× larger) |
510,687 | 780,906 | +52.9% (1.53× more) |
decompile · InitStd — main from: base run @ e45ff02 (not on bencher)
1 constant · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-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 |
5.694 s | 6.301 s | +10.7% (1.11× slower) |
18.53K | 18.58K | +0.3% | 3.63 GiB | 4.22 GiB | +16.3% (1.16× larger) |
301.20 MiB | 324.60 MiB | +7.8% (1.08× larger) |
105,492 | 117,084 | +11.0% (1.11× more) |
decompile · Lean — main from: base run @ e45ff02 (not on bencher)
1 constant · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-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 |
12.089 s | 13.017 s | +7.7% (1.08× slower) |
15.63K | 15.88K | +1.5% | 5.00 GiB | 5.43 GiB | +8.6% (1.09× larger) |
448.62 MiB | 481.12 MiB | +7.2% (1.07× larger) |
188,999 | 206,647 | +9.3% (1.09× more) |
decompile · Mathlib — main from: base run @ e45ff02 (not on bencher)
1 constant · 1 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).
| constant | decompile-time (main) | decompile-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 27.4s | 4m 3.9s | +17.6% (1.18× slower) |
3.55K | 3.16K | -11.0% (1.12× slower) |
31.75 GiB | 32.80 GiB | +3.3% |
2.94 GiB | 3.10 GiB | +5.4% (1.05× larger) |
736,618 | 771,129 | +4.7% |
Author
|
| env/constant | check-time (main) | check-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|
InitStd |
9.231 s | 7.750 s | -16.0% (1.19× faster) 🟢 | 9.64K | 12.75K | +32.2% (1.32× faster) 🟢 | 1.85 GiB | 2.33 GiB | +26.3% (1.26× larger) |
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual |
3.382 s | 3.408 s | +0.8% | 1.68K | 1.81K | +8.3% (1.08× faster) 🟢 | 2.19 GiB | 2.32 GiB | +5.7% (1.06× larger) |
Array.extract_append |
516.2 ms | 517.5 ms | +0.2% | 3.00K | 3.12K | +3.9% 🟢 | 1.76 GiB | 1.19 GiB | -32.5% (1.48× smaller) 🟢 |
Vector.extract_append._proof_2 |
511.7 ms | 512.4 ms | +0.1% | 2.56K | 2.66K | +4.0% 🟢 | 1.66 GiB | 1.72 GiB | +3.5% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
278.1 ms | 279.6 ms | +0.5% | 9.70K | 9.95K | +2.6% | 1.28 GiB | 1.21 GiB | -5.4% (1.06× smaller) 🟢 |
Char.ofOrdinal_le_of_le |
273.0 ms | 274.1 ms | +0.4% | 9.74K | 10.13K | +4.0% 🟢 | 1.76 GiB | 1.62 GiB | -8.0% (1.09× smaller) 🟢 |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
264.2 ms | 264.9 ms | +0.3% | 6.88K | 7.07K | +2.8% | 1.51 GiB | 1.68 GiB | +11.0% (1.11× larger) |
String.split |
263.6 ms | 264.1 ms | +0.2% | 6.72K | 6.94K | +3.3% 🟢 | 1.40 GiB | 1.45 GiB | +4.0% |
List.mergeSort |
261.1 ms | 261.7 ms | +0.2% | 5.57K | 5.79K | +3.9% 🟢 | 1.13 GiB | 1.04 GiB | -7.4% (1.08× smaller) 🟢 |
Vector.append |
254.4 ms | 255.0 ms | +0.2% | 1.96K | 2.10K | +7.2% (1.07× faster) 🟢 | 983.48 MiB | 772.68 MiB | -21.4% (1.27× smaller) 🟢 |
Nat.gcd_comm |
254.2 ms | 254.5 ms | +0.1% | 1.53K | 1.65K | +7.3% (1.07× faster) 🟢 | 983.48 MiB | 1005.77 MiB | +2.3% |
String.append |
252.9 ms | 253.3 ms | +0.2% | 1.21K | 1.30K | +7.3% (1.07× faster) 🟢 | 1.08 GiB | 1.30 GiB | +19.8% (1.20× larger) |
Nat.sub_le_of_le_add |
252.5 ms | 252.9 ms | +0.1% | 673.180 | 727.620 | +8.1% (1.08× faster) 🟢 | 658.93 MiB | 679.77 MiB | +3.2% |
Int.gcd |
252.5 ms | 252.7 ms | +0.1% | 823.750 | 882.560 | +7.1% (1.07× faster) 🟢 | 778.80 MiB | 827.77 MiB | +6.3% (1.06× larger) |
Nat.add_comm |
252.2 ms | 252.2 ms | +0.0% | 166.560 | 182.360 | +9.5% (1.09× faster) 🟢 | 499.68 MiB | 524.97 MiB | +5.1% (1.05× larger) |
per-constant drill-down — Σ check 198.51s → 214.13s (+7.9%), Σ cost +7.8%; 1958 cost mover(s), 33 time-only mover(s); 12392 added (19.34s), 2933 removed (3.46s)
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 regressions (counter-backed)
| constant | main | PR | Δtime | Δcost (Zisk) | driver |
|---|---|---|---|---|---|
Vector.range_eq_range' |
0.5ms | 208ms | +42052.3% (421.52× slower) |
+84243.5% (843.44× more) |
whnf +1026160.0% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant._proof_1_25 |
0.1ms | 14ms | +9745.3% (98.45× slower) |
+8466.9% (85.67× more) |
subst +11585.2% |
Std.Time.FormatConfig.mk.sizeOf_spec |
0.4ms | 7.8ms | +1934.1% (20.34× slower) |
+6693.5% (67.94× more) |
whnf +18226.7% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_motive._proof_1_9 |
0.3ms | 19ms | +7073.9% (71.74× slower) |
+6077.9% (61.78× more) |
whnf +62800.0% |
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go._unary._proof_6 |
0.4ms | 20ms | +4954.4% (50.54× slower) |
+6021.9% (61.22× more) |
whnf +83800.0% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_derivedLits._proof_1_21 |
0.4ms | 26ms | +7032.0% (71.32× slower) |
+6007.7% (61.08× more) |
whnf +31066.7% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive._proof_1_28 |
0.3ms | 12ms | +3551.7% (36.52× slower) |
+4511.0% (46.11× more) |
whnf +40400.0% |
_private.Init.Data.Array.Lex.Basic.0.Array.lex._proof_1 |
0.4ms | 18ms | +4305.8% (44.06× slower) |
+3969.9% (40.70× more) |
whnf +17125.0% |
Std.Time.DateTime.toLeanDateTimeWithZoneString |
0.1ms | 3.9ms | +2564.8% (26.65× slower) |
+3947.5% (40.48× more) |
whnf +7500.0% |
_private.Init.Data.Array.Lex.Basic.0.Array.lex._proof_2 |
0.4ms | 17ms | +3623.2% (37.23× slower) |
+3727.7% (38.28× more) |
whnf +65800.0% |
Cost improvements (counter-backed)
| constant | main | PR | Δtime | Δcost (Zisk) | driver |
|---|---|---|---|---|---|
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant._proof_1_35 |
18ms | 0.1ms | -99.2% (125.96× faster) 🟢 | -99.4% (165.42× fewer) 🟢 | whnf -99.8% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant._proof_1_33 |
9.5ms | 0.2ms | -98.3% (59.19× faster) 🟢 | -99.0% (97.37× fewer) 🟢 | subst -99.3% |
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go |
17ms | 0.5ms | -97.1% (34.39× faster) 🟢 | -98.6% (70.93× fewer) 🟢 | whnf -99.8% |
Std.Tactic.BVDecide.BVExpr.decEq |
40ms | 2.3ms | -94.1% (16.98× faster) 🟢 | -98.2% (55.38× fewer) 🟢 | subst -99.7% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_invariant_helper._proof_1_12 |
21ms | 0.3ms | -98.4% (62.12× faster) 🟢 | -97.8% (46.40× fewer) 🟢 | whnf -99.2% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive._proof_1_16 |
16ms | 0.2ms | -98.7% (74.69× faster) 🟢 | -97.5% (40.41× fewer) 🟢 | whnf -100.0% |
_private.Init.Data.Array.Lex.Basic.0.Array.lex._proof_3 |
18ms | 0.4ms | -97.8% (46.20× faster) 🟢 | -97.5% (40.16× fewer) 🟢 | nat_arith -100.0% |
_private.Init.Data.Array.Lex.Basic.0.Array.lex._proof_4 |
16ms | 0.4ms | -97.3% (36.64× faster) 🟢 | -97.4% (37.77× fewer) 🟢 | whnf -100.0% |
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_confirmRupHint._proof_1_12 |
6.2ms | 0.2ms | -96.2% (26.66× faster) 🟢 | -97.1% (34.71× fewer) 🟢 | whnf -99.3% |
Std.Do.ExceptConds.false_and |
2.9ms | 0.2ms | -94.5% (18.25× faster) 🟢 | -97.1% (34.70× fewer) 🟢 | whnf -100.0% |
Time-only movers (cost flat — scheduling/locality noise)
| constant | main | PR | Δtime | Δcost (Zisk) | driver |
|---|---|---|---|---|---|
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.encode |
0.4ms | 22ms | +5724.0% (58.24× slower) |
+0.0% | — |
Std.TreeSet.Raw.get!_congr |
0.4ms | 19ms | +4461.6% (45.62× slower) |
+0.0% | — |
BitVec.iunfoldr_replace |
1.3ms | 17ms | +1143.7% (12.44× slower) |
+0.8% | — |
Std.DHashMap.Raw.get!_eq_getD_default |
1.9ms | 22ms | +1086.7% (11.87× slower) |
+0.0% | — |
List.zipIdxLE_total |
2.2ms | 16ms | +598.1% (6.98× slower) |
+0.0% | — |
Author
|
| constant | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | execute-time (main) | execute-time (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Array.extract_append |
34.319 s | 40.817 s | +18.9% (1.19× slower) |
44.930 | 39.350 | -12.4% (1.14× slower) |
77.55 GiB | 77.74 GiB | +0.3% | 9.873 s | 11.025 s | +11.7% (1.12× slower) |
126.4 ms | 139.4 ms | +10.3% (1.10× slower) |
21.15 MiB | 21.15 MiB | +0.0% | 147.17B | 156.30B | +6.2% (1.06× more) |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
33.270 s | 38.127 s | +14.6% (1.15× slower) |
80.880 | 72.780 | -10.0% (1.11× slower) |
76.74 GiB | 76.41 GiB | -0.4% | 9.915 s | 9.975 s | +0.6% | 127.6 ms | 141.0 ms | +10.5% (1.11× slower) |
21.25 MiB | 21.25 MiB | +0.0% | 152.43B | 153.04B | +0.4% |
Char.ofOrdinal_le_of_le |
25.578 s | 30.352 s | +18.7% (1.19× slower) |
103.450 | 91.030 | -12.0% (1.14× slower) |
63.33 GiB | 64.33 GiB | +1.6% | 6.557 s | 6.901 s | +5.2% (1.05× slower) |
149.5 ms | 133.3 ms | -10.8% (1.12× faster) 🟢 | 21.26 MiB | 21.26 MiB | +0.0% | 103.35B | 107.22B | +3.7% |
Vector.extract_append._proof_2 |
19.604 s | 25.733 s | +31.3% (1.31× slower) |
66.410 | 52.700 | -20.6% (1.26× slower) |
42.30 GiB | 51.79 GiB | +22.4% (1.22× larger) |
5.675 s | 5.949 s | +4.8% |
127.5 ms | 130.6 ms | +2.5% | 20.90 MiB | 20.99 MiB | +0.4% | 84.13B | 88.64B | +5.4% (1.05× more) |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
15.380 s | 17.885 s | +16.3% (1.16× slower) |
117.820 | 104.390 | -11.4% (1.13× slower) |
36.15 GiB | 36.65 GiB | +1.4% | 3.810 s | 3.668 s | -3.7% 🟢 | 126.9 ms | 140.1 ms | +10.4% (1.10× slower) |
21.10 MiB | 21.10 MiB | +0.0% | 60.20B | 60.82B | +1.0% |
String.split |
14.442 s | 16.474 s | +14.1% (1.14× slower) |
122.210 | 110.900 | -9.3% (1.10× slower) |
34.14 GiB | 34.21 GiB | +0.2% | 3.489 s | 3.387 s | -2.9% | 134.0 ms | 137.1 ms | +2.4% | 21.24 MiB | 21.24 MiB | +0.0% | 55.11B | 55.33B | +0.4% |
List.mergeSort |
11.184 s | 12.491 s | +11.7% (1.12× slower) |
129.470 | 120.800 | -6.7% (1.07× slower) |
25.64 GiB | 25.17 GiB | -1.8% | 2.506 s | 2.543 s | +1.5% | 131.0 ms | 129.9 ms | -0.8% | 21.15 MiB | 21.15 MiB | +0.0% | 39.90B | 40.17B | +0.7% |
Vector.append |
3.667 s | 4.080 s | +11.2% (1.11× slower) |
132.250 | 127.950 | -3.3% |
6.72 GiB | 6.75 GiB | +0.5% | 710.1 ms | 700.8 ms | -1.3% | 126.5 ms | 125.1 ms | -1.1% | 19.73 MiB | 19.73 MiB | +0.0% | 9.14B | 9.15B | +0.1% |
Nat.gcd_comm |
2.880 s | 3.257 s | +13.1% (1.13× slower) |
135.430 | 128.660 | -5.0% (1.05× slower) |
5.04 GiB | 5.02 GiB | -0.2% | 531.3 ms | 529.4 ms | -0.4% | 125.3 ms | 119.5 ms | -4.6% 🟢 | 19.56 MiB | 19.56 MiB | +0.0% | 5.87B | 5.97B | +1.8% |
String.append |
2.148 s | 2.412 s | +12.3% (1.12× slower) |
141.510 | 135.570 | -4.2% |
4.70 GiB | 4.71 GiB | +0.2% | 409.5 ms | 398.5 ms | -2.7% | 113.9 ms | 115.4 ms | +1.3% | 18.81 MiB | 18.81 MiB | +0.0% | 3.23B | 3.28B | +1.7% |
Int.gcd |
1.884 s | 2.100 s | +11.5% (1.11× slower) |
110.380 | 106.180 | -3.8% |
4.64 GiB | 4.70 GiB | +1.3% | 347.9 ms | 355.7 ms | +2.3% | 121.4 ms | 113.1 ms | -6.9% (1.07× faster) 🟢 | 18.39 MiB | 18.39 MiB | +0.0% | 2.09B | 2.13B | +1.9% |
Nat.sub_le_of_le_add |
1.709 s | 1.957 s | +14.5% (1.14× slower) |
99.450 | 94.040 | -5.4% (1.06× slower) |
4.71 GiB | 4.78 GiB | +1.3% | 342.5 ms | 342.8 ms | +0.1% | 118.7 ms | 115.7 ms | -2.5% | 18.77 MiB | 18.84 MiB | +0.4% | 1.81B | 1.86B | +2.7% |
Nat.add_comm |
1.064 s | 1.092 s | +2.7% | 39.490 | 42.120 | +6.7% (1.07× faster) 🟢 | 3.70 GiB | 3.87 GiB | +4.6% |
251.8 ms | 252.2 ms | +0.2% | 100.9 ms | 111.1 ms | +10.1% (1.10× slower) |
17.20 MiB | 17.20 MiB | +0.0% | 287.58M | 303.19M | +5.4% (1.05× more) |
Member
|
!bencher-thresholds-reset all |
github-actions
Bot
added
the
bencher-thresholds-reset:all
|
♻️ Baseline reset queued for: all — will anchor to the merge commit when this PR merges. |
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 free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 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.
lean-toolchainand dependencies updated for Lean releasev4.33.0by lean-update.