perf: test uniqueness non-atomically first in `lean_dec_ref_cold` #11830

Kha · 2025-12-29T13:59:43Z

No description provided.

Kha · 2025-12-29T13:59:50Z

!bench

leanprover-radar · 2025-12-29T13:59:57Z

Benchmark results for 1acde3e against 13c88f9 are in! @Kha

Large changes (8🟥)

🟥 big_do//instructions: +126.2M (+0.4%)
🟥 deriv//instructions: +34.5M (+0.5%)
🟥 hashmap.lean//instructions: +42.6M (+1.1%)
🟥 rbmap//instructions: +188.5M (+1.2%)
🟥 rbmap_10//instructions: +164.5M (+1.0%)
🟥 rbmap_library//instructions: +120.9M (+0.9%)
🟥 treemap.lean//instructions: +40.9M (+0.2%)
🟥 unionfind//instructions: +395.6M (+1.6%)

Medium changes (21🟥)

🟥 Init.Data.BitVec.Lemmas//instructions: +741.9M (+0.5%)
🟥 Init.Data.List.Sublist async//instructions: +79.0M (+0.6%)
🟥 Init.Prelude async//instructions: +122.0M (+0.9%)
🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +1.6G (+0.6%)
🟥 Std.Data.Internal.List.Associative//instructions: +664.1M (+0.7%)
🟥 big_beq_rec//instructions: +139.4M (+0.6%)
🟥 big_match_partial//instructions: +136.5M (+0.7%)
🟥 big_omega.lean MT//instructions: +98.9M (+0.4%)
🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.0G (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.5G (+0.6%)
🟥 grind_bitvec2.lean//instructions: +1.1G (+0.5%)
🟥 identifier auto-completion//instructions: +411.5M (+0.5%)
🟥 ilean roundtrip//instructions: +103.7M (+0.4%)
🟥 iterators (elab)//instructions: +19.4M (+0.5%)
🟥 iterators (interpreted)//instructions: +22.1M (+0.1%)
🟥 liasolver//instructions: +20.8M (+0.5%)
🟥 mut_rec_wf//instructions: +222.5M (+0.7%)
🟥 parser//instructions: +214.3M (+0.4%)
🟥 rbmap_1//instructions: +11.7M (+0.1%)
🟥 riscv-ast.lean//instructions: +984.2M (+0.7%)
🟥 simp_local//instructions: +743.1M (+1.2%)

Small changes (706🟥)

🟥 big_beq//instructions: +74.1M (+0.6%)
🟥 big_deceq//instructions: +22.9M (+0.4%)
🟥 big_deceq_rec//instructions: +35.6M (+0.5%)
🟥 big_match//instructions: +51.1M (+0.4%)
🟥 big_match_nat_split//instructions: +75.4M (+0.5%)
🟥 big_omega.lean//instructions: +81.8M (+0.3%)
🟥 binarytrees.st//instructions: +9.0M (+0.0%)
🟥 binarytrees//instructions: +18.2M (+0.0%)
🟥 build//instructions: +76.4G (+0.5%)
🟥 build/module/Init.BinderPredicates//instructions: +15.2M (+0.6%)
🟥 build/module/Init.Control.Basic//instructions: +18.7M (+0.7%)
🟥 build/module/Init.Control.Except//instructions: +11.5M (+0.7%)
🟥 build/module/Init.Control.Lawful.Basic//instructions: +16.3M (+0.7%)
🟥 build/module/Init.Control.Lawful.Instances//instructions: +55.5M (+0.6%)
🟥 build/module/Init.Conv//instructions: +35.2M (+0.8%)
🟥 build/module/Init.Core//instructions: +88.6M (+0.7%)
🟥 build/module/Init.Data.Array.Attach//instructions: +89.0M (+0.6%)
🟥 build/module/Init.Data.Array.Basic//instructions: +111.4M (+0.7%)
🟥 build/module/Init.Data.Array.Bootstrap//instructions: +22.1M (+0.7%)
🟥 build/module/Init.Data.Array.Erase//instructions: +55.8M (+0.5%)
🟥 build/module/Init.Data.Array.Find//instructions: +86.0M (+0.6%)
🟥 build/module/Init.Data.Array.Lemmas//instructions: +440.8M (+0.6%)
🟥 build/module/Init.Data.Array.Lex.Lemmas//instructions: +89.5M (+0.6%)
🟥 build/module/Init.Data.Array.MapIdx//instructions: +73.4M (+0.6%)
🟥 build/module/Init.Data.Array.Monadic//instructions: +57.9M (+0.7%)
🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +101.0M (+0.6%)
🟥 build/module/Init.Data.Array.Range//instructions: +29.8M (+0.5%)
🟥 build/module/Init.Data.Array.Subarray//instructions: +15.4M (+0.8%)
🟥 build/module/Init.Data.Array.Zip//instructions: +37.1M (+0.6%)
🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +294.0M (+0.5%)
🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +795.7M (+0.5%)
🟥 build/module/Init.Data.Bool//instructions: +36.2M (+0.7%)
🟥 build/module/Init.Data.ByteArray.Basic//instructions: +18.2M (+0.6%)
🟥 build/module/Init.Data.ByteArray.Lemmas//instructions: +28.2M (+0.6%)
🟥 build/module/Init.Data.Char.Basic//instructions: +7.4M (+0.7%)
🟥 build/module/Init.Data.Fin.Fold//instructions: +32.9M (+0.6%)
🟥 build/module/Init.Data.Fin.Lemmas//instructions: +83.0M (+0.5%)
🟥 build/module/Init.Data.Float32//instructions: +6.7M (+0.7%)
🟥 build/module/Init.Data.Format.Basic//instructions: +21.0M (+0.6%)
🟥 build/module/Init.Data.Int.DivMod.Bootstrap//instructions: +42.0M (+0.6%)
🟥 build/module/Init.Data.Int.DivMod.Lemmas//instructions: +281.9M (+0.5%)
🟥 build/module/Init.Data.Int.Gcd//instructions: +43.6M (+0.7%)
🟥 build/module/Init.Data.Int.Lemmas//instructions: +43.1M (+0.7%)
🟥 build/module/Init.Data.Int.Order//instructions: +82.0M (+0.7%)
🟥 build/module/Init.Data.Iterators.Basic//instructions: +34.5M (+0.8%)
🟥 build/module/Init.Data.Iterators.Combinators.Monadic.FilterMap//instructions: +15.8M (+0.7%)
🟥 build/module/Init.Data.Iterators.Consumers.Loop//instructions: +16.0M (+0.6%)
🟥 build/module/Init.Data.Iterators.Consumers.Monadic.Loop//instructions: +31.5M (+0.6%)
🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.FilterMap//instructions: +163.2M (+0.6%)
🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.FlatMap//instructions: +50.9M (+0.6%)
🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: +315.7M (+0.6%)
🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap//instructions: +74.3M (+0.7%)
🟥 build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop//instructions: +96.6M (+0.6%)
🟥 build/module/Init.Data.Iterators.PostconditionMonad//instructions: +23.2M (+0.7%)
🟥 build/module/Init.Data.List.Attach//instructions: +84.9M (+0.8%)
🟥 build/module/Init.Data.List.Basic//instructions: +117.0M (+0.7%)
🟥 build/module/Init.Data.List.BasicAux//instructions: +20.4M (+0.7%)
🟥 build/module/Init.Data.List.Control//instructions: +24.0M (+0.7%)
🟥 build/module/Init.Data.List.Count//instructions: +23.3M (+0.6%)
🟥 build/module/Init.Data.List.Erase//instructions: +60.7M (+0.7%)
🟥 build/module/Init.Data.List.Find//instructions: +157.0M (+0.6%)
🟥 build/module/Init.Data.List.Lemmas//instructions: +327.4M (+0.6%)
🟥 build/module/Init.Data.List.Lex//instructions: +80.1M (+0.7%)
🟥 build/module/Init.Data.List.MapIdx//instructions: +75.1M (+0.6%)
🟥 build/module/Init.Data.List.Monadic//instructions: +80.9M (+0.6%)
🟥 build/module/Init.Data.List.Nat.InsertIdx//instructions: +24.9M (+0.5%)
🟥 build/module/Init.Data.List.Nat.Modify//instructions: +51.1M (+0.6%)
🟥 build/module/Init.Data.List.Nat.TakeDrop//instructions: +69.0M (+0.5%)
🟥 build/module/Init.Data.List.OfFn//instructions: +15.0M (+0.6%)
🟥 build/module/Init.Data.List.Pairwise//instructions: +36.4M (+0.8%)
🟥 build/module/Init.Data.List.Perm//instructions: +52.0M (+0.6%)
🟥 build/module/Init.Data.List.Sort.Impl//instructions: +80.4M (+0.5%)
🟥 build/module/Init.Data.List.Sort.Lemmas//instructions: +131.2M (+0.6%)
🟥 build/module/Init.Data.List.Sublist//instructions: +88.5M (+0.6%)
🟥 build/module/Init.Data.List.TakeDrop//instructions: +38.6M (+0.6%)
🟥 build/module/Init.Data.List.ToArray//instructions: +146.7M (+0.5%)
🟥 build/module/Init.Data.List.Zip//instructions: +85.0M (+0.6%)
🟥 build/module/Init.Data.Nat.Basic//instructions: +67.2M (+0.7%)
🟥 build/module/Init.Data.Nat.Bitwise.Lemmas//instructions: +67.3M (+0.6%)
🟥 build/module/Init.Data.Nat.Div.Basic//instructions: +28.6M (+0.6%)
🟥 build/module/Init.Data.Nat.Fold//instructions: +74.0M (+0.6%)
🟥 build/module/Init.Data.Nat.Gcd//instructions: +25.1M (+0.8%)
🟥 build/module/Init.Data.Nat.Lemmas//instructions: +150.4M (+0.5%)
🟥 build/module/Init.Data.NeZero//instructions: +4.7M (+0.7%)
🟥 build/module/Init.Data.Option.Attach//instructions: +36.2M (+0.6%)
🟥 build/module/Init.Data.Option.Basic//instructions: +15.5M (+0.7%)
🟥 build/module/Init.Data.Option.Lemmas//instructions: +140.2M (+0.6%)
🟥 build/module/Init.Data.Ord.Array//instructions: +25.2M (+0.6%)
🟥 build/module/Init.Data.Ord.Basic//instructions: +35.4M (+0.7%)
🟥 build/module/Init.Data.Ord.SInt//instructions: +19.0M (+0.6%)
🟥 build/module/Init.Data.Order.Lemmas//instructions: +23.6M (+0.7%)
🟥 build/module/Init.Data.Order.LemmasExtra//instructions: +10.5M (+0.6%)
🟥 build/module/Init.Data.Order.Ord//instructions: +33.9M (+0.7%)
🟥 build/module/Init.Data.Order.PackageFactories//instructions: +58.4M (+0.8%)
🟥 build/module/Init.Data.Range.Polymorphic.Basic//instructions: +14.3M (+0.7%)
🟥 build/module/Init.Data.Range.Polymorphic.IntLemmas//instructions: +192.0M (+0.5%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: +414.0M (+0.7%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Range.Polymorphic.NatLemmas//instructions: +251.4M (+0.5%)
🟥 build/module/Init.Data.Range.Polymorphic.PRange//instructions: +29.0M (+0.6%)
🟥 build/module/Init.Data.Range.Polymorphic.RangeIterator//instructions: +161.6M (+0.6%)
🟥 build/module/Init.Data.Range.Polymorphic.UpwardEnumerable//instructions: +22.9M (+0.8%)
🟥 build/module/Init.Data.Rat.Lemmas//instructions: +93.6M (+0.7%)
🟥 build/module/Init.Data.Repr//instructions: +16.8M (+0.8%)
🟥 build/module/Init.Data.SInt.Basic//instructions: +25.5M (+0.7%)
🟥 build/module/Init.Data.SInt.Bitwise//instructions: +102.2M (+0.7%)
🟥 build/module/Init.Data.SInt.Lemmas//instructions: +438.2M (+0.6%)
🟥 build/module/Init.Data.Slice.Array.Lemmas//instructions: +79.7M (+0.6%)
🟥 build/module/Init.Data.Slice.List.Lemmas//instructions: +38.4M (+0.7%)
🟥 build/module/Init.Data.Slice.Notation//instructions: +13.5M (+0.6%)
🟥 build/module/Init.Data.String.Basic//instructions: +312.7M (+0.8%)
🟥 build/module/Init.Data.String.Defs//instructions: +22.3M (+0.7%)
🟥 build/module/Init.Data.String.Grind//instructions: +22.1M (+0.6%)
🟥 build/module/Init.Data.String.Pattern.String//instructions: +83.4M (+0.5%)
🟥 build/module/Init.Data.String.PosRaw//instructions: +14.3M (+0.6%)
🟥 build/module/Init.Data.String.Search//instructions: +41.5M (+0.7%)
🟥 build/module/Init.Data.String.Slice//instructions: +114.8M (+0.6%)
🟥 build/module/Init.Data.UInt.Bitwise//instructions: +196.5M (+0.7%)
🟥 build/module/Init.Data.Vector.Algebra//instructions: +42.8M (+0.6%)
🟥 build/module/Init.Data.Vector.Attach//instructions: +68.9M (+0.7%)
🟥 build/module/Init.Data.Vector.Basic//instructions: +68.8M (+0.6%)
🟥 build/module/Init.Data.Vector.Find//instructions: +41.4M (+0.6%)
🟥 build/module/Init.Data.Vector.Lemmas//instructions: +355.6M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Vector.Lex//instructions: +42.8M (+0.6%)
🟥 build/module/Init.Data.Vector.MapIdx//instructions: +55.3M (+0.6%)
🟥 build/module/Init.Data.Vector.Monadic//instructions: +33.0M (+0.6%)
🟥 build/module/Init.Data.Vector.OfFn//instructions: +36.5M (+0.5%)
🟥 build/module/Init.Data.Vector.Perm//instructions: +35.1M (+0.5%)
🟥 build/module/Init.Data.Vector.Range//instructions: +32.7M (+0.7%)
🟥 build/module/Init.GetElem//instructions: +31.3M (+0.7%)
🟥 build/module/Init.Grind.Config//instructions: +14.6M (+0.4%)
🟥 build/module/Init.Grind.Interactive//instructions: +18.8M (+0.7%)
🟥 build/module/Init.Grind.Module.Envelope//instructions: +53.1M (+0.5%)
🟥 build/module/Init.Grind.Ordered.Field//instructions: +26.3M (+0.7%)
🟥 build/module/Init.Grind.Ordered.Ring//instructions: +41.5M (+0.7%)
🟥 build/module/Init.Grind.Ring.Basic//instructions: +57.7M (+0.6%)
🟥 build/module/Init.Grind.Ring.Envelope//instructions: +66.8M (+0.5%)
🟥 build/module/Init.GrindInstances.ToInt//instructions: +66.6M (+0.5%)
🟥 build/module/Init.LawfulBEqTactics//instructions: +14.0M (+0.6%)
🟥 build/module/Init.Meta.Defs//instructions: +98.4M (+0.7%)
🟥 build/module/Init.Meta//instructions: +34.5M (+0.7%)
🟥 build/module/Init.MetaTypes//instructions: +19.2M (+0.6%)
🟥 build/module/Init.Notation//instructions: +151.2M (+0.7%) (reduced significance based on absolute threshold)
🟥 build/module/Init.NotationExtra//instructions: +100.2M (+0.7%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Omega.Constraint//instructions: +40.0M (+0.7%)
🟥 build/module/Init.Omega.IntList//instructions: +50.4M (+0.7%)
🟥 build/module/Init.Prelude//instructions: +134.4M (+0.9%) (reduced significance based on absolute threshold)
🟥 build/module/Init.PropLemmas//instructions: +34.9M (+0.7%)
🟥 build/module/Init.Simproc//instructions: +42.7M (+0.7%)
🟥 build/module/Init.SizeOf//instructions: +11.1M (+0.8%)
🟥 build/module/Init.System.ST//instructions: +15.3M (+0.8%)
🟥 build/module/Init.Tactics//instructions: +109.9M (+0.8%) (reduced significance based on absolute threshold)
🟥 build/module/Init.TacticsExtra//instructions: +19.9M (+0.7%)
🟥 build/module/Init.WF//instructions: +14.8M (+0.7%)
🟥 build/module/Init.WFExtrinsicFix//instructions: +15.0M (+0.7%)
🟥 build/module/Init.WFTactics//instructions: +15.1M (+0.7%)
🟥 build/module/Lake.Build.Common//instructions: +143.4M (+0.5%)
🟥 build/module/Lake.Build.Data//instructions: +29.6M (+0.7%)
🟥 build/module/Lake.Build.Infos//instructions: +17.7M (+0.5%)
🟥 build/module/Lake.Build.Job.Monad//instructions: +36.4M (+0.5%)
🟥 build/module/Lake.Build.Library//instructions: +42.1M (+0.5%)
🟥 build/module/Lake.Build.Module//instructions: +240.8M (+0.4%)
🟥 build/module/Lake.Build.Package//instructions: +50.4M (+0.6%)
🟥 build/module/Lake.Build.Run//instructions: +36.8M (+0.6%)
🟥 build/module/Lake.Build.Target.Fetch//instructions: +45.6M (+0.6%)
🟥 build/module/Lake.Build.Targets//instructions: +26.0M (+0.6%)
🟥 build/module/Lake.CLI.Build//instructions: +20.6M (+0.5%)
🟥 build/module/Lake.CLI.Init//instructions: +35.0M (+0.6%)
🟥 build/module/Lake.CLI.Main//instructions: +241.7M (+0.7%)
🟥 build/module/Lake.CLI.Translate.Lean//instructions: +125.0M (+0.7%)
🟥 build/module/Lake.CLI.Translate.Toml//instructions: +58.9M (+0.6%)
🟥 build/module/Lake.Config.Cache//instructions: +42.5M (+0.6%)
🟥 build/module/Lake.Config.Env//instructions: +19.8M (+0.6%)
🟥 build/module/Lake.Config.LeanConfig//instructions: +26.1M (+0.6%)
🟥 build/module/Lake.Config.Meta//instructions: +55.3M (+0.5%)
🟥 build/module/Lake.Config.Module//instructions: +15.9M (+0.6%)
🟥 build/module/Lake.Config.Package//instructions: +19.4M (+0.5%)
🟥 build/module/Lake.Config.PackageConfig//instructions: +45.6M (+0.6%)
🟥 build/module/Lake.Config.Workspace//instructions: +16.2M (+0.6%)
🟥 build/module/Lake.DSL.Package//instructions: +27.9M (+0.7%)
🟥 build/module/Lake.DSL.Syntax//instructions: +13.4M (+0.6%)
🟥 build/module/Lake.DSL.Targets//instructions: +76.2M (+0.7%)
🟥 build/module/Lake.Load.Lean.Elab//instructions: +28.2M (+0.6%)
🟥 build/module/Lake.Load.Lean.Eval//instructions: +22.9M (+0.5%)
🟥 build/module/Lake.Load.Materialize//instructions: +25.2M (+0.6%)
🟥 build/module/Lake.Load.Resolve//instructions: +74.9M (+0.6%)
🟥 build/module/Lake.Load.Toml//instructions: +92.3M (+0.5%)
🟥 build/module/Lake.Toml.Elab.Expression//instructions: +35.1M (+0.6%)
🟥 build/module/Lake.Toml.Elab.Value//instructions: +33.6M (+0.6%)
🟥 build/module/Lake.Toml.Grammar//instructions: +32.6M (+0.7%)
🟥 build/module/Lake.Toml.ParserUtil//instructions: +19.8M (+0.7%)
🟥 build/module/Lake.Util.Binder//instructions: +23.2M (+0.6%)
🟥 build/module/Lake.Util.EStateT//instructions: +14.8M (+0.7%)
🟥 build/module/Lake.Util.Log//instructions: +41.6M (+0.7%)
🟥 build/module/Lake.Util.OpaqueType//instructions: +18.5M (+0.6%)
🟥 build/module/Lake.Util.Version//instructions: +63.5M (+0.7%)
🟥 build/module/Lean.AddDecl//instructions: +31.0M (+0.5%)
🟥 build/module/Lean.Compiler.IR.EmitC//instructions: +71.8M (+0.6%)
🟥 build/module/Lean.Compiler.IR.EmitLLVM//instructions: +251.6M (+0.5%)
🟥 build/module/Lean.Compiler.IR.ToIR//instructions: +38.0M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Basic//instructions: +75.2M (+0.8%)
🟥 build/module/Lean.Compiler.LCNF.Check//instructions: +52.6M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Closure//instructions: +19.4M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.CompilerM//instructions: +38.8M (+0.7%)
🟥 build/module/Lean.Compiler.LCNF.ElimDeadBranches//instructions: +70.0M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Internalize//instructions: +21.2M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.JoinPoints//instructions: +65.1M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.LambdaLifting//instructions: +28.0M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Main//instructions: +31.3M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Passes//instructions: +14.0M (+0.5%)
🟥 build/module/Lean.Compiler.LCNF.PrettyPrinter//instructions: +23.4M (+0.7%)
🟥 build/module/Lean.Compiler.LCNF.Probing//instructions: +29.8M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Simp.ConstantFold//instructions: +91.1M (+0.7%)
🟥 build/module/Lean.Compiler.LCNF.Simp.JpCases//instructions: +37.4M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Simp.Main//instructions: +41.5M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Simp.SimpM//instructions: +27.6M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Simp//instructions: +12.5M (+0.5%)
🟥 build/module/Lean.Compiler.LCNF.Specialize//instructions: +87.1M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.StructProjCases//instructions: +23.5M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Testing//instructions: +23.6M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.ToDecl//instructions: +26.3M (+0.5%)
🟥 build/module/Lean.Compiler.LCNF.ToLCNF//instructions: +130.4M (+0.7%)
🟥 build/module/Lean.Compiler.LCNF.ToMono//instructions: +62.6M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Types//instructions: +32.1M (+0.6%)
🟥 build/module/Lean.Compiler.LCNF.Visibility//instructions: +33.5M (+0.5%)
🟥 build/module/Lean.Compiler.NameMangling//instructions: +47.8M (+0.5%)
🟥 build/module/Lean.CoreM//instructions: +70.4M (+0.6%)
🟥 build/module/Lean.Data.AssocList//instructions: +9.9M (+0.7%)
🟥 build/module/Lean.Data.Json.Elab//instructions: +24.8M (+0.6%)
🟥 build/module/Lean.Data.Json.Printer//instructions: +33.5M (+0.6%)
🟥 build/module/Lean.Data.JsonRpc//instructions: +42.2M (+0.7%)
🟥 build/module/Lean.Data.Lsp.Capabilities//instructions: +24.2M (+0.5%)
🟥 build/module/Lean.Data.Lsp.CodeActions//instructions: +26.6M (+0.7%)
🟥 build/module/Lean.Data.Lsp.InitShutdown//instructions: +15.7M (+0.6%)
🟥 build/module/Lean.Data.Lsp.Ipc//instructions: +44.3M (+0.6%)
🟥 build/module/Lean.Data.Lsp.LanguageFeatures//instructions: +149.2M (+0.7%)
🟥 build/module/Lean.Data.RBMap//instructions: +46.9M (+0.7%)
🟥 build/module/Lean.Data.Xml.Parser//instructions: +63.1M (+0.6%)
🟥 build/module/Lean.DocString.Add//instructions: +35.0M (+0.6%)
🟥 build/module/Lean.DocString.Extension//instructions: +43.6M (+0.6%)
🟥 build/module/Lean.DocString.Formatter//instructions: +41.5M (+0.6%)
🟥 build/module/Lean.DocString.Links//instructions: +14.4M (+0.6%)
🟥 build/module/Lean.DocString.Markdown//instructions: +38.3M (+0.8%)
🟥 build/module/Lean.DocString.Parser//instructions: +84.2M (+0.7%)
🟥 build/module/Lean.DocString.Syntax//instructions: +10.4M (+0.5%)
🟥 build/module/Lean.DocString.Types//instructions: +75.8M (+0.8%)
🟥 build/module/Lean.Elab.App//instructions: +283.5M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Binders//instructions: +139.9M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.BuiltinCommand//instructions: +128.1M (+0.6%)
🟥 build/module/Lean.Elab.BuiltinEvalCommand//instructions: +56.9M (+0.5%)
🟥 build/module/Lean.Elab.BuiltinNotation//instructions: +127.4M (+0.6%)
🟥 build/module/Lean.Elab.BuiltinTerm//instructions: +80.1M (+0.5%)
🟥 build/module/Lean.Elab.Calc//instructions: +33.4M (+0.6%)
🟥 build/module/Lean.Elab.Coinductive//instructions: +37.0M (+0.5%)
🟥 build/module/Lean.Elab.Command//instructions: +94.5M (+0.6%)
🟥 build/module/Lean.Elab.ComputedFields//instructions: +37.6M (+0.5%)
🟥 build/module/Lean.Elab.DeclNameGen//instructions: +60.3M (+0.5%)
🟥 build/module/Lean.Elab.Declaration//instructions: +73.3M (+0.6%)
🟥 build/module/Lean.Elab.Deriving.BEq//instructions: +69.1M (+0.6%)
🟥 build/module/Lean.Elab.Deriving.Basic//instructions: +70.6M (+0.6%)
🟥 build/module/Lean.Elab.Deriving.DecEq//instructions: +72.3M (+0.6%)
🟥 build/module/Lean.Elab.Deriving.FromToJson//instructions: +71.5M (+0.5%)
🟥 build/module/Lean.Elab.Deriving.Hashable//instructions: +30.1M (+0.5%)
🟥 build/module/Lean.Elab.Deriving.Inhabited//instructions: +42.3M (+0.6%)
🟥 build/module/Lean.Elab.Deriving.Ord//instructions: +66.3M (+0.7%)
🟥 build/module/Lean.Elab.Deriving.Repr//instructions: +39.9M (+0.5%)
🟥 build/module/Lean.Elab.Deriving.ToExpr//instructions: +65.4M (+0.5%)
🟥 build/module/Lean.Elab.Deriving.Util//instructions: +41.8M (+0.6%)
🟥 build/module/Lean.Elab.Do.Basic//instructions: +101.1M (+0.6%)
🟥 build/module/Lean.Elab.Do.Legacy//instructions: +434.4M (+0.7%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.DocString.Builtin.Keywords//instructions: +114.2M (+0.6%)
🟥 build/module/Lean.Elab.DocString.Builtin.Postponed//instructions: +32.1M (+0.6%)
🟥 build/module/Lean.Elab.DocString.Builtin//instructions: +358.9M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.DocString//instructions: +368.5M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.ElabRules//instructions: +42.0M (+0.6%)
🟥 build/module/Lean.Elab.ErrorExplanation//instructions: +37.4M (+0.6%)
🟥 build/module/Lean.Elab.Extra//instructions: +71.8M (+0.6%)
🟥 build/module/Lean.Elab.Frontend//instructions: +20.0M (+0.6%)
🟥 build/module/Lean.Elab.GuardMsgs//instructions: +44.1M (+0.6%)
🟥 build/module/Lean.Elab.Inductive//instructions: +64.7M (+0.5%)
🟥 build/module/Lean.Elab.InfoTree.Main//instructions: +36.8M (+0.6%)
🟥 build/module/Lean.Elab.LetRec//instructions: +38.0M (+0.5%)
🟥 build/module/Lean.Elab.MacroArgUtil//instructions: +64.0M (+0.7%)
🟥 build/module/Lean.Elab.MacroRules//instructions: +27.5M (+0.6%)
🟥 build/module/Lean.Elab.Match//instructions: +205.0M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.MatchExpr//instructions: +36.8M (+0.7%)
🟥 build/module/Lean.Elab.Mixfix//instructions: +26.7M (+0.6%)
🟥 build/module/Lean.Elab.MutualDef//instructions: +253.7M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.MutualInductive//instructions: +268.6M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Notation//instructions: +40.9M (+0.6%)
🟥 build/module/Lean.Elab.Open//instructions: +22.2M (+0.6%)
🟥 build/module/Lean.Elab.Parallel//instructions: +57.2M (+0.6%)
🟥 build/module/Lean.Elab.ParseImportsFast//instructions: +20.1M (+0.7%)
🟥 build/module/Lean.Elab.PatternVar//instructions: +107.0M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.Basic//instructions: +50.3M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.Eqns//instructions: +61.1M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.FixedParams//instructions: +66.5M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.Main//instructions: +67.4M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.MkInhabitant//instructions: +23.7M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Eqns//instructions: +18.5M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Induction//instructions: +67.5M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Main//instructions: +38.6M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.Structural.BRecOn//instructions: +46.3M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.Structural.Eqns//instructions: +31.7M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.Structural.FindRecArg//instructions: +71.1M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.Structural.IndPred//instructions: +34.4M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.Structural.Main//instructions: +33.4M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.TerminationHint//instructions: +23.6M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.TerminationMeasure//instructions: +26.7M (+0.6%)
🟥 build/module/Lean.Elab.PreDefinition.WF.Fix//instructions: +54.8M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.WF.GuessLex//instructions: +107.4M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.WF.Main//instructions: +26.5M (+0.5%)
🟥 build/module/Lean.Elab.PreDefinition.WF.Preprocess//instructions: +27.7M (+0.4%)
🟥 build/module/Lean.Elab.PreDefinition.WF.Unfold//instructions: +44.5M (+0.5%)
🟥 build/module/Lean.Elab.Print//instructions: +51.5M (+0.5%)
🟥 build/module/Lean.Elab.Quotation.Precheck//instructions: +36.5M (+0.6%)
🟥 build/module/Lean.Elab.Quotation//instructions: +206.1M (+0.6%)
🟥 build/module/Lean.Elab.StructInst//instructions: +257.7M (+0.5%)
🟥 build/module/Lean.Elab.StructInstHint//instructions: +20.1M (+0.6%)
🟥 build/module/Lean.Elab.Structure//instructions: +316.6M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Syntax//instructions: +135.3M (+0.7%)
🟥 build/module/Lean.Elab.SyntheticMVars//instructions: +101.8M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVCheck//instructions: +13.4M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify//instructions: +48.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVDecide//instructions: +71.9M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.BVTrace//instructions: +14.0M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC//instructions: +49.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums//instructions: +61.6M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: +245.1M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures//instructions: +18.0M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.TypeAnalysis//instructions: +52.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize//instructions: +23.9M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Basic//instructions: +112.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.BuiltinTactic//instructions: +157.9M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Config//instructions: +50.5M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Conv.Basic//instructions: +38.6M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Conv.Congr//instructions: +63.3M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Conv.Simp//instructions: +19.4M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.Attr//instructions: +35.3M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.LetElim//instructions: +33.7M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Cases//instructions: +37.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Delab//instructions: +21.0M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.MGoal//instructions: +32.2M (+0.7%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Pure//instructions: +26.0M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Refine//instructions: +27.4M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Revert//instructions: +19.4M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Do.ProofMode.Specialize//instructions: +42.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.Spec//instructions: +78.7M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.Syntax//instructions: +27.6M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen.Basic//instructions: +75.5M (+0.7%)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen.Split//instructions: +14.8M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen.SuggestInvariant//instructions: +87.8M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen//instructions: +251.4M (+0.5%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.ElabTerm//instructions: +75.4M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Ext//instructions: +67.8M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.Basic//instructions: +86.9M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.BuiltinTactic//instructions: +115.3M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.Config//instructions: +54.7M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Grind.Lint//instructions: +40.8M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.Main//instructions: +92.2M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.Param//instructions: +70.5M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Grind.ShowState//instructions: +35.7M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Guard//instructions: +37.6M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Induction//instructions: +192.2M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Lets//instructions: +26.7M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.LibrarySearch//instructions: +30.9M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Monotonicity//instructions: +45.5M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.NormCast//instructions: +74.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Omega.Core//instructions: +71.3M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Omega.Frontend//instructions: +207.4M (+0.5%)
🟥 build/module/Lean.Elab.Tactic.Omega.OmegaM//instructions: +58.9M (+0.7%)
🟥 build/module/Lean.Elab.Tactic.RCases//instructions: +89.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Rewrite//instructions: +32.1M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Rewrites//instructions: +20.7M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Simp//instructions: +141.6M (+0.7%)
🟥 build/module/Lean.Elab.Tactic.SimpTrace//instructions: +76.7M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.SolveByElim//instructions: +35.4M (+0.6%)
🟥 build/module/Lean.Elab.Tactic.Try//instructions: +251.4M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Term.TermElabM//instructions: +225.0M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Util//instructions: +26.4M (+0.6%)
🟥 build/module/Lean.Environment//instructions: +149.0M (+0.7%)
🟥 build/module/Lean.ErrorExplanation//instructions: +34.6M (+0.6%)
🟥 build/module/Lean.Expr//instructions: +122.5M (+0.7%)
🟥 build/module/Lean.IdentifierSuggestion//instructions: +25.3M (+0.5%)
🟥 build/module/Lean.Language.Lean//instructions: +55.9M (+0.6%)
🟥 build/module/Lean.Level//instructions: +91.6M (+0.7%)
🟥 build/module/Lean.LibrarySuggestions.Basic//instructions: +49.4M (+0.6%)
🟥 build/module/Lean.LibrarySuggestions.MePo//instructions: +21.4M (+0.6%)
🟥 build/module/Lean.LibrarySuggestions.SineQuaNon//instructions: +29.6M (+0.6%)
🟥 build/module/Lean.Linter.List//instructions: +41.2M (+0.6%)
🟥 build/module/Lean.Linter.MissingDocs//instructions: +58.0M (+0.6%)
🟥 build/module/Lean.Linter.UnusedVariables//instructions: +71.8M (+0.6%)
🟥 build/module/Lean.Message//instructions: +59.5M (+0.7%)
🟥 build/module/Lean.Meta.AbstractNestedProofs//instructions: +17.2M (+0.6%)
🟥 build/module/Lean.Meta.AppBuilder//instructions: +72.2M (+0.6%)
🟥 build/module/Lean.Meta.ArgsPacker//instructions: +48.6M (+0.5%)
🟥 build/module/Lean.Meta.Basic//instructions: +212.6M (+0.7%)
🟥 build/module/Lean.Meta.Canonicalizer//instructions: +21.9M (+0.7%)
🟥 build/module/Lean.Meta.Check//instructions: +45.5M (+0.6%)
🟥 build/module/Lean.Meta.Closure//instructions: +52.4M (+0.7%)
🟥 build/module/Lean.Meta.Coe//instructions: +37.2M (+0.5%)
🟥 build/module/Lean.Meta.CongrTheorems//instructions: +58.2M (+0.7%)
🟥 build/module/Lean.Meta.Constructions.BRecOn//instructions: +36.1M (+0.5%)
🟥 build/module/Lean.Meta.Constructions.CasesOnSameCtor//instructions: +24.6M (+0.5%)
🟥 build/module/Lean.Meta.Constructions.CtorElim//instructions: +26.5M (+0.5%)
🟥 build/module/Lean.Meta.Constructions.NoConfusion//instructions: +53.1M (+0.5%)
🟥 build/module/Lean.Meta.DiscrTree//instructions: +59.3M (+0.7%)
🟥 build/module/Lean.Meta.Eqns//instructions: +35.8M (+0.7%)
🟥 build/module/Lean.Meta.ExprDefEq//instructions: +179.5M (+0.6%)
🟥 build/module/Lean.Meta.Hint//instructions: +35.2M (+0.6%)
🟥 build/module/Lean.Meta.IndPredBelow//instructions: +90.9M (+0.6%)
🟥 build/module/Lean.Meta.InferType//instructions: +48.9M (+0.7%)
🟥 build/module/Lean.Meta.Injective//instructions: +93.7M (+0.6%)
🟥 build/module/Lean.Meta.Instances//instructions: +50.4M (+0.7%)
🟥 build/module/Lean.Meta.LazyDiscrTree//instructions: +99.3M (+0.6%)
🟥 build/module/Lean.Meta.LetToHave//instructions: +67.1M (+0.6%)
🟥 build/module/Lean.Meta.LevelDefEq//instructions: +19.0M (+0.6%)
🟥 build/module/Lean.Meta.LitValues//instructions: +37.6M (+0.8%)
🟥 build/module/Lean.Meta.Match.Basic//instructions: +29.6M (+0.6%)
🟥 build/module/Lean.Meta.Match.Match//instructions: +150.1M (+0.6%)
🟥 build/module/Lean.Meta.Match.MatchEqs//instructions: +58.0M (+0.6%)
🟥 build/module/Lean.Meta.Match.MatcherApp.Transform//instructions: +56.8M (+0.6%)
🟥 build/module/Lean.Meta.Match.Rewrite//instructions: +29.0M (+0.6%)
🟥 build/module/Lean.Meta.Match.SolveOverlap//instructions: +27.3M (+0.5%)
🟥 build/module/Lean.Meta.MethodSpecs//instructions: +32.3M (+0.5%)
🟥 build/module/Lean.Meta.MkIffOfInductiveProp//instructions: +49.6M (+0.6%)
🟥 build/module/Lean.Meta.Offset//instructions: +28.9M (+0.6%)
🟥 build/module/Lean.Meta.SizeOf//instructions: +72.6M (+0.6%)
🟥 build/module/Lean.Meta.SplitSparseCasesOn//instructions: +17.8M (+0.5%)
🟥 build/module/Lean.Meta.Structure//instructions: +33.9M (+0.6%)
🟥 build/module/Lean.Meta.SynthInstance//instructions: +105.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.AC.Main//instructions: +61.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Apply//instructions: +37.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Backtrack//instructions: +38.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Cases//instructions: +44.9M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Congr//instructions: +15.6M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Contradiction//instructions: +47.2M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.ElimInfo//instructions: +37.6M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +332.7M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.AC.Eq//instructions: +200.8M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.AC.Proof//instructions: +105.0M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.AC.Seq//instructions: +59.5M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.AC.Util//instructions: +34.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr//instructions: +251.1M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Functions//instructions: +16.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize//instructions: +66.4M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM//instructions: +13.0M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Proof//instructions: +168.3M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Reify//instructions: +81.5M (+0.4%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.RingId//instructions: +25.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.RingM//instructions: +25.1M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly//instructions: +37.0M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM//instructions: +34.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing//instructions: +26.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr//instructions: +34.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr//instructions: +185.8M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv//instructions: +42.3M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr//instructions: +56.9M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat//instructions: +31.2M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof//instructions: +230.1M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars//instructions: +35.2M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Search//instructions: +173.8M (+0.5%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt//instructions: +103.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: +445.2M (+1.2%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Util//instructions: +38.7M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Var//instructions: +33.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.EvalNum//instructions: +31.5M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.FieldNormNum//instructions: +45.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr//instructions: +34.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Internalize//instructions: +27.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Inv//instructions: +33.5M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Model//instructions: +19.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule//instructions: +38.1M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Proof//instructions: +155.9M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq//instructions: +91.1M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Reify//instructions: +29.0M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Search//instructions: +122.4M (+0.4%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Util//instructions: +37.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Propagate//instructions: +18.6M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Simproc//instructions: +42.7M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Attr//instructions: +38.0M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Canon//instructions: +59.1M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.CheckResult//instructions: +15.9M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Core//instructions: +88.1M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: +298.3M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.EMatchAction//instructions: +36.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.EMatchTheorem//instructions: +241.0M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.EMatchTheoremParam//instructions: +30.5M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.ForallProp//instructions: +58.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Internalize//instructions: +139.5M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Intro//instructions: +60.8M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Inv//instructions: +41.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.MBTC//instructions: +41.2M (+0.4%)
🟥 build/module/Lean.Meta.Tactic.Grind.Main//instructions: +64.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.MatchCond//instructions: +104.6M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Order.Assert//instructions: +82.0M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Order.Internalize//instructions: +89.3M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.Order.OrderM//instructions: +15.7M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Order.Proof//instructions: +27.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Order.StructId//instructions: +19.2M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.PP//instructions: +43.1M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Proof//instructions: +45.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Propagate//instructions: +92.2M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.PropagatorAttr//instructions: +15.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.ProveEq//instructions: +38.5M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Grind.RegisterCommand//instructions: +11.9M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Grind.Simp//instructions: +23.3M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.SimpUtil//instructions: +37.9M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Split//instructions: +84.6M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Grind.Types//instructions: +307.3M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Grind.Util//instructions: +29.0M (+0.4%)
🟥 build/module/Lean.Meta.Tactic.Lets//instructions: +58.0M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.LibrarySearch//instructions: +33.2M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Rewrites//instructions: +41.2M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.Arith.Int.Basic//instructions: +44.1M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.Arith.Int.Simp//instructions: +20.3M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Simp.Arith.Nat.Basic//instructions: +34.0M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec//instructions: +75.8M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char//instructions: +20.5M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin//instructions: +50.8M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int//instructions: +42.7M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat//instructions: +56.6M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt//instructions: +149.1M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.String//instructions: +13.7M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt//instructions: +113.4M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.Simp.Diagnostics//instructions: +13.7M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Simp.LoopProtection//instructions: +17.0M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Simp.Main//instructions: +190.7M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.Rewrite//instructions: +142.5M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Meta.Tactic.Simp.SimpAll//instructions: +28.3M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.SimpTheorems//instructions: +60.3M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.Simproc//instructions: +74.2M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Simp.Types//instructions: +103.5M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.SolveByElim//instructions: +29.8M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Split//instructions: +71.5M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.SplitIf//instructions: +54.5M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Subst//instructions: +33.0M (+0.5%)
🟥 build/module/Lean.Meta.Tactic.Try.Collect//instructions: +33.2M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.TryThis//instructions: +63.6M (+0.7%)
🟥 build/module/Lean.Meta.Tactic.UnifyEq//instructions: +17.4M (+0.6%)
🟥 build/module/Lean.Meta.Tactic.Util//instructions: +29.4M (+0.5%)
🟥 build/module/Lean.Meta.Transform//instructions: +35.6M (+0.6%)
🟥 build/module/Lean.Meta.UnificationHint//instructions: +27.8M (+0.6%)
🟥 build/module/Lean.Meta.WHNF//instructions: +94.7M (+0.6%)
🟥 build/module/Lean.MetavarContext//instructions: +85.7M (+0.6%)
🟥 build/module/Lean.Parser.Basic//instructions: +71.8M (+0.7%)
🟥 build/module/Lean.Parser.Command//instructions: +95.9M (+0.7%)
🟥 build/module/Lean.Parser.Do//instructions: +46.3M (+0.7%)
🟥 build/module/Lean.Parser.Extension//instructions: +62.8M (+0.7%)
🟥 build/module/Lean.Parser.Extra//instructions: +37.0M (+0.7%)
🟥 build/module/Lean.Parser.Module//instructions: +26.2M (+0.6%)
🟥 build/module/Lean.Parser.Syntax//instructions: +38.0M (+0.7%)
🟥 build/module/Lean.Parser.Tactic.Doc//instructions: +40.1M (+0.6%)
🟥 build/module/Lean.Parser.Term.Basic//instructions: +27.0M (+0.8%)
🟥 build/module/Lean.Parser.Term//instructions: +137.5M (+0.8%)
🟥 build/module/Lean.Parser.Types//instructions: +27.9M (+0.7%)
🟥 build/module/Lean.Parser//instructions: +24.3M (+0.6%)
🟥 build/module/Lean.PrettyPrinter.Delaborator.Basic//instructions: +57.5M (+0.6%)
🟥 build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: +324.3M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.PrettyPrinter.Delaborator.TopDownAnalyze//instructions: +146.9M (+0.6%)
🟥 build/module/Lean.PrettyPrinter.Formatter//instructions: +69.1M (+0.7%)
🟥 build/module/Lean.PrettyPrinter//instructions: +17.1M (+0.6%)
🟥 build/module/Lean.ResolveName//instructions: +34.2M (+0.6%)
🟥 build/module/Lean.Server.CodeActions.Provider//instructions: +29.0M (+0.6%)
🟥 build/module/Lean.Server.CodeActions.UnknownIdentifier//instructions: +35.7M (+0.6%)
🟥 build/module/Lean.Server.Completion.CompletionCollectors//instructions: +78.8M (+0.6%)
🟥 build/module/Lean.Server.Completion.CompletionInfoSelection//instructions: +12.3M (+0.6%)
🟥 build/module/Lean.Server.Completion.CompletionItemCompression//instructions: +53.2M (+0.6%)
🟥 build/module/Lean.Server.Completion.CompletionUtils//instructions: +22.2M (+0.6%)
🟥 build/module/Lean.Server.Completion.ImportCompletion//instructions: +17.6M (+0.5%)
🟥 build/module/Lean.Server.FileWorker.RequestHandling//instructions: +116.1M (+0.6%)
🟥 build/module/Lean.Server.FileWorker.SemanticHighlighting//instructions: +69.6M (+0.6%)
🟥 build/module/Lean.Server.FileWorker.SignatureHelp//instructions: +20.8M (+0.6%)
🟥 build/module/Lean.Server.FileWorker.WidgetRequests//instructions: +66.9M (+0.6%)
🟥 build/module/Lean.Server.FileWorker//instructions: +97.8M (+0.6%)
🟥 build/module/Lean.Server.GoTo//instructions: +36.9M (+0.6%)
🟥 build/module/Lean.Server.InfoUtils//instructions: +42.9M (+0.6%)
🟥 build/module/Lean.Server.Logging//instructions: +15.5M (+0.7%)
🟥 build/module/Lean.Server.References//instructions: +64.2M (+0.6%)
🟥 build/module/Lean.Server.Requests//instructions: +60.1M (+0.7%)
🟥 build/module/Lean.Server.Rpc.Deriving//instructions: +59.5M (+0.6%)
🟥 build/module/Lean.Server.Test.Cancel//instructions: +32.8M (+0.6%)
🟥 build/module/Lean.Server.Test.Runner//instructions: +156.1M (+0.7%)
🟥 build/module/Lean.Server.Watchdog//instructions: +207.8M (+0.7%)
🟥 build/module/Lean.Setup//instructions: +34.8M (+0.7%)
🟥 build/module/Lean.Shell//instructions: +46.4M (+0.6%)
🟥 build/module/Lean.Util.Profiler//instructions: +68.6M (+0.7%)
🟥 build/module/Lean.Util.Trace//instructions: +28.8M (+0.6%)
🟥 build/module/Lean.Widget.Commands//instructions: +22.6M (+0.5%)
🟥 build/module/Lean.Widget.Diff//instructions: +31.1M (+0.7%)
🟥 build/module/Lean.Widget.InteractiveCode//instructions: +15.2M (+0.7%)
🟥 build/module/Lean.Widget.InteractiveDiagnostic//instructions: +48.8M (+0.6%)
🟥 build/module/Lean.Widget.InteractiveGoal//instructions: +45.5M (+0.6%)
🟥 build/module/Std.Data.DHashMap.Basic//instructions: +31.2M (+0.6%)
🟥 build/module/Std.Data.DHashMap.Internal.AssocList.Basic//instructions: +20.0M (+0.7%)
🟥 build/module/Std.Data.DHashMap.Internal.Model//instructions: +80.2M (+0.6%)
🟥 build/module/Std.Data.DHashMap.Internal.Raw//instructions: +25.4M (+0.6%)
🟥 build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: +1.9G (+0.7%)
🟥 build/module/Std.Data.DHashMap.Internal.WF//instructions: +139.2M (+0.6%)
🟥 build/module/Std.Data.DHashMap.Lemmas//instructions: +461.2M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.DHashMap.Raw//instructions: +55.9M (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Basic//instructions: +45.6M (+0.7%)
🟥 build/module/Std.Data.DTreeMap.Internal.Operations//instructions: +330.1M (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Internal.Queries//instructions: +141.2M (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Internal.WF.Lemmas//instructions: +291.7M (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Internal.Zipper//instructions: +153.7M (+0.8%)
🟥 build/module/Std.Data.DTreeMap.Lemmas//instructions: +420.3M (+0.6%)
🟥 build/module/Std.Data.DTreeMap.Raw.Basic//instructions: +43.2M (+0.7%)
🟥 build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: +523.4M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.ExtDHashMap.Lemmas//instructions: +415.5M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.ExtDTreeMap.Basic//instructions: +61.0M (+0.7%)
🟥 build/module/Std.Data.ExtDTreeMap.Lemmas//instructions: +405.4M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.ExtHashMap.Lemmas//instructions: +232.6M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.ExtHashSet.Lemmas//instructions: +68.9M (+0.7%)
🟥 build/module/Std.Data.ExtTreeMap.Lemmas//instructions: +280.2M (+0.7%)
🟥 build/module/Std.Data.ExtTreeSet.Lemmas//instructions: +87.3M (+0.7%)
🟥 build/module/Std.Data.HashMap.Lemmas//instructions: +274.4M (+0.6%)
🟥 build/module/Std.Data.HashMap.RawLemmas//instructions: +989.1M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.HashSet.Lemmas//instructions: +84.7M (+0.7%)
🟥 build/module/Std.Data.HashSet.RawLemmas//instructions: +98.2M (+0.8%)
🟥 build/module/Std.Data.Internal.List.Associative//instructions: +736.4M (+0.7%)
🟥 build/module/Std.Data.Iterators.Combinators.Monadic.Zip//instructions: +23.5M (+0.7%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.DropWhile//instructions: +20.8M (+0.6%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile//instructions: +30.9M (+0.6%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: +41.4M (+0.7%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip//instructions: +19.4M (+0.7%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.TakeWhile//instructions: +24.8M (+0.5%)
🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Zip//instructions: +74.1M (+0.6%)
🟥 build/module/Std.Data.Iterators.Lemmas.Equivalence.HetT//instructions: +42.2M (+0.7%)
🟥 build/module/Std.Data.Iterators.Lemmas.Producers.Range//instructions: +17.9M (+0.7%)
🟥 build/module/Std.Data.TreeMap.Lemmas//instructions: +237.4M (+0.6%)
🟥 build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: +357.1M (+0.7%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Data.TreeSet.Lemmas//instructions: +107.2M (+0.8%)
🟥 build/module/Std.Data.TreeSet.Raw.Lemmas//instructions: +145.6M (+0.7%)
🟥 build/module/Std.Do.PostCond//instructions: +73.3M (+0.8%)
🟥 build/module/Std.Do.PredTrans//instructions: +18.9M (+0.6%)
🟥 build/module/Std.Do.SPred.DerivedLaws//instructions: +61.8M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Do.SPred.Laws//instructions: +18.0M (+0.5%)
🟥 build/module/Std.Do.SPred.Notation.Basic//instructions: +17.2M (+0.6%)
🟥 build/module/Std.Do.SPred.Notation//instructions: +152.7M (+0.7%)
🟥 build/module/Std.Do.SPred.SPred//instructions: +22.9M (+0.7%)
🟥 build/module/Std.Do.Triple.SpecLemmas//instructions: +210.3M (+0.6%)
🟥 build/module/Std.Do.WP.Basic//instructions: +17.5M (+0.6%)
🟥 build/module/Std.Do.WP.Monad//instructions: +20.7M (+0.6%)
🟥 build/module/Std.Do.WP.SimpLemmas//instructions: +93.7M (+0.7%)
🟥 build/module/Std.Internal.Async.Basic//instructions: +43.7M (+0.7%)
🟥 build/module/Std.Internal.Async.ContextAsync//instructions: +22.9M (+0.5%)
🟥 build/module/Std.Sat.AIG.Basic//instructions: +87.8M (+0.6%)
🟥 build/module/Std.Sat.AIG.CNF//instructions: +64.8M (+0.5%)
🟥 build/module/Std.Sat.AIG.CachedGatesLemmas//instructions: +29.4M (+0.8%)
🟥 build/module/Std.Sat.AIG.CachedLemmas//instructions: +32.4M (+0.6%)
🟥 build/module/Std.Sat.AIG.If//instructions: +66.5M (+0.5%)
🟥 build/module/Std.Sat.AIG.LawfulOperator//instructions: +22.8M (+0.6%)
🟥 build/module/Std.Sat.AIG.Lemmas//instructions: +27.7M (+0.5%)
🟥 build/module/Std.Sat.AIG.RefVec//instructions: +36.1M (+0.6%)
🟥 build/module/Std.Sat.AIG.RefVecOperator.Map//instructions: +55.1M (+0.6%)
🟥 build/module/Std.Sat.AIG.RefVecOperator.Zip//instructions: +63.5M (+0.6%)
🟥 build/module/Std.Sat.AIG.Relabel//instructions: +33.5M (+0.6%)
🟥 build/module/Std.Sat.AIG.RelabelNat//instructions: +32.1M (+0.6%)
🟥 build/module/Std.Sync.Broadcast//instructions: +52.1M (+0.6%)
🟥 build/module/Std.Sync.Channel//instructions: +60.8M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Basic//instructions: +112.7M (+0.9%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: +459.0M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add//instructions: +49.6M (+0.5%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +176.8M (+0.6%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight//instructions: +85.2M (+0.5%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv//instructions: +58.9M (+0.4%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure//instructions: +93.8M (+0.8%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +739.9M (+0.5%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz//instructions: +48.2M (+0.5%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul//instructions: +36.9M (+0.4%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight//instructions: +145.1M (+0.5%)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: +145.3M (+0.7%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Clause//instructions: +48.9M (+0.7%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas//instructions: +125.7M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult//instructions: +95.9M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound//instructions: +146.8M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: +385.1M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound//instructions: +133.0M (+0.6%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound//instructions: +21.5M (+0.5%)
🟥 build/module/Std.Time.Date.PlainDate//instructions: +18.5M (+0.6%)
🟥 build/module/Std.Time.Date.Unit.Month//instructions: +76.4M (+0.6%)
🟥 build/module/Std.Time.Format.Basic//instructions: +193.2M (+0.6%)
🟥 build/module/Std.Time.Internal.Bounded//instructions: +25.7M (+0.7%)
🟥 build/module/Std.Time.Notation.Spec//instructions: +45.2M (+0.7%)
🟥 build/module/Std.Time.Notation//instructions: +55.8M (+0.6%)
🟥 build/module/Std.Time.Zoned.Database.TzIf//instructions: +30.9M (+0.6%)
🟥 bv_decide_large_aig.lean//instructions: +154.7M (+0.3%)
🟥 bv_decide_mul//instructions: +176.0M (+0.4%)
🟥 bv_decide_rewriter.lean//instructions: +62.1M (+0.4%)
🟥 charactersIn//instructions: +95.1M (+0.2%)
🟥 grind_list2.lean//instructions: +380.7M (+0.6%)
🟥 grind_ring_5.lean//instructions: +23.9M (+0.2%)
🟥 iterators (compiled)//instructions: +904.1k (+0.2%)
🟥 lake build clean//instructions: +11.3G (+0.5%)
🟥 language server startup with ileans//instructions: +71.0M (+0.3%)
🟥 nat_repr//instructions: +36.5M (+1.1%)
🟥 omega_stress.lean async//instructions: +27.2M (+0.5%)
🟥 phashmap.lean//instructions: +54.3M (+0.5%)
🟥 qsort//instructions: +96.3M (+0.6%)
🟥 rbmap_fbip//instructions: +5.8M (+0.1%)
🟥 reduceMatch//instructions: +60.3M (+0.3%)
🟥 simp_bubblesort_256//instructions: +142.9M (+0.9%)
🟥 simp_congr//instructions: +115.5M (+0.7%)
🟥 simp_subexpr//instructions: +129.7M (+0.8%)
🟥 tests/bench/ interpreted//instructions: +703.5M (+0.3%)
🟥 workspaceSymbols//instructions: +73.9M (+0.3%)

leanprover-bot · 2025-12-29T15:09:34Z

Reference manual CI status:

✅ Reference manual branch lean-pr-testing-11830 has successfully built against this PR. (2025-12-29 15:09:32) View Log
🟡 Reference manual branch lean-pr-testing-11830 build against this PR didn't complete normally. (2025-12-29 15:10:30) View Log

leanprover-community-bot · 2025-12-29T16:10:45Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-11830 has successfully built against this PR. (2025-12-29 16:10:43) View Log

perf: test uniqueness non-atomically first in lean_dec_ref_cold

1acde3e

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 29, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 29, 2025

Update lean-toolchain for testing leanprover/lean4#11830

e8cb67f

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Dec 29, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 29, 2025

Update lean-toolchain for testing leanprover/lean4#11830

f581fed

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 29, 2025

Update lean-toolchain for testing leanprover/lean4#11830

7a07ec8

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Dec 29, 2025

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 29, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

perf: test uniqueness non-atomically first in `lean_dec_ref_cold` #11830

perf: test uniqueness non-atomically first in `lean_dec_ref_cold` #11830

Uh oh!

Kha commented Dec 29, 2025

Uh oh!

Kha commented Dec 29, 2025

Uh oh!

leanprover-radar commented Dec 29, 2025 •

edited

Loading

Uh oh!

leanprover-bot commented Dec 29, 2025 •

edited

Loading

Uh oh!

leanprover-community-bot commented Dec 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

perf: test uniqueness non-atomically first in lean_dec_ref_cold #11830

Are you sure you want to change the base?

perf: test uniqueness non-atomically first in lean_dec_ref_cold #11830

Uh oh!

Conversation

Kha commented Dec 29, 2025

Uh oh!

Kha commented Dec 29, 2025

Uh oh!

leanprover-radar commented Dec 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Dec 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot commented Dec 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

perf: test uniqueness non-atomically first in `lean_dec_ref_cold` #11830

perf: test uniqueness non-atomically first in `lean_dec_ref_cold` #11830

leanprover-radar commented Dec 29, 2025 •

edited

Loading

leanprover-bot commented Dec 29, 2025 •

edited

Loading