Skip to content

perf: use absl::flat_hash_map #11743

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
Closed
Kha wants to merge 3 commits into from
Closed

perf: use absl::flat_hash_map #11743

Kha wants to merge 3 commits into from

Conversation

@Kha
Copy link
Member

@Kha Kha commented Dec 19, 2025

No description provided.

@Kha Kha force-pushed the push-lqxlpkxnnxrx branch 5 times, most recently from 7809625 to 930f79d Compare December 19, 2025 23:32
@Kha Kha force-pushed the push-lqxlpkxnnxrx branch from 930f79d to 50b1dd9 Compare December 20, 2025 14:57
@Kha
Copy link
Member Author

Kha commented Dec 22, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Dec 22, 2025 •
edited
Loading

Benchmark results for 50b1dd9 against cec9758 are in! @Kha

Runs (1🟥)
  • 🟥 other exited with code 1
Small changes (116✅)
  • ✅ build/module/Init.Control.Lawful.Instances//instructions: -42.6M (-0.5%)
  • ✅ build/module/Init.Data.Array.Attach//instructions: -78.4M (-0.5%)
  • ✅ build/module/Init.Data.Array.Extract//instructions: -284.3M (-0.5%)
  • ✅ build/module/Init.Data.Array.Find//instructions: -67.7M (-0.5%)
  • ✅ build/module/Init.Data.Array.Lemmas//instructions: -348.3M (-0.5%)
  • ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -72.2M (-0.5%)
  • ✅ build/module/Init.Data.Array.MapIdx//instructions: -55.9M (-0.4%)
  • ✅ build/module/Init.Data.Array.Monadic//instructions: -43.9M (-0.5%)
  • ✅ build/module/Init.Data.Array.QSort.Basic//instructions: -80.6M (-0.4%)
  • ✅ build/module/Init.Data.Array.Zip//instructions: -28.5M (-0.5%)
  • ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -203.3M (-0.4%)
  • ✅ build/module/Init.Data.Int.DivMod.Lemmas//instructions: -247.7M (-0.4%)
  • ✅ build/module/Init.Data.Int.LemmasAux//instructions: -73.3M (-0.5%)
  • ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.FilterMap//instructions: -85.0M (-0.3%)
  • ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.FlatMap//instructions: -32.9M (-0.3%)
  • ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: -191.5M (-0.4%)
  • ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap//instructions: -56.3M (-0.4%)
  • ✅ build/module/Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop//instructions: -75.4M (-0.5%)
  • ✅ build/module/Init.Data.List.Attach//instructions: -49.9M (-0.5%)
  • ✅ build/module/Init.Data.List.Basic//instructions: -64.0M (-0.4%)
  • ✅ build/module/Init.Data.List.Find//instructions: -120.2M (-0.5%)
  • ✅ build/module/Init.Data.List.Lemmas//instructions: -233.5M (-0.4%)
  • ✅ build/module/Init.Data.List.Lex//instructions: -53.4M (-0.4%)
  • ✅ build/module/Init.Data.List.Nat.Modify//instructions: -37.0M (-0.4%)
  • ✅ build/module/Init.Data.List.Nat.TakeDrop//instructions: -75.0M (-0.5%)
  • ✅ build/module/Init.Data.List.Sort.Impl//instructions: -79.2M (-0.4%)
  • ✅ build/module/Init.Data.List.Sort.Lemmas//instructions: -83.2M (-0.4%)
  • ✅ build/module/Init.Data.List.ToArray//instructions: -102.2M (-0.4%)
  • ✅ build/module/Init.Data.List.Zip//instructions: -70.7M (-0.5%)
  • ✅ build/module/Init.Data.Nat.Bitwise.Lemmas//instructions: -53.9M (-0.4%)
  • ✅ build/module/Init.Data.Nat.Lemmas//instructions: -149.8M (-0.5%)
  • ✅ build/module/Init.Data.Option.Lemmas//instructions: -113.1M (-0.5%)
  • ✅ build/module/Init.Data.Option.Monadic//instructions: -23.5M (-0.5%)
  • ✅ build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: -367.8M (-0.6%)
  • ✅ build/module/Init.Data.Range.Polymorphic.NatLemmas//instructions: -233.4M (-0.4%)
  • ✅ build/module/Init.Data.Range.Polymorphic.RangeIterator//instructions: -86.4M (-0.3%)
  • ✅ build/module/Init.Data.SInt.Lemmas//instructions: -240.0M (-0.3%)
  • ✅ build/module/Init.Data.Slice.Array.Lemmas//instructions: -51.4M (-0.4%)
  • ✅ build/module/Init.Data.Slice.List.Lemmas//instructions: -27.2M (-0.5%)
  • ✅ build/module/Init.Data.UInt.Bitwise//instructions: -117.5M (-0.4%)
  • ✅ build/module/Init.Data.Vector.Algebra//instructions: -51.4M (-0.8%)
  • ✅ build/module/Init.Data.Vector.Attach//instructions: -55.2M (-0.6%)
  • ✅ build/module/Init.Data.Vector.Basic//instructions: -51.4M (-0.4%)
  • ✅ build/module/Init.Data.Vector.Extract//instructions: -168.6M (-0.4%)
  • ✅ build/module/Init.Data.Vector.Lemmas//instructions: -296.4M (-0.5%)
  • ✅ build/module/Init.Data.Vector.Lex//instructions: -31.1M (-0.4%)
  • ✅ build/module/Init.Data.Vector.MapIdx//instructions: -47.0M (-0.5%)
  • ✅ build/module/Init.Data.Vector.Monadic//instructions: -32.4M (-0.6%)
  • ✅ build/module/Init.Data.Vector.Perm//instructions: -88.7M (-1.4%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.GetElem//instructions: -21.3M (-0.5%)
  • ✅ build/module/Init.Grind.Order//instructions: -31.1M (-0.7%)
  • ✅ build/module/Init.Notation//instructions: -84.1M (-0.4%)
  • ✅ build/module/Init.NotationExtra//instructions: -45.4M (-0.3%)
  • ✅ build/module/Init.Omega.IntList//instructions: -36.6M (-0.5%)
  • ✅ build/module/Lean.Elab.App//instructions: -109.0M (-0.2%)
  • ✅ build/module/Lean.Elab.Binders//instructions: -59.9M (-0.3%)
  • ✅ build/module/Lean.Elab.BuiltinNotation//instructions: -49.9M (-0.2%)
  • ✅ build/module/Lean.Elab.Do.Basic//instructions: -41.2M (-0.3%)
  • ✅ build/module/Lean.Elab.Do.Legacy//instructions: -177.4M (-0.3%)
  • ✅ build/module/Lean.Elab.DocString.Builtin//instructions: -148.0M (-0.2%)
  • ✅ build/module/Lean.Elab.DocString//instructions: -134.6M (-0.2%)
  • ✅ build/module/Lean.Elab.Match//instructions: -77.4M (-0.2%)
  • ✅ build/module/Lean.Elab.MutualDef//instructions: -79.3M (-0.2%)
  • ✅ build/module/Lean.Elab.MutualInductive//instructions: -106.9M (-0.2%)
  • ✅ build/module/Lean.Elab.PatternVar//instructions: -46.2M (-0.3%)
  • ✅ build/module/Lean.Elab.Quotation//instructions: -85.5M (-0.3%)
  • ✅ build/module/Lean.Elab.Structure//instructions: -122.7M (-0.2%)
  • ✅ build/module/Lean.Elab.Tactic.Basic//instructions: -63.4M (-0.4%)
  • ✅ build/module/Lean.Elab.Tactic.Grind.Basic//instructions: -37.7M (-0.3%)
  • ✅ build/module/Lean.Elab.Tactic.Grind.Main//instructions: -42.5M (-0.3%)
  • ✅ build/module/Lean.Elab.Tactic.Try//instructions: -116.0M (-0.3%)
  • ✅ build/module/Lean.Elab.Term.TermElabM//instructions: -93.0M (-0.3%)
  • ✅ build/module/Lean.Meta.Injective//instructions: -38.5M (-0.2%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr//instructions: -61.9M (-0.2%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: -68.1M (-0.2%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.MatchCond//instructions: -46.0M (-0.2%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Types//instructions: -121.8M (-0.3%)
  • ✅ build/module/Lean.Meta.Tactic.Simp.Main//instructions: -70.2M (-0.2%)
  • ✅ build/module/Lean.Meta.Tactic.Simp.Simproc//instructions: -27.9M (-0.2%)
  • ✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -158.1M (-0.3%)
  • ✅ build/module/Std.Data.DHashMap.Internal.WF//instructions: -90.1M (-0.4%)
  • ✅ build/module/Std.Data.DHashMap.Lemmas//instructions: -295.5M (-0.4%)
  • ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -644.7M (-0.4%)
  • ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -958.9M (-0.4%)
  • ✅ build/module/Std.Data.DTreeMap.Lemmas//instructions: -247.8M (-0.4%)
  • ✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -377.3M (-0.4%)
  • ✅ build/module/Std.Data.ExtDHashMap.Lemmas//instructions: -297.9M (-0.4%)
  • ✅ build/module/Std.Data.ExtDTreeMap.Lemmas//instructions: -273.5M (-0.4%)
  • ✅ build/module/Std.Data.ExtHashMap.Lemmas//instructions: -138.8M (-0.4%)
  • ✅ build/module/Std.Data.ExtHashSet.Lemmas//instructions: -45.9M (-0.5%)
  • ✅ build/module/Std.Data.ExtTreeMap.Lemmas//instructions: -131.6M (-0.3%)
  • ✅ build/module/Std.Data.HashMap.Lemmas//instructions: -166.6M (-0.4%)
  • ✅ build/module/Std.Data.Internal.List.Associative//instructions: -441.8M (-0.4%)
  • ✅ build/module/Std.Data.Iterators.Lemmas.Equivalence.HetT//instructions: -24.0M (-0.4%)
  • ✅ build/module/Std.Data.Iterators.Lemmas.Producers.Range//instructions: -18.6M (-0.6%)
  • ✅ build/module/Std.Data.TreeMap.Lemmas//instructions: -119.9M (-0.3%)
  • ✅ build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: -230.4M (-0.4%)
  • ✅ build/module/Std.Data.TreeSet.Raw.Lemmas//instructions: -99.4M (-0.5%)
  • ✅ build/module/Std.Do.PostCond//instructions: -41.0M (-0.4%)
  • ✅ build/module/Std.Do.PredTrans//instructions: -17.7M (-0.5%)
  • ✅ build/module/Std.Do.SPred.DerivedLaws//instructions: -55.6M (-0.6%)
  • ✅ build/module/Std.Do.SPred.Laws//instructions: -19.4M (-0.5%)
  • ✅ build/module/Std.Do.SPred.SPred//instructions: -16.8M (-0.5%)
  • ✅ build/module/Std.Do.Triple.SpecLemmas//instructions: -132.7M (-0.6%)
  • ✅ build/module/Std.Do.WP.Monad//instructions: -19.4M (-0.5%)
  • ✅ build/module/Std.Do.WP.SimpLemmas//instructions: -78.7M (-0.6%)
  • ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -215.9M (-0.3%)
  • ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: -100.1M (-0.3%)
  • ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz//instructions: -30.0M (-0.3%)
  • ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight//instructions: -94.0M (-0.4%)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas//instructions: -227.0M (-1.1%)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult//instructions: -62.0M (-0.4%)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound//instructions: -86.3M (-0.3%)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: -410.2M (-0.7%) (reduced significance based on absolute threshold)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound//instructions: -75.0M (-0.3%)
  • ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound//instructions: -20.9M (-0.5%)

@Kha
Copy link
Member Author

Kha commented Jan 14, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 14, 2026 •
edited
Loading

Benchmark results for 1cb9a2f against 8435dea are in! @Kha

Runs (1🟥)
  • 🟥 other exited with code 1
Small changes (1✅)
  • ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -226.5M (-0.1%)

@Kha
Copy link
Member Author

Kha commented Jan 14, 2026

Appears to be wholly subsumed by #11957

@Kha Kha closed this Jan 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

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