Skip to content

feat: linearity marker for HashMaps - #15049

Merged
hargoniX merged 2 commits into
masterfrom
hbv/marklinear
Sep 9, 2026
Merged

feat: linearity marker for HashMaps#15049
hargoniX merged 2 commits into
masterfrom
hbv/marklinear

Conversation

@hargoniX

@hargoniX hargoniX commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR introduces markLinear functions for hash maps, akin to Array.markLinear

@hargoniX

hargoniX commented Sep 7, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 05399bb against c8e19cc are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +10.1G (+0.09%)

Large changes (1✅, 6🟥)

  • ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//task-clock: -15s (-11.90%)
  • 🟥 size/Init/.olean//bytes: +653kiB (+0.67%)
  • 🟥 size/all/.ir//bytes: +10MiB (+2.85%)
  • 🟥 size/all/.olean.private//bytes: +21MiB (+1.61%)
  • 🟥 size/all/.olean//bytes: +3MiB (+0.87%)
  • 🟥 size/compile/.out//bytes: +20MiB (+0.70%)
  • 🟥 size/install//bytes: +35MiB (+1.09%)

Medium changes (2✅, 5🟥)

  • 🟥 build/stat/imported bytes//bytes: +2GiB (+1.19%)
  • 🟥 compiled/parser//maxrss: +6MiB (+8.11%)
  • 🟥 compiled/phashmap//instructions: +18.9M (+0.22%)
  • 🟥 elab/big_beq_rec//maxrss: +19MiB (+1.09%)
  • ✅ elab/bv_decide_large_aig//maxrss: -34MiB (-2.54%)
  • ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//wall-clock: -469ms (-8.52%)
  • 🟥 size/Init/.olean.server//bytes: +52kiB (+0.46%)

Small changes (1✅, 39🟥)

  • 🟥 build/module/Init.Data.Array.Basic//instructions: +40.8M (+0.38%)
  • 🟥 build/module/Lean.Compiler.LCNF.CSE//instructions: +63.4M (+2.63%)
  • 🟥 build/module/Lean.Compiler.LCNF.ExtractClosed//instructions: +234.2M (+5.12%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Data.DHashMap.Basic//instructions: +42.5M (+1.15%)
  • 🟥 build/module/Std.Data.DHashMap.Raw//instructions: +46.6M (+0.69%)
  • 🟥 build/module/Std.Data.HashMap.Basic//instructions: +33.0M (+1.38%)
  • 🟥 build/module/Std.Data.HashMap.Raw//instructions: +45.8M (+1.82%) (reduced significance based on *//lines)
  • 🟥 compiled/ilean_roundtrip//instructions: +13.5M (+0.06%)
  • 🟥 compiled/incr_header_save//maxrss: +12MiB (+0.59%)
  • 🟥 elab/big_beq//maxrss: +15MiB (+0.87%)
  • 🟥 elab/big_deceq//maxrss: +15MiB (+0.87%)
  • 🟥 elab/big_deceq_rec//maxrss: +16MiB (+0.88%)
  • 🟥 elab/big_match//maxrss: +13MiB (+0.75%)
  • 🟥 elab/big_match_nat//maxrss: +16MiB (+0.88%)
  • 🟥 elab/big_match_nat_split//maxrss: +17MiB (+0.96%)
  • 🟥 elab/big_match_partial//maxrss: +14MiB (+0.77%)
  • 🟥 elab/bv_decide_incremental//maxrss: +23MiB (+1.13%)
  • 🟥 elab/bv_decide_mul//instructions: +49.6M (+0.15%)
  • 🟥 elab/cbv_merge_sort//maxrss: +20MiB (+1.08%)
  • 🟥 elab/delayed_assign//maxrss: +17MiB (+0.95%)
  • and 20 more

@github-actions github-actions Bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Sep 7, 2026
@hargoniX

hargoniX commented Sep 7, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 9032001 against 64906da are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +17.7G (+0.16%)

Large changes (4🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +56.8M (+0.26%)
  • 🟥 compiled/phashmap//instructions: +61.3M (+0.70%)
  • 🟥 compiled/qsort//instructions: +46.6M (+0.31%)
  • 🟥 size/compile/.out//bytes: +18MiB (+0.67%)

Small changes (12🟥)

  • 🟥 build/module/Init.Data.Array.Basic//instructions: +50.2M (+0.48%)
  • 🟥 build/module/Lean.Compiler.LCNF.CSE//instructions: +61.9M (+2.66%)
  • 🟥 build/module/Lean.Compiler.LCNF.ExtractClosed//instructions: +235.0M (+5.30%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Data.DHashMap.Basic//instructions: +42.5M (+1.18%)
  • 🟥 build/module/Std.Data.DHashMap.Raw//instructions: +48.9M (+0.74%)
  • 🟥 build/module/Std.Data.HashMap.Basic//instructions: +36.5M (+1.58%)
  • 🟥 build/module/Std.Data.HashMap.Raw//instructions: +43.8M (+1.79%) (reduced significance based on *//lines)
  • 🟥 compiled/io_compute//instructions: +12.5M (+0.11%)
  • 🟥 compiled/parser//instructions: +35.4M (+0.10%)
  • 🟥 compiled/unionfind//instructions: +3.0M (+0.01%)
  • 🟥 elab/big_do//instructions: +44.0M (+0.25%)
  • 🟥 elab/bv_decide_mul//instructions: +58.3M (+0.18%)

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 7, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 64906da38cdd68f83829f45f6fafe35468f06f7b --onto c155094f54eab345cca3da867dbd888a34fbf0d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-07 12:27:33)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 235b7598586a37909478143129fed0af93049a24 --onto c155094f54eab345cca3da867dbd888a34fbf0d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-08 15:47:18)
  • ✅ Mathlib branch lean-pr-testing-15049 has successfully built against this PR. (2026-09-08 16:21:34) View Log

@leanprover-bot

leanprover-bot commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 64906da38cdd68f83829f45f6fafe35468f06f7b --onto 9de86005af5061b5ccf438d01134ee6d3ecea6b3. You can force reference manual CI using the force-manual-ci label. (2026-09-07 12:27:34)
  • ✅ Reference manual branch lean-pr-testing-15049 has successfully built against this PR. (2026-09-08 15:29:47) View Log
  • 🟡 Reference manual branch lean-pr-testing-15049 build against this PR didn't complete normally. (2026-09-08 15:31:36) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 235b7598586a37909478143129fed0af93049a24 --onto c155094f54eab345cca3da867dbd888a34fbf0d2. You can force reference manual CI using the force-manual-ci label. (2026-09-08 15:47:20)

@hargoniX

hargoniX commented Sep 7, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for ecb0237 against 64906da are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +14.3G (+0.13%)

Large changes (4🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +56.7M (+0.26%)
  • 🟥 compiled/phashmap//instructions: +61.3M (+0.70%)
  • 🟥 compiled/qsort//instructions: +46.6M (+0.31%)
  • 🟥 size/compile/.out//bytes: +19MiB (+0.68%)

Medium changes (1🟥)

  • 🟥 compiled/hashmap//instructions: +7.2M (+0.22%)

Small changes (10🟥)

  • 🟥 build/module/Init.Data.Array.Basic//instructions: +47.1M (+0.45%)
  • 🟥 build/module/Std.Data.DHashMap.Basic//instructions: +41.4M (+1.15%)
  • 🟥 build/module/Std.Data.DHashMap.Raw//instructions: +47.1M (+0.71%)
  • 🟥 build/module/Std.Data.HashMap.Basic//instructions: +35.8M (+1.55%)
  • 🟥 build/module/Std.Data.HashMap.Raw//instructions: +42.6M (+1.75%) (reduced significance based on *//lines)
  • 🟥 compiled/io_compute//instructions: +12.5M (+0.11%)
  • 🟥 compiled/parser//instructions: +29.3M (+0.08%)
  • 🟥 compiled/unionfind//instructions: +3.0M (+0.01%)
  • 🟥 elab/big_do//instructions: +43.4M (+0.25%)
  • 🟥 elab/bv_decide_mul//instructions: +70.5M (+0.22%)

@hargoniX
hargoniX force-pushed the hbv/marklinear branch 2 times, most recently from bde8ea4 to bda8eee Compare September 7, 2026 15:24
@hargoniX

hargoniX commented Sep 7, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Sep 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for bda8eee against 64906da are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +20.8G (+0.19%)

Large changes (6🟥)

  • 🟥 compiled/ilean_roundtrip//instructions: +62.6M (+0.29%)
  • 🟥 compiled/io_compute//instructions: +362.5M (+3.31%)
  • 🟥 compiled/nat_repr//instructions: +110.6M (+0.33%)
  • 🟥 compiled/phashmap//instructions: +85.5M (+0.98%)
  • 🟥 compiled/qsort//instructions: +47.7M (+0.31%)
  • 🟥 size/compile/.out//bytes: +48MiB (+1.76%)

Medium changes (3🟥)

  • 🟥 compiled/hashmap//instructions: +7.2M (+0.22%)
  • 🟥 compiled/parser//instructions: +97.6M (+0.27%)
  • 🟥 elab/bv_decide_mul//instructions: +148.1M (+0.46%)

Small changes (14🟥)

  • 🟥 build/module/Init.Data.Array.Basic//instructions: +53.3M (+0.51%)
  • 🟥 build/module/Init.Data.ByteArray.Basic//instructions: +44.5M (+1.74%)
  • 🟥 build/module/Init.Data.FloatArray.Basic//instructions: +24.5M (+1.88%)
  • 🟥 build/module/Init.Data.String.Defs//instructions: +29.4M (+1.14%)
  • 🟥 build/module/Lean.Elab.Deriving//instructions: +20.7M (+2.60%)
  • 🟥 build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: +18.7M (+0.38%)
  • 🟥 build/module/Std.Data.DHashMap.Basic//instructions: +46.1M (+1.29%)
  • 🟥 build/module/Std.Data.DHashMap.Raw//instructions: +52.1M (+0.78%)
  • 🟥 build/module/Std.Data.HashMap.Basic//instructions: +38.6M (+1.67%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Data.HashMap.Raw//instructions: +46.6M (+1.91%) (reduced significance based on *//lines)
  • 🟥 compiled/select//instructions: +10.4M (+0.39%)
  • 🟥 compiled/unionfind//instructions: +3.0M (+0.01%)
  • 🟥 elab/big_do//instructions: +62.8M (+0.35%)
  • 🟥 elab/bv_decide_large_aig//maxrss: +26MiB (+1.90%)

@hargoniX hargoniX changed the title feat: markLinear feat: linearity marker for HashMaps Sep 8, 2026
@github-actions github-actions Bot added mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN and removed changes-stage0 Contains stage0 changes, merge manually using rebase labels Sep 8, 2026
@hargoniX

hargoniX commented Sep 8, 2026

Copy link
Copy Markdown
Member Author

!bench

@hargoniX
hargoniX marked this pull request as ready for review September 8, 2026 15:24
@hargoniX
hargoniX requested a review from TwoFX as a code owner September 8, 2026 15:24
@leanprover-radar

leanprover-radar commented Sep 8, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 810801c against 235b759 are in. No significant results found. @hargoniX

  • ✅ build//instructions: -26.2M (-0.00%)

Small changes (1✅, 6🟥)

  • 🟥 build/module/Std.Data.DHashMap.Basic//instructions: +38.9M (+1.08%)
  • 🟥 build/module/Std.Data.DHashMap.Raw//instructions: +49.0M (+0.74%)
  • 🟥 build/module/Std.Data.HashMap.Basic//instructions: +33.4M (+1.44%)
  • 🟥 build/module/Std.Data.HashMap.Raw//instructions: +41.3M (+1.69%) (reduced significance based on *//lines)
  • 🟥 lake/inundation/config/elab//instructions: +29.1M (+1.14%)
  • 🟥 size/compile/.out//bytes: +10MiB (+0.37%)
  • ✅ vcgen/GetThrowSetGrind/200/kernel//wall-clock: -11ms (-8.65%)

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 8, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 8, 2026
@hargoniX hargoniX added the changelog-library Library label Sep 9, 2026
@hargoniX
hargoniX added this pull request to the merge queue Sep 9, 2026
Merged via the queue into master with commit eea0213 Sep 9, 2026
50 of 54 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@hargoniX @leanprover-radar @leanprover-bot @TwoFX