Skip to content

just for bench - #14976

Closed
TwoFX wants to merge 3 commits into
leanprover:masterfrom
TwoFX:julia/mimalloc-no-changes
Closed

just for bench#14976
TwoFX wants to merge 3 commits into
leanprover:masterfrom
TwoFX:julia/mimalloc-no-changes

Conversation

@TwoFX

@TwoFX TwoFX commented Aug 31, 2026

Copy link
Copy Markdown
Member

No description provided.

@TwoFX

TwoFX commented Aug 31, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Aug 31, 2026

Copy link
Copy Markdown

Benchmark results for a604c7d against fe1939c are in. There are significant results. @TwoFX

  • build//instructions: -132.0G (-1.15%)

Large changes (19✅, 4🟥)

  • compiled/binarytrees.st//instructions: -2.5G (-4.47%)
  • compiled/binarytrees//instructions: -2.5G (-4.48%)
  • compiled/deriv//instructions: -77.8M (-1.18%)
  • compiled/hashmap//instructions: -59.5M (-1.85%)
  • compiled/ilean_roundtrip//instructions: -185.8M (-0.84%)
  • 🟥 compiled/io_compute//instructions: +1.4G (+13.06%)
  • 🟥 compiled/io_compute//task-clock: +277ms (+13.06%)
  • 🟥 compiled/io_compute//wall-clock: +277ms (+13.07%)
  • compiled/liasolver//instructions: -31.4M (-0.94%)
  • compiled/nat_repr//instructions: -216.7M (-0.64%)
  • compiled/phashmap//instructions: -81.0M (-0.92%)
  • compiled/qsort//instructions: -59.9M (-0.40%)
  • compiled/rbmap//instructions: -195.9M (-2.44%)
  • compiled/rbmap_checkpoint2//instructions: -180.9M (-2.11%)
  • 🟥 compiled/rbmap_fbip//instructions: +66.8M (+0.97%)
  • compiled/rbmap_library//instructions: -976.4M (-10.43%)
  • compiled/select//instructions: -112.7M (-4.09%)
  • compiled/sigmaIterator//instructions: -60.0M (-2.24%)
  • compiled/treemap//instructions: -486.3M (-2.82%)
  • compiled/unionfind//instructions: -628.0M (-2.90%)
  • and 3 more

Medium changes (13✅)

  • build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.5G (-1.02%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -1.4G (-0.92%)
  • build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.0G (-0.91%)
  • compiled/parser//instructions: -314.3M (-0.88%)
  • compiled/workspaceSymbolsNewRanges//instructions: -10.5M (-1.57%)
  • elab/cbv_arm_ldst//instructions: -548.3M (-1.01%)
  • elab/grind_bitvec2//instructions: -1.5G (-0.90%)
  • elab/grind_list2//instructions: -392.0M (-1.00%)
  • elab/iterators//instructions: -37.4M (-1.53%)
  • elab/whnfMatcherImplicitTransparencyCaching//instructions: -139.5M (-0.57%)
  • interpreted/identifier_completion//instructions: -937.7M (-1.40%)
  • misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.5G (-1.15%)
  • size/install//bytes: -13MiB (-0.42%)

Small changes (1399✅, 1🟥)

  • build//task-clock: -38s (-1.89%)
  • build//wall-clock: -3s (-2.40%)
  • build/lakeprof/longest rebuild path//instructions: -8.0G (-1.32%)
  • build/module/Init.BinderPredicates//instructions: -29.6M (-1.40%)
  • build/module/Init.CbvSimproc//instructions: -27.0M (-1.28%)
  • build/module/Init.Control.Basic//instructions: -31.0M (-1.43%)
  • build/module/Init.Control.Except//instructions: -17.3M (-1.21%)
  • build/module/Init.Control.ExceptCps//instructions: -13.0M (-1.17%)
  • build/module/Init.Control.Lawful.Basic//instructions: -22.1M (-1.03%)
  • build/module/Init.Control.Lawful.Instances//instructions: -63.9M (-0.95%)
  • build/module/Init.Control.Lawful.MonadAttach.Instances//instructions: -14.7M (-0.89%)
  • build/module/Init.Control.Lawful.MonadAttach//instructions: -5.0M (-0.98%)
  • build/module/Init.Control.Lawful.MonadLift.Instances//instructions: -12.4M (-1.06%)
  • build/module/Init.Control.Lawful.MonadLift//instructions: -5.1M (-1.01%)
  • build/module/Init.Control.Option//instructions: -10.0M (-1.14%)
  • build/module/Init.Control.State//instructions: -13.4M (-1.22%)
  • build/module/Init.Control.StateCps//instructions: -12.8M (-1.25%)
  • build/module/Init.Control.StateRef//instructions: -9.6M (-1.05%)
  • build/module/Init.Conv//instructions: -54.3M (-1.45%)
  • build/module/Init.Core//instructions: -123.4M (-1.24%) (reduced significance based on absolute threshold)
  • and 1379 more
  • and 1 hidden

@TwoFX TwoFX closed this Aug 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants