Skip to content

perf: outline lean_dec_ref_cold deletion case #11829

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
Kha wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

perf: outline lean_dec_ref_cold deletion case #11829

Kha wants to merge 2 commits into from
+25 −24

Conversation

@Kha
Copy link
Member

@Kha Kha commented Dec 29, 2025

No description provided.

@Kha
Copy link
Member Author

Kha commented Dec 29, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Dec 29, 2025 •
edited
Loading

Benchmark results for 34e4c90 against 13c88f9 are in! @Kha

Large changes (11🟥)
  • 🟥 big_do//instructions: +134.2M (+0.4%)
  • 🟥 binarytrees.st//instructions: +616.9M (+0.9%)
  • 🟥 binarytrees//instructions: +615.8M (+0.9%)
  • 🟥 deriv//instructions: +83.6M (+1.1%)
  • 🟥 hashmap.lean//instructions: +69.3M (+1.8%)
  • 🟥 rbmap//instructions: +250.8M (+1.6%)
  • 🟥 rbmap_1//instructions: +137.3M (+0.9%)
  • 🟥 rbmap_10//instructions: +235.5M (+1.5%)
  • 🟥 rbmap_library//instructions: +162.7M (+1.2%)
  • 🟥 treemap.lean//instructions: +95.2M (+0.4%)
  • 🟥 unionfind//instructions: +531.9M (+2.1%)
Medium changes (5✅, 6🟥)
  • ✅ Init.Prelude async//instructions: -86.2M (-0.6%)
  • ✅ big_beq_rec//instructions: -151.2M (-0.7%)
  • ✅ big_match_partial//instructions: -118.1M (-0.6%)
  • 🟥 big_omega.lean//instructions: +101.9M (+0.4%)
  • 🟥 bv_decide_mul//instructions: +285.4M (+0.6%)
  • 🟥 ilean roundtrip//instructions: +152.5M (+0.6%)
  • 🟥 liasolver//instructions: +24.2M (+0.6%)
  • ✅ mut_rec_wf//instructions: -191.0M (-0.6%)
  • 🟥 parser//instructions: +185.6M (+0.3%)
  • 🟥 rbmap_fbip//instructions: +8.1M (+0.1%)
  • ✅ simp_local//instructions: -699.6M (-1.2%)
Small changes (10✅, 189🟥)
  • 🟥 Init.Data.BitVec.Lemmas//instructions: +292.4M (+0.2%)
  • 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +761.3M (+0.3%)
  • ✅ big_beq//instructions: -46.8M (-0.4%)
  • 🟥 big_match_nat_split//instructions: +64.2M (+0.5%)
  • 🟥 big_omega.lean MT//instructions: +71.5M (+0.3%)
  • 🟥 build/module/Init.Data.Ord.SInt//instructions: +16.3M (+0.5%)
  • 🟥 build/module/Init.Data.Range.Polymorphic.IntLemmas//instructions: +45.2M (+0.1%)
  • 🟥 build/module/Init.Data.Vector.Perm//instructions: +39.2M (+0.6%)
  • 🟥 build/module/Init.Notation//instructions: +76.4M (+0.4%)
  • 🟥 build/module/Init.NotationExtra//instructions: +57.5M (+0.4%)
  • ✅ build/module/Init.Prelude//instructions: -110.9M (-0.7%)
  • 🟥 build/module/Lake.Build.Common//instructions: +96.1M (+0.3%)
  • 🟥 build/module/Lake.Build.Library//instructions: +38.0M (+0.5%)
  • 🟥 build/module/Lake.Build.Module//instructions: +229.5M (+0.4%)
  • 🟥 build/module/Lake.Build.Package//instructions: +44.3M (+0.5%)
  • 🟥 build/module/Lake.Build.Target.Fetch//instructions: +38.0M (+0.5%)
  • 🟥 build/module/Lake.CLI.Main//instructions: +130.6M (+0.4%)
  • 🟥 build/module/Lake.Config.Meta//instructions: +29.4M (+0.3%)
  • 🟥 build/module/Lake.Load.Resolve//instructions: +50.6M (+0.4%)
  • 🟥 build/module/Lake.Toml.Elab.Value//instructions: +20.2M (+0.4%)
  • 🟥 build/module/Lake.Toml.Grammar//instructions: +14.3M (+0.3%)
  • 🟥 build/module/Lean.AddDecl//instructions: +21.3M (+0.4%)
  • 🟥 build/module/Lean.Compiler.LCNF.Main//instructions: +23.2M (+0.4%)
  • 🟥 build/module/Lean.Compiler.LCNF.Simp.Main//instructions: +29.2M (+0.4%)
  • 🟥 build/module/Lean.Compiler.LCNF.Simp.SimpM//instructions: +16.4M (+0.4%)
  • 🟥 build/module/Lean.Compiler.LCNF.Specialize//instructions: +44.9M (+0.3%)
  • 🟥 build/module/Lean.Compiler.LCNF.ToDecl//instructions: +18.1M (+0.4%)
  • 🟥 build/module/Lean.Compiler.LCNF.Visibility//instructions: +24.4M (+0.4%)
  • 🟥 build/module/Lean.Data.Json.Elab//instructions: +15.2M (+0.4%)
  • 🟥 build/module/Lean.Data.Xml.Parser//instructions: +52.1M (+0.5%)
  • 🟥 build/module/Lean.DocString.Formatter//instructions: +28.8M (+0.4%)
  • ✅ build/module/Lean.DocString.Types//instructions: -72.3M (-0.8%)
  • 🟥 build/module/Lean.Elab.App//instructions: +138.6M (+0.3%)
  • 🟥 build/module/Lean.Elab.Binders//instructions: +79.9M (+0.4%)
  • 🟥 build/module/Lean.Elab.BuiltinCommand//instructions: +75.3M (+0.3%)
  • 🟥 build/module/Lean.Elab.BuiltinEvalCommand//instructions: +37.0M (+0.4%)
  • 🟥 build/module/Lean.Elab.BuiltinNotation//instructions: +79.8M (+0.4%)
  • 🟥 build/module/Lean.Elab.BuiltinTerm//instructions: +57.8M (+0.4%)
  • 🟥 build/module/Lean.Elab.Deriving.Basic//instructions: +43.1M (+0.4%)
  • 🟥 build/module/Lean.Elab.Deriving.Ord//instructions: +45.8M (+0.5%)
  • 🟥 build/module/Lean.Elab.Deriving.ToExpr//instructions: +43.0M (+0.4%)
  • 🟥 build/module/Lean.Elab.Deriving.Util//instructions: +34.1M (+0.5%)
  • 🟥 build/module/Lean.Elab.Do.Basic//instructions: +45.8M (+0.3%)
  • 🟥 build/module/Lean.Elab.Do.Legacy//instructions: +165.6M (+0.3%)
  • 🟥 build/module/Lean.Elab.DocString.Builtin.Keywords//instructions: +77.2M (+0.4%)
  • 🟥 build/module/Lean.Elab.DocString.Builtin//instructions: +217.1M (+0.4%)
  • 🟥 build/module/Lean.Elab.DocString//instructions: +147.9M (+0.3%)
  • 🟥 build/module/Lean.Elab.ErrorExplanation//instructions: +28.8M (+0.4%)
  • 🟥 build/module/Lean.Elab.Extra//instructions: +42.5M (+0.4%)
  • 🟥 build/module/Lean.Elab.Inductive//instructions: +52.4M (+0.4%)
  • 🟥 build/module/Lean.Elab.Match//instructions: +100.8M (+0.3%)
  • 🟥 build/module/Lean.Elab.MutualDef//instructions: +128.6M (+0.3%)
  • 🟥 build/module/Lean.Elab.MutualInductive//instructions: +160.1M (+0.3%)
  • 🟥 build/module/Lean.Elab.Parallel//instructions: +33.1M (+0.3%)
  • 🟥 build/module/Lean.Elab.PatternVar//instructions: +53.4M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Basic//instructions: +34.4M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Eqns//instructions: +40.1M (+0.4%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Main//instructions: +51.4M (+0.4%)
  • 🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Induction//instructions: +43.3M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Main//instructions: +26.6M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Structural.FindRecArg//instructions: +39.7M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Structural.Main//instructions: +32.3M (+0.5%)
  • 🟥 build/module/Lean.Elab.PreDefinition.WF.GuessLex//instructions: +57.5M (+0.3%)
  • 🟥 build/module/Lean.Elab.PreDefinition.WF.Main//instructions: +21.4M (+0.4%)
  • 🟥 build/module/Lean.Elab.Quotation.Precheck//instructions: +19.5M (+0.3%)
  • 🟥 build/module/Lean.Elab.StructInst//instructions: +127.2M (+0.3%)
  • 🟥 build/module/Lean.Elab.Structure//instructions: +170.2M (+0.3%)
  • 🟥 build/module/Lean.Elab.Syntax//instructions: +70.4M (+0.3%)
  • 🟥 build/module/Lean.Elab.SyntheticMVars//instructions: +58.9M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify//instructions: +23.5M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVDecide//instructions: +39.7M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVTrace//instructions: +13.8M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: +188.9M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.TypeAnalysis//instructions: +34.8M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize//instructions: +19.7M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Basic//instructions: +54.5M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.BuiltinTactic//instructions: +115.4M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Do.Spec//instructions: +44.0M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.Do.Syntax//instructions: +25.5M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.Do.VCGen//instructions: +113.5M (+0.2%)
  • 🟥 build/module/Lean.Elab.Tactic.ElabTerm//instructions: +48.8M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Ext//instructions: +41.6M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.Basic//instructions: +44.1M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.BuiltinTactic//instructions: +71.0M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.Config//instructions: +54.4M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.Main//instructions: +71.3M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.Param//instructions: +39.6M (+0.3%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.ShowState//instructions: +25.1M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Induction//instructions: +113.4M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Lets//instructions: +24.3M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.Omega.Frontend//instructions: +146.0M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Rewrite//instructions: +28.9M (+0.5%)
  • 🟥 build/module/Lean.Elab.Tactic.Simp//instructions: +74.3M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.SolveByElim//instructions: +24.2M (+0.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Try//instructions: +142.7M (+0.3%)
  • 🟥 build/module/Lean.Elab.Term.TermElabM//instructions: +73.7M (+0.2%)
  • 🟥 build/module/Lean.Linter.UnusedVariables//instructions: +37.2M (+0.3%)
  • 🟥 build/module/Lean.Meta.AppBuilder//instructions: +35.2M (+0.3%)
  • 🟥 build/module/Lean.Meta.Constructions.NoConfusion//instructions: +37.7M (+0.4%)
  • 🟥 build/module/Lean.Meta.ExprDefEq//instructions: +103.3M (+0.3%)
  • 🟥 build/module/Lean.Meta.Injective//instructions: +56.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.Match.Match//instructions: +72.5M (+0.3%)
  • 🟥 build/module/Lean.Meta.Match.MatcherApp.Transform//instructions: +26.2M (+0.3%)
  • 🟥 build/module/Lean.Meta.Match.Rewrite//instructions: +18.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Offset//instructions: +23.9M (+0.5%)
  • 🟥 build/module/Lean.Meta.SizeOf//instructions: +44.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.SplitSparseCasesOn//instructions: +14.0M (+0.4%)
  • 🟥 build/module/Lean.Meta.SynthInstance//instructions: +53.6M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Cases//instructions: +24.3M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Contradiction//instructions: +27.0M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +182.0M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.AC.Eq//instructions: +153.1M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.AC.Proof//instructions: +65.0M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr//instructions: +249.5M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize//instructions: +62.1M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Proof//instructions: +125.5M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Reify//instructions: +76.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly//instructions: +30.8M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr//instructions: +34.8M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr//instructions: +141.5M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv//instructions: +37.2M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr//instructions: +51.3M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat//instructions: +21.4M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof//instructions: +145.4M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars//instructions: +25.8M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Search//instructions: +148.5M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt//instructions: +63.3M (+0.4%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: -981.0M (-2.6%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.EvalNum//instructions: +35.0M (+0.6%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr//instructions: +33.0M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Internalize//instructions: +23.2M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Inv//instructions: +32.2M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Proof//instructions: +101.0M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq//instructions: +83.4M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Search//instructions: +117.2M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Util//instructions: +26.1M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Simproc//instructions: +27.3M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Attr//instructions: +19.7M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Canon//instructions: +46.8M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Core//instructions: +77.8M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: +241.2M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.EMatchAction//instructions: +26.5M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.EMatchTheorem//instructions: +135.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.EMatchTheoremParam//instructions: +25.5M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Ext//instructions: +23.1M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.ForallProp//instructions: +44.1M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Internalize//instructions: +118.9M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Intro//instructions: +48.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Inv//instructions: +41.0M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.MBTC//instructions: +35.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.MatchCond//instructions: +78.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Assert//instructions: +70.8M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Order.Internalize//instructions: +74.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.PP//instructions: +22.2M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Proof//instructions: +30.8M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Propagate//instructions: +85.5M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Simp//instructions: +21.8M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.SimpUtil//instructions: +26.7M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Split//instructions: +64.9M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat//instructions: +28.0M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt//instructions: +76.8M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.LoopProtection//instructions: +15.2M (+0.5%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.Main//instructions: +121.5M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.Rewrite//instructions: +114.3M (+0.4%)
  • 🟥 build/module/Lean.Meta.Tactic.Simp.Simproc//instructions: +41.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.Split//instructions: +37.3M (+0.3%)
  • 🟥 build/module/Lean.Meta.Tactic.SplitIf//instructions: +28.1M (+0.3%)
  • 🟥 build/module/Lean.Meta.WHNF//instructions: +59.2M (+0.4%)
  • 🟥 build/module/Lean.Parser//instructions: +18.5M (+0.4%)
  • 🟥 build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: +230.4M (+0.4%)
  • 🟥 build/module/Lean.Server.Completion.CompletionCollectors//instructions: +40.1M (+0.3%)
  • 🟥 build/module/Lean.Server.Completion.CompletionItemCompression//instructions: +36.7M (+0.4%)
  • 🟥 build/module/Lean.Server.Test.Cancel//instructions: +26.2M (+0.5%)
  • 🟥 build/module/Lean.Shell//instructions: +20.3M (+0.3%)
  • ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Zip//instructions: -57.6M (-0.5%)
  • ✅ build/module/Std.Do.PostCond//instructions: -33.9M (-0.4%)
  • 🟥 build/module/Std.Do.SPred.Notation//instructions: +90.7M (+0.4%)
  • 🟥 build/module/Std.Internal.Async.ContextAsync//instructions: +12.8M (+0.3%)
  • 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +117.8M (+0.4%)
  • 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz//instructions: +25.1M (+0.3%)
  • 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight//instructions: +84.5M (+0.3%)
  • 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult//instructions: +74.1M (+0.5%)
  • 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound//instructions: +94.2M (+0.4%)
  • 🟥 bv_decide_large_aig.lean//instructions: +288.4M (+0.6%)
  • 🟥 bv_decide_rewriter.lean//instructions: +55.4M (+0.4%)
  • 🟥 const_fold//instructions: +48.0M (+0.6%)
  • 🟥 grind_bitvec2.lean//instructions: +557.7M (+0.3%)
  • 🟥 grind_list2.lean//instructions: +232.7M (+0.4%)
  • 🟥 iterators (compiled)//instructions: +1.2M (+0.2%)
  • 🟥 iterators (elab)//instructions: +13.7M (+0.4%)
  • 🟥 iterators (interpreted)//instructions: +17.7M (+0.1%)
  • 🟥 language server startup with ileans//instructions: +130.7M (+0.5%)
  • 🟥 nat_repr//instructions: +60.8M (+1.8%)
  • 🟥 phashmap.lean//instructions: +108.9M (+1.0%)
  • 🟥 qsort//instructions: +128.0M (+0.8%)
  • ✅ riscv-ast.lean//instructions: -583.3M (-0.4%)
  • ✅ simp_bubblesort_256//instructions: -119.8M (-0.8%)
  • ✅ simp_congr//instructions: -149.0M (-0.8%)
  • ✅ simp_subexpr//instructions: -120.7M (-0.8%)

@Kha Kha force-pushed the push-kuuqqwxstpzx branch from 34e4c90 to 9f323e1 Compare December 29, 2025 12:36
@Kha
Copy link
Member Author

Kha commented Dec 29, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Dec 29, 2025

Benchmarking 9f323e1 (status) against 13c88f9 (status).

React with 👀 to be notified when the results are in. The command author is always notified.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Kha @leanprover-radar