perf: outline heartbeat inc

[hargoniX]

No description provided.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 79e9fb1 against 548f78b are in. There are significant results. @hargoniX

• 🟥 build//instructions: +89.8G (+0.80%)

Large changes (7✅, 12🟥)

• ✅ compiled/binarytrees.st//instructions: -320.5M (-0.57%)
• ✅ compiled/binarytrees//instructions: -321.4M (-0.57%)
• 🟥 compiled/deriv//instructions: +127.5M (+1.89%)
• 🟥 compiled/hashmap//instructions: +159.0M (+4.75%)
• 🟥 compiled/ilean_roundtrip//instructions: +155.2M (+0.69%)
• 🟥 compiled/io_compute//instructions: +168.2M (+1.50%)
• 🟥 compiled/parser//instructions: +276.7M (+0.80%)
• 🟥 compiled/phashmap//instructions: +187.3M (+2.12%)
• 🟥 compiled/qsort//instructions: +160.3M (+0.94%)
• 🟥 compiled/rbmap//instructions: +366.0M (+4.42%)
• 🟥 compiled/rbmap_checkpoint//instructions: +378.6M (+2.90%)
• 🟥 compiled/rbmap_checkpoint2//instructions: +367.6M (+4.13%)
• 🟥 compiled/rbmap_fbip//instructions: +690.1M (+9.65%)
• ✅ compiled/rbmap_library//instructions: -606.3M (-6.32%)
• ✅ compiled/sigmaIterator//instructions: -30.0M (-1.12%)
• ✅ compiled/treemap//instructions: -215.8M (-1.24%)
• 🟥 compiled/unionfind//instructions: +539.9M (+2.03%)
• ✅ size/compile/.out//bytes: -63MiB (-2.39%)
• ✅ size/libleanshared.so//bytes: -3MiB (-1.91%)

Medium changes (1✅, 17🟥)

• 🟥 build//instructions: +89.8G (+0.80%)
• 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.0G (+0.75%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.5G (+0.80%)
• 🟥 compiled/iterators//instructions: +4.5M (+0.81%)
• 🟥 compiled/liasolver//instructions: +25.0M (+0.71%)
• 🟥 compiled/workspaceSymbolsNewRanges//instructions: +10.2M (+1.45%)
• 🟥 elab/big_do//instructions: +106.1M (+0.53%)
• 🟥 elab/big_match//instructions: +69.0M (+0.67%)
• 🟥 elab/big_match_nat_split//instructions: +100.8M (+0.97%)
• 🟥 elab/big_match_partial//instructions: +124.9M (+0.91%)
• 🟥 elab/big_omega_MT//instructions: +129.7M (+0.61%)
• 🟥 elab/cbv_decide//instructions: +399.5M (+0.93%)
• 🟥 elab/grind_bitvec2//instructions: +1.3G (+0.88%)
• 🟥 elab/grind_list2//instructions: +412.4M (+0.93%)
• 🟥 elab/grind_ring_5//instructions: +57.1M (+0.67%)
• 🟥 elab/mut_rec_wf//instructions: +172.5M (+0.80%)
• 🟥 interpreted/iterators//instructions: +34.1M (+0.10%)
• ✅ size/install//bytes: -13MiB (-0.43%)

and 1 hidden

Small changes (999🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 2ff4ac1 against 548f78b are in. There are significant results. @hargoniX

• 🟥 build//instructions: +32.6G (+0.29%)

Large changes (6✅, 13🟥)

• ✅ compiled/binarytrees.st//instructions: -931.4M (-1.65%)
• ✅ compiled/binarytrees//instructions: -932.7M (-1.64%)
• 🟥 compiled/deriv//instructions: +91.5M (+1.35%)
• 🟥 compiled/hashmap//instructions: +66.5M (+1.99%)
• 🟥 compiled/ilean_roundtrip//instructions: +82.1M (+0.36%)
• 🟥 compiled/io_compute//instructions: +87.2M (+0.78%)
• 🟥 compiled/parser//instructions: +185.7M (+0.54%)
• 🟥 compiled/phashmap//instructions: +102.6M (+1.16%)
• 🟥 compiled/qsort//instructions: +96.0M (+0.56%)
• 🟥 compiled/rbmap//instructions: +238.5M (+2.88%)
• 🟥 compiled/rbmap_checkpoint//instructions: +247.9M (+1.90%)
• 🟥 compiled/rbmap_checkpoint2//instructions: +239.0M (+2.69%)
• 🟥 compiled/rbmap_fbip//instructions: +465.5M (+6.51%)
• 🟥 compiled/rbmap_library//instructions: +262.8M (+2.74%)
• ✅ compiled/sigmaIterator//instructions: -60.1M (-2.24%)
• ✅ compiled/treemap//instructions: -297.0M (-1.70%)
• 🟥 compiled/unionfind//instructions: +228.7M (+0.86%)
• ✅ size/compile/.out//bytes: -69MiB (-2.61%)
• ✅ size/libleanshared.so//bytes: -3MiB (-1.81%)

Medium changes (1✅, 2🟥)

• 🟥 compiled/iterators//instructions: +3.6M (+0.66%)
• 🟥 compiled/workspaceSymbolsNewRanges//instructions: +7.6M (+1.08%)
• ✅ size/install//bytes: -12MiB (-0.41%)

Small changes (1✅, 158🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 2d865d2 against 548f78b are in. There are significant results. @hargoniX

• ✅ build//instructions: -10.1G (-0.09%)

Large changes (4✅, 2🟥)

• ✅ compiled/rbmap//instructions: -54.5M (-0.66%)
• ✅ compiled/rbmap_checkpoint2//instructions: -55.0M (-0.62%)
• 🟥 compiled/rbmap_library//instructions: +158.3M (+1.65%)
• ✅ compiled/sigmaIterator//instructions: -60.2M (-2.25%)
• 🟥 compiled/treemap//instructions: +134.9M (+0.77%)
• ✅ compiled/unionfind//instructions: -52.6M (-0.20%)

Medium changes (3✅)

• ✅ compiled/parser//instructions: -22.9M (-0.07%)
• ✅ compiled/rbmap_checkpoint//instructions: -54.7M (-0.42%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.3G (-1.05%)

Small changes (19✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 548f78b6df79791338293f5c658db853c6f8a6c0 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-12 20:10:20)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 548f78b6df79791338293f5c658db853c6f8a6c0 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-12 20:10:22)