Skip to content

feat: add cbv annotations to HashMap/HashSet operations - #14707

Merged
wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wkr/cbv_annotations_ofList
Aug 7, 2026
Merged

feat: add cbv annotations to HashMap/HashSet operations#14707
wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wkr/cbv_annotations_ofList

Conversation

@wkrozowski

@wkrozowski wkrozowski commented Aug 6, 2026

Copy link
Copy Markdown
Contributor

This PR adds missing cbv_eval annotations to ofList/ofArray, get!, getD, insert operations on HashMap/HashSet.

@wkrozowski
wkrozowski requested a review from TwoFX as a code owner August 6, 2026 17:13
@wkrozowski wkrozowski changed the title feat: add cbv annotations to ofList/ofArray for HashMap/HashSet feat: add cbv annotations to HashMap/HashSet operations Aug 6, 2026
@wkrozowski
wkrozowski added this pull request to the merge queue Aug 7, 2026
Merged via the queue into leanprover:master with commit 0dfa5c0 Aug 7, 2026
24 of 30 checks passed
@Kha

Kha commented Aug 7, 2026

Copy link
Copy Markdown
Member

!bench

@leanprover-radar

leanprover-radar commented Aug 7, 2026

Copy link
Copy Markdown

Benchmark results for 11ce9b4 against 4a37393 are in. There are significant results. @Kha

  • 🟥 build//instructions: +5.7G (+0.05%)

Small changes (34🟥)

  • 🟥 build/module/Lake.DSL.DeclUtil//instructions: +100.1M (+3.24%)
  • 🟥 build/module/Lean.Compiler.LCNF.SimpCase//instructions: +27.9M (+1.59%)
  • 🟥 build/module/Lean.Elab.AssertExists//instructions: +153.5M (+6.05%)
  • 🟥 build/module/Lean.Elab.AuxDef//instructions: +134.1M (+8.90%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.CheckTactic//instructions: +115.6M (+5.10%)
  • 🟥 build/module/Lean.Elab.Command.WithWeakNamespace//instructions: +126.5M (+11.80%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.GenInjective//instructions: +124.8M (+13.18%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.InfoTrees//instructions: +145.4M (+11.58%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.Print//instructions: +97.5M (+1.63%)
  • 🟥 build/module/Lean.Elab.RecommendedSpelling//instructions: +95.9M (+5.98%)
  • 🟥 build/module/Lean.Elab.Tactic.CbvSimproc//instructions: +80.5M (+4.89%)
  • 🟥 build/module/Lean.Elab.Tactic.DiscrTreeKey//instructions: +139.6M (+7.92%)
  • 🟥 build/module/Lean.Elab.Tactic.Doc//instructions: +84.3M (+2.13%)
  • 🟥 build/module/Lean.Elab.Tactic.Grind.Annotated//instructions: +138.6M (+11.48%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.Tactic.Simproc//instructions: +136.2M (+8.16%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Elab.Time//instructions: +123.1M (+11.50%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Linter.Basic//instructions: +105.7M (+7.83%)
  • 🟥 build/module/Lean.Linter.Builtin//instructions: +137.4M (+6.90%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Linter.CodeQuality.Frontend//instructions: +111.3M (+5.98%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Lean.Linter.Coe//instructions: +125.7M (+7.58%) (reduced significance based on absolute threshold)
  • and 14 more

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

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants