Skip to content

perf: don't enqueue last object in the deletion list - #15004

Draft
TwoFX wants to merge 3 commits into
leanprover:masterfrom
TwoFX:julia/free
Draft

perf: don't enqueue last object in the deletion list#15004
TwoFX wants to merge 3 commits into
leanprover:masterfrom
TwoFX:julia/free

Conversation

@TwoFX

@TwoFX TwoFX commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR slightly optimizes the freeing logic in the runtime.

When deleting an object, instead of looping over all children and adding them to the deletion list if they are also no longer needed, we loop over all children except for the last one. Afterwards, if the last child also needs to be deleted, we immediately continue with that child. This saves us from having to add that child to the deletion list.

@TwoFX

TwoFX commented Sep 3, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 17a2c74 against 138ca9f are in. There are significant results. @TwoFX

  • 🟥 build exited with code -1
  • 🟥 other exited with code 1

No significant changes detected.

@TwoFX

TwoFX commented Sep 3, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 0a39fc4 against 138ca9f are in. There are significant results. @TwoFX

  • 🟥 build//instructions: +66.2G (+0.58%)

Large changes (7✅, 5🟥)

  • ✅ compiled/binarytrees.st//instructions: -1.3G (-2.46%)
  • ✅ compiled/binarytrees//instructions: -1.3G (-2.46%)
  • ✅ compiled/deriv//instructions: -117.2M (-1.79%)
  • 🟥 compiled/hashmap//instructions: +36.4M (+1.13%)
  • ✅ compiled/ilean_roundtrip//instructions: -54.6M (-0.25%)
  • 🟥 compiled/io_compute//instructions: +68.8M (+0.62%)
  • ✅ compiled/nat_repr//instructions: -774.9M (-2.29%)
  • ✅ compiled/phashmap//instructions: -83.6M (-0.96%)
  • 🟥 compiled/qsort//instructions: +158.2M (+1.04%)
  • ✅ compiled/treemap//instructions: -41.0M (-0.24%)
  • 🟥 compiled/unionfind//instructions: +412.6M (+1.93%)
  • 🟥 elab/simp_local//instructions: +1.6G (+5.21%)

Medium changes (5✅, 9🟥)

  • 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.7G (+1.14%)
  • 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +2.1G (+0.96%)
  • ✅ compiled/liasolver//instructions: -12.2M (-0.36%)
  • ✅ compiled/parser//instructions: -174.9M (-0.49%)
  • ✅ compiled/rbmap_checkpoint2//instructions: -13.1M (-0.15%)
  • ✅ compiled/rbmap_library//instructions: -9.7M (-0.10%)
  • ✅ elab/big_do//instructions: -83.4M (-0.46%)
  • 🟥 elab/big_struct_dep//instructions: +219.3M (+1.61%)
  • 🟥 elab/cbv_arm_ldst//instructions: +664.2M (+1.23%)
  • 🟥 elab/cbv_leroy//instructions: +736.4M (+1.61%)
  • 🟥 elab/cbv_system_f//instructions: +1.2G (+1.27%)
  • 🟥 elab/charactersIn//instructions: +172.1M (+0.56%)
  • 🟥 elab/simp_bubblesort_256//instructions: +318.3M (+3.27%)
  • 🟥 elab/simp_subexpr//instructions: +321.5M (+3.19%)

Small changes (7✅, 422🟥)

  • 🟥 build/module/Init.Control.Basic//instructions: +14.9M (+0.69%)
  • 🟥 build/module/Init.Control.Except//instructions: +13.7M (+0.97%)
  • 🟥 build/module/Init.Control.Lawful.Basic//instructions: +19.4M (+0.92%)
  • 🟥 build/module/Init.Control.Lawful.Instances//instructions: +49.2M (+0.74%)
  • 🟥 build/module/Init.Control.StateCps//instructions: +11.0M (+1.08%)
  • 🟥 build/module/Init.Conv//instructions: +27.5M (+0.74%)
  • 🟥 build/module/Init.Core//instructions: +104.9M (+1.07%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.AC//instructions: +60.3M (+1.58%)
  • 🟥 build/module/Init.Data.Array.Attach//instructions: +56.7M (+0.56%)
  • 🟥 build/module/Init.Data.Array.Basic//instructions: +96.6M (+0.90%)
  • 🟥 build/module/Init.Data.Array.BinSearch//instructions: +27.0M (+0.46%)
  • 🟥 build/module/Init.Data.Array.Erase//instructions: +45.9M (+0.65%)
  • 🟥 build/module/Init.Data.Array.Find//instructions: +63.7M (+0.66%)
  • 🟥 build/module/Init.Data.Array.Lemmas//instructions: +367.1M (+0.70%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.Lex.Lemmas//instructions: +70.9M (+0.75%)
  • 🟥 build/module/Init.Data.Array.MapIdx//instructions: +49.8M (+0.58%)
  • 🟥 build/module/Init.Data.Array.Monadic//instructions: +35.3M (+0.59%)
  • 🟥 build/module/Init.Data.Array.Range//instructions: +27.1M (+0.68%)
  • 🟥 build/module/Init.Data.Array.Subarray//instructions: +18.1M (+1.00%)
  • 🟥 build/module/Init.Data.Array.Zip//instructions: +31.5M (+0.69%)
  • and 409 more

@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Sep 3, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 3, 2026
@leanprover-bot

leanprover-bot commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 3, 2026
@mathlib-lean-pr-testing

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

Copy link
Copy Markdown

Mathlib CI status (docs):

@TwoFX

TwoFX commented Sep 3, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 27f2f40 against 138ca9f are in. There are significant results. @TwoFX

  • ✅ build//instructions: -61.9G (-0.54%)

Large changes (12✅)

  • ✅ compiled/binarytrees.st//instructions: -2.0G (-3.59%)
  • ✅ compiled/binarytrees//instructions: -2.0G (-3.60%)
  • ✅ compiled/deriv//instructions: -173.0M (-2.64%)
  • ✅ compiled/hashmap//instructions: -40.7M (-1.26%)
  • ✅ compiled/ilean_roundtrip//instructions: -92.3M (-0.42%)
  • ✅ compiled/io_compute//instructions: -56.6M (-0.51%)
  • ✅ compiled/parser//instructions: -324.2M (-0.91%)
  • ✅ compiled/phashmap//instructions: -149.7M (-1.71%)
  • ✅ compiled/qsort//instructions: -31.3M (-0.21%)
  • ✅ compiled/rbmap_checkpoint2//instructions: -23.7M (-0.28%)
  • ✅ compiled/treemap//instructions: -142.2M (-0.83%)
  • ✅ compiled/unionfind//instructions: -290.1M (-1.36%)

Medium changes (5✅)

  • ✅ compiled/rbmap_library//instructions: -15.7M (-0.17%)
  • ✅ elab/big_do//instructions: -141.2M (-0.77%)
  • ✅ elab/big_struct_dep//instructions: -203.8M (-1.50%)
  • ✅ elab/whnfMatcherImplicitTransparencyCaching//instructions: -123.5M (-0.51%)
  • ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.3G (-1.07%)

Small changes (418✅)

  • ✅ build/module/Init.Control.Basic//instructions: -14.0M (-0.65%)
  • ✅ build/module/Init.Control.Lawful.Instances//instructions: -41.9M (-0.63%)
  • ✅ build/module/Init.Conv//instructions: -24.8M (-0.67%)
  • ✅ build/module/Init.Core//instructions: -66.2M (-0.67%)
  • ✅ build/module/Init.Data.Array.Attach//instructions: -63.4M (-0.62%)
  • ✅ build/module/Init.Data.Array.Basic//instructions: -66.8M (-0.62%)
  • ✅ build/module/Init.Data.Array.BinSearch//instructions: -27.9M (-0.48%)
  • ✅ build/module/Init.Data.Array.Erase//instructions: -32.8M (-0.47%)
  • ✅ build/module/Init.Data.Array.Extract//instructions: -155.2M (-0.46%)
  • ✅ build/module/Init.Data.Array.Find//instructions: -54.5M (-0.57%)
  • ✅ build/module/Init.Data.Array.Lemmas//instructions: -316.7M (-0.61%)
  • ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -56.3M (-0.60%)
  • ✅ build/module/Init.Data.Array.MapIdx//instructions: -49.8M (-0.57%)
  • ✅ build/module/Init.Data.Array.Monadic//instructions: -40.2M (-0.67%)
  • ✅ build/module/Init.Data.Array.QSort.Basic//instructions: -58.0M (-0.58%)
  • ✅ build/module/Init.Data.Array.Range//instructions: -22.8M (-0.57%)
  • ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -266.0M (-0.54%)
  • ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -568.1M (-0.49%)
  • ✅ build/module/Init.Data.ByteArray.Lemmas//instructions: -25.9M (-0.48%)
  • ✅ build/module/Init.Data.Char.Ordinal//instructions: -27.1M (-0.47%)
  • and 398 more

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#15004
c6b20c5
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#15004
cc1cc23
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#15004
b471ea6
@TwoFX

TwoFX commented Sep 3, 2026

Copy link
Copy Markdown
Member Author

!bench mathlib

@leanprover-radar

leanprover-radar commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@cc1cc23 against leanprover-community/mathlib4-nightly-testing@aee6a83 are in. There are significant results. @TwoFX

  • ✅ build//instructions: -439.8G (-0.31%)

Large changes (1✅)

  • 1 hidden

Small changes (17✅, 31🟥)

  • 🟥 build/module/Aesop.BaseM//instructions: +24.5M (+1.53%)
  • 🟥 build/module/Aesop.Builder.Constructors//instructions: +28.9M (+1.79%)
  • ✅ build/module/Aesop.Builder.Forward//instructions: -32.6M (-0.63%)
  • 🟥 build/module/Aesop.BuiltinRules.Subst//instructions: +26.9M (+1.01%)
  • 🟥 build/module/Aesop.ElabM//instructions: +21.7M (+1.50%)
  • ✅ build/module/Aesop.RuleSet//instructions: -82.1M (-0.70%)
  • ✅ build/module/Aesop.RuleTac.Forward//instructions: -37.5M (-0.61%)
  • 🟥 build/module/Aesop.RuleTac.Tactic//instructions: +46.2M (+1.78%)
  • ✅ build/module/Aesop.Saturate//instructions: -109.8M (-0.79%)
  • 🟥 build/module/Aesop.Script.CtorNames//instructions: +36.7M (+1.51%)
  • ✅ build/module/Aesop.Search.Expansion.Norm//instructions: -83.0M (-0.68%)
  • ✅ build/module/Aesop.Search.Expansion//instructions: -48.2M (-0.62%)
  • 🟥 build/module/Aesop.Stats.File//instructions: +26.7M (+1.64%)
  • ✅ build/module/Aesop.Tree.Tracing//instructions: -29.4M (-0.59%)
  • ✅ build/module/Aesop.Util.Basic//instructions: -48.5M (-0.62%)
  • 🟥 build/module/Aesop//instructions: +27.2M (+1.79%)
  • ✅ build/module/Batteries.CodeAction.Misc//instructions: -59.2M (-0.76%)
  • 🟥 build/module/Batteries.Control.Nondet.Basic//instructions: +24.3M (+1.24%)
  • 🟥 build/module/Batteries.Control.OptionT//instructions: +17.6M (+1.13%)
  • 🟥 build/module/Batteries.Data.FloatArray//instructions: +20.6M (+1.93%)
  • and 28 more

@TwoFX TwoFX mentioned this pull request Sep 3, 2026
Merged
@TwoFX

TwoFX commented Sep 3, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Sep 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for cc59af7 against 138ca9f are in. There are significant results. @TwoFX

  • ✅ build//instructions: -65.4G (-0.58%)

Large changes (10✅, 1🟥)

  • ✅ compiled/binarytrees.st//instructions: -2.3G (-4.16%)
  • ✅ compiled/binarytrees//instructions: -2.3G (-4.16%)
  • ✅ compiled/deriv//instructions: -185.2M (-2.82%)
  • 🟥 compiled/hashmap//instructions: +20.3M (+0.63%)
  • ✅ compiled/ilean_roundtrip//instructions: -106.2M (-0.48%)
  • ✅ compiled/parser//instructions: -370.5M (-1.03%)
  • ✅ compiled/phashmap//instructions: -84.2M (-0.96%)
  • ✅ compiled/qsort//instructions: -63.5M (-0.42%)
  • ✅ compiled/rbmap_checkpoint2//instructions: -31.5M (-0.37%)
  • ✅ compiled/treemap//instructions: -93.0M (-0.54%)
  • ✅ compiled/unionfind//instructions: -296.2M (-1.38%)

Medium changes (5✅, 1🟥)

  • 🟥 compiled/io_compute//instructions: +37.1M (+0.34%)
  • ✅ compiled/rbmap_library//instructions: -17.5M (-0.19%)
  • ✅ elab/big_do//instructions: -155.7M (-0.85%)
  • ✅ elab/big_struct_dep//instructions: -222.8M (-1.63%)
  • ✅ elab/whnfMatcherImplicitTransparencyCaching//instructions: -146.5M (-0.60%)
  • ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.5G (-1.20%)

Small changes (460✅, 2🟥)

  • ✅ build/module/Init.Control.Basic//instructions: -14.4M (-0.67%)
  • ✅ build/module/Init.Control.Lawful.Instances//instructions: -46.5M (-0.70%)
  • ✅ build/module/Init.Conv//instructions: -29.1M (-0.78%)
  • ✅ build/module/Init.Core//instructions: -69.2M (-0.70%)
  • ✅ build/module/Init.Data.Array.Attach//instructions: -64.5M (-0.64%)
  • ✅ build/module/Init.Data.Array.Basic//instructions: -70.5M (-0.66%)
  • ✅ build/module/Init.Data.Array.BinSearch//instructions: -31.8M (-0.54%)
  • ✅ build/module/Init.Data.Array.Erase//instructions: -36.5M (-0.52%)
  • ✅ build/module/Init.Data.Array.Extract//instructions: -189.0M (-0.56%)
  • ✅ build/module/Init.Data.Array.Find//instructions: -57.7M (-0.60%)
  • ✅ build/module/Init.Data.Array.Lemmas//instructions: -327.2M (-0.63%)
  • ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -62.4M (-0.66%)
  • ✅ build/module/Init.Data.Array.MapIdx//instructions: -50.2M (-0.58%)
  • ✅ build/module/Init.Data.Array.Monadic//instructions: -40.0M (-0.67%)
  • ✅ build/module/Init.Data.Array.QSort.Basic//instructions: -56.4M (-0.57%)
  • ✅ build/module/Init.Data.Array.Range//instructions: -22.6M (-0.57%)
  • ✅ build/module/Init.Data.Array.Sort.Lemmas//instructions: -18.1M (-0.57%)
  • ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -293.0M (-0.59%)
  • ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -663.3M (-0.58%)
  • ✅ build/module/Init.Data.ByteArray.Lemmas//instructions: -29.9M (-0.55%)
  • and 442 more

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#15004
ff29257
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 3, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#15004
eff8e47
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 3, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#15004
97c2df1
meerkatone pushed a commit to meerkatone/lean4 that referenced this pull request Sep 3, 2026
@TwoFX
chore: remove LEAN_LAZY_RC (leanprover#15006)
137a88d 
This PR removes the long-obsolete `LEAN_LAZY_RC` option.

This will make leanprover#15004 slightly easier to land, if we decide to land that
one.
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

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 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.

3 participants

@TwoFX @leanprover-radar @leanprover-bot