perf: use xType field rather than conservatively recomputing it #9345

zwarich · 2025-07-13T21:51:28Z

No description provided.

zwarich · 2025-07-13T21:51:47Z

!bench

leanprover-community-bot · 2025-07-13T22:10:56Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f298360ff9d473d54258398ce9f202c5ae4cc3bf --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-13 22:10:56)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c90cc392f722145d51935a781a5e8214f3650230 --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-13 22:51:38)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 74206c755f8d455a4719095ec28810249e59c0ea --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-14 01:26:12)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 87dae299b89f7dffebae8ccd9bb8111250ef4a98 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-27 22:48:19)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 87dae299b89f7dffebae8ccd9bb8111250ef4a98 --onto 95e753c6b42900cb727b726646d1f884df87c7db. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-28 00:57:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0fe7cc87941dea9e9252d7ed442d6301af6344c2 --onto e38f0c699014515ab0c40a9c5d794029177ecec4. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-28 16:54:45)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab87a6f797b0ca4cf847a3eabe7e07377505dae4 --onto e38f0c699014515ab0c40a9c5d794029177ecec4. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-28 19:57:53)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e3517f1c86d84ff031f0590214f835106649aafb --onto 6ae31ea2d6e9d6d30c0e2bedac166377a15d07ef. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-29 23:27:18)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9006af4a965c797e18000600b1893684eb0027b8 --onto 6ae31ea2d6e9d6d30c0e2bedac166377a15d07ef. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-30 04:22:43)

leanprover-bot · 2025-07-13T22:10:58Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f298360ff9d473d54258398ce9f202c5ae4cc3bf --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-13 22:10:57)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c90cc392f722145d51935a781a5e8214f3650230 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-13 22:51:39)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 74206c755f8d455a4719095ec28810249e59c0ea --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-14 01:26:13)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 87dae299b89f7dffebae8ccd9bb8111250ef4a98 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-27 22:48:20)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0fe7cc87941dea9e9252d7ed442d6301af6344c2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-28 16:54:47)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab87a6f797b0ca4cf847a3eabe7e07377505dae4 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-28 19:57:54)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e3517f1c86d84ff031f0590214f835106649aafb --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-29 23:27:19)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9006af4a965c797e18000600b1893684eb0027b8 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-30 04:22:45)

leanprover-bot · 2025-07-13T22:20:14Z

Here are the benchmark results for commit 5f1633b.
There were significant changes against commit f298360:

  Benchmark                            Metric                  Change
  =============================================================================
- Init.Data.List.Sublist re-elab -j4   branch-misses             1.3%  (23.2 σ)
- hashmap.lean                         eraseInsert              10.1%  (24.8 σ)
- hashmap.lean                         insertHit                12.8%
- hashmap.lean                         insertIfNewHit            9.4%
- hashmap.lean                         insertMissEmpty          13.4%  (26.7 σ)
- hashmap.lean                         iterate                   6.3%
- hashmap.lean                         task-clock               10.7%  (63.4 σ)
- hashmap.lean                         wall-clock               10.7%  (67.2 σ)
+ stdlib                               blocked (unaccounted)    -1.4% (-29.3 σ)
+ stdlib                               congr simp thm           -1.6% (-24.3 σ)
+ stdlib                               grind canon              -1.2% (-85.0 σ)
- workspaceSymbols                     instructions              1.0% (499.1 σ)

zwarich · 2025-07-13T22:29:57Z

!bench

leanprover-bot · 2025-07-13T23:15:07Z

Here are the benchmark results for commit 81a0418.
There were significant changes against commit c90cc39:

  Benchmark                            Metric                        Change
  ====================================================================================
+ Init.Data.List.Sublist re-elab -j4   maxrss                         -1.2% (-411.0 σ)
+ bv_decide_rewriter.lean              task-clock                     -3.2%  (-88.3 σ)
+ bv_decide_rewriter.lean              wall-clock                     -3.6%  (-64.3 σ)
- channel.lean                         boundedn_mpsc                  17.2%   (28.2 σ)
- hashmap.lean                         eraseInsert                    13.2%   (21.8 σ)
- hashmap.lean                         insertHit                      14.1%   (30.9 σ)
- hashmap.lean                         insertIfNewHit                  7.1%
- hashmap.lean                         insertMissEmpty                18.4%   (28.8 σ)
- hashmap.lean                         insertMissEmptyWithCapacity    16.0%   (27.9 σ)
- hashmap.lean                         iterate                         1.8%
- hashmap.lean                         task-clock                     12.2%   (22.1 σ)
- hashmap.lean                         wall-clock                     12.2%   (22.0 σ)
+ stdlib                               dsimp                          -3.7%  (-55.6 σ)
- workspaceSymbols                     instructions                    1.0%  (354.3 σ)

zwarich · 2025-07-13T23:27:37Z

I'm very confused about the hashmap regressions, because the generated IR didn't change at all.

zwarich · 2025-07-14T01:03:52Z

!bench

leanprover-bot · 2025-07-14T01:56:19Z

Here are the benchmark results for commit 77a4c36.
There were significant changes against commit 74206c7:

  Benchmark                            Metric                  Change
  ==============================================================================
- Init.Data.List.Sublist re-elab -j4   wall-clock                1.1%   (52.3 σ)
- hashmap.lean                         insertIfNewHit            7.4%
- hashmap.lean                         insertMissEmpty          10.7%   (22.1 σ)
- hashmap.lean                         iterate                   5.0%
- hashmap.lean                         task-clock                8.5%   (24.6 σ)
- hashmap.lean                         wall-clock                8.5%   (24.1 σ)
+ stdlib                               attribute application    -1.1%  (-39.6 σ)
- workspaceSymbols                     instructions              1.0% (1326.0 σ)

zwarich · 2025-07-16T17:21:24Z

!bench

leanprover-bot · 2025-07-16T17:57:07Z

Here are the benchmark results for commit c874073.
There were significant changes against commit f3944a3:

  Benchmark          Metric                    Change
  =============================================================
+ hashmap.lean       eraseInsert               -11.9% (-30.6 σ)
+ hashmap.lean       insertHit                 -14.5% (-27.1 σ)
- stdlib             grind mark subsingleton     1.2%  (27.7 σ)
- workspaceSymbols   instructions                1.0% (538.8 σ)

zwarich · 2025-07-27T22:05:05Z

Including #9563 for benchmarking to see if this weird workplaceSymbols regression goes away.

zwarich · 2025-07-27T22:21:04Z

!bench

leanprover-bot · 2025-07-27T22:56:39Z

Here are the benchmark results for commit fac2434.
There were significant changes against commit 87dae29:

  Benchmark                 Metric                  Change
  ==============================================================================
+ bv_decide_rewriter.lean   wall-clock               -4.2%             (-30.0 σ)
- channel.lean              boundedn_mpsc             8.7% (431455047186873.3 σ)
- hashmap.lean              branch-misses             6.3%              (37.3 σ)
+ nat_repr                  branches                 -2.0%           (-1168.6 σ)
- phashmap.lean             insertMissEmptyShared    19.4%              (98.1 σ)
- phashmap.lean             task-clock               16.3%              (26.5 σ)
- phashmap.lean             wall-clock               16.3%              (26.9 σ)
- stdlib                    type checking             1.7%              (96.0 σ)
+ workspaceSymbols          instructions             -4.7%          (-17910.9 σ)

zwarich · 2025-07-28T00:15:42Z

Looks like there is still a (smaller) regression on workplaceSymbols. I'm going to try selectively enabling the optimization until I find the files responsible for the regression.

zwarich · 2025-07-28T00:15:45Z

!bench

leanprover-bot · 2025-07-28T00:50:10Z

Here are the benchmark results for commit fa71853.
There were significant changes against commit 87dae29:

  Benchmark      Metric         Change
  ===============================================
+ channel.lean   boundedn_seq    -7.3%
+ nat_repr       branches        -2.0% (-954.7 σ)
+ stdlib         grind simp      -2.1%  (-22.9 σ)

zwarich · 2025-07-28T03:08:01Z

!bench

leanprover-bot · 2025-07-28T03:42:01Z

Here are the benchmark results for commit fa73ed7.
There were significant changes against commit 87dae29:

  Benchmark       Metric     Change
  ============================================
+ channel.lean    maxrss      -1.8%  (-25.5 σ)
+ hashmap.lean    maxrss      -2.0%  (-39.4 σ)
+ lake startup    maxrss      -1.8%  (-21.5 σ)
+ liasolver       maxrss      -2.0%  (-32.8 σ)
+ nat_repr        branches    -2.0% (-393.4 σ)
+ nat_repr        maxrss      -1.8%  (-27.6 σ)
+ parser          maxrss      -2.1%  (-43.3 σ)
+ phashmap.lean   maxrss      -1.8%  (-31.7 σ)
+ qsort           maxrss      -1.8%  (-32.6 σ)
+ rbmap           maxrss      -2.0%  (-31.5 σ)
+ rbmap_fbip      maxrss      -1.8%  (-28.2 σ)
- stdlib          dsimp        3.7%   (23.8 σ)
+ treemap.lean    maxrss      -2.1%  (-35.4 σ)
+ unionfind       maxrss      -2.0%  (-31.5 σ)

zwarich · 2025-07-28T03:55:14Z

!bench

leanprover-bot · 2025-07-28T04:29:09Z

Here are the benchmark results for commit 63c7bdf.
There were significant changes against commit 87dae29:

  Benchmark       Metric           Change
  ==================================================
- hashmap.lean    branch-misses      6.4%   (32.3 σ)
+ nat_repr        branches          -2.0% (-439.3 σ)
- phashmap.lean   containsHit        1.2%
+ stdlib          congr simp thm    -2.5%  (-34.4 σ)

zwarich · 2025-07-28T04:31:00Z

!bench

leanprover-bot · 2025-07-28T05:05:03Z

Here are the benchmark results for commit bbab333.
There were significant changes against commit 87dae29:

  Benchmark             Metric                        Change
  =====================================================================
- hashmap.lean          insertHit                      12.5%
- hashmap.lean          insertIfNewHit                 18.1%
- hashmap.lean          insertMissEmpty                15.9%   (36.0 σ)
- hashmap.lean          insertMissEmptyWithCapacity    11.7%   (23.0 σ)
- hashmap.lean          iterate                         7.2%
- hashmap.lean          task-clock                     11.4%   (29.8 σ)
- hashmap.lean          wall-clock                     11.3%   (29.5 σ)
+ nat_repr              branches                       -2.0% (-802.0 σ)
- phashmap.lean         containsMiss                   20.0%
- phashmap.lean         eraseInsert                    15.6%   (26.6 σ)
- phashmap.lean         insertMissEmptyShared          17.9%   (52.3 σ)
- phashmap.lean         task-clock                     16.0%   (27.7 σ)
- phashmap.lean         wall-clock                     16.0%   (28.5 σ)
- riscv-ast.lean        wall-clock                      2.5%   (26.5 σ)
+ simp_bubblesort_256   task-clock                     -5.2%  (-25.2 σ)
+ simp_bubblesort_256   wall-clock                     -5.8%  (-28.3 σ)
- stdlib                grind ematch                    4.3%   (20.8 σ)
- stdlib                let-to-have transformation      1.1%   (44.2 σ)
- stdlib                maxrss                          4.0%   (32.3 σ)
- stdlib                type checking                   2.0%   (42.4 σ)
- unionfind             task-clock                     11.2%  (161.0 σ)
- unionfind             wall-clock                     11.2%  (134.9 σ)

zwarich · 2025-07-28T16:15:13Z

!bench

leanprover-bot · 2025-07-28T16:53:07Z

Here are the benchmark results for commit e4f2926.
There were significant changes against commit 0fe7cc8:

  Benchmark          Metric            Change
  =====================================================
+ hashmap.lean       containsHit        -6.0%
+ hashmap.lean       containsMiss       -6.8%
+ hashmap.lean       insertMissEmpty   -10.1%
- stdlib             type checking       1.3%  (25.7 σ)
- workspaceSymbols   instructions        1.3% (488.5 σ)

zwarich · 2025-07-28T19:03:45Z

!bench

zwarich · 2025-07-28T19:36:52Z

!bench

leanprover-bot · 2025-07-28T20:24:23Z

Here are the benchmark results for commit dee8ea1.
There were significant changes against commit ab87a6f:

  Benchmark          Metric                 Change
  ===========================================================
+ phashmap.lean      insertMissEmpty         -7.6%
- stdlib             grind cutsat             6.2%   (52.0 σ)
- stdlib             instantiate metavars     1.3%   (35.0 σ)
+ stdlib             maxrss                  -1.6%  (-24.7 σ)
- workspaceSymbols   instructions             1.5% (2590.4 σ)
- workspaceSymbols   wall-clock               3.3%   (22.2 σ)

zwarich · 2025-07-29T22:31:55Z

!bench

leanprover-bot · 2025-07-29T23:31:56Z

Here are the benchmark results for commit 3b5aeff.
There were significant changes against commit e3517f1:

  Benchmark          Metric         Change
  ===================================================
- channel.lean       boundedn_seq     5.6%
- hashmap.lean       iterate          2.1%
+ lake build clean   maxrss          -1.2%  (-34.0 σ)
+ nat_repr           branches        -2.0% (-676.0 σ)
- workspaceSymbols   instructions     1.6%   (82.4 σ)

zwarich · 2025-07-30T00:01:40Z

!bench

leanprover-bot · 2025-07-30T01:05:40Z

Here are the benchmark results for commit 4243ab8.
There were significant changes against commit e3517f1:

  Benchmark          Metric                  Change
  ============================================================
+ nat_repr           branches                 -2.0% (-836.2 σ)
- phashmap.lean      containsHit               4.3%
- phashmap.lean      containsMiss              9.1%
- phashmap.lean      insertMissEmptyShared    19.3%   (30.6 σ)
- phashmap.lean      iterate                   8.7%
- stdlib             grind                     1.5%   (36.2 σ)
- workspaceSymbols   instructions              1.6%  (370.5 σ)

zwarich · 2025-07-30T01:14:06Z

!bench

leanprover-bot · 2025-07-30T02:12:59Z

Here are the benchmark results for commit 97baebd.
There were significant changes against commit e3517f1:

  Benchmark          Metric                      Change
  ================================================================
+ nat_repr           branches                     -2.0% (-388.4 σ)
- phashmap.lean      containsHit                   4.3%
+ rbmap_library      maxrss                       -5.4%  (-34.2 σ)
+ stdlib             grind typeclass inference    -2.1%  (-38.8 σ)
- workspaceSymbols   instructions                  1.7%   (39.0 σ)

zwarich · 2025-07-30T03:38:04Z

I looked at the whole IR diff that produces this minor regression (with this optimization applied to a single top-level decl), and It all looks beneficial with respect to our IR cost model (and the regression doesn't occur on my machine). I'm going to go ahead and land this (after double checking the results with the full change), because this keeps coming up again and again when looking at IR dumps.

zwarich · 2025-07-30T03:38:23Z

!bench

leanprover-bot · 2025-07-30T04:12:47Z

Here are the benchmark results for commit b26ef62.
There were significant changes against commit 9006af4:

  Benchmark                  Metric         Change
  ==========================================================
+ bv_decide_large_aig.lean   task-clock     -12.2% (-91.0 σ)
+ bv_decide_large_aig.lean   wall-clock     -12.0% (-29.3 σ)
- bv_decide_mod              task-clock       2.8%  (73.3 σ)
+ liasolver                  task-clock      -9.0% (-34.4 σ)
+ liasolver                  wall-clock      -9.0% (-32.3 σ)
+ phashmap.lean              containsHit     -2.0%
- workspaceSymbols           instructions     1.6% (130.9 σ)

zwarich requested a review from leodemoura as a code owner July 13, 2025 21:51

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 13, 2025

zwarich force-pushed the boxing-getScrutineeType branch from 5f1633b to 81a0418 Compare July 13, 2025 22:29

zwarich force-pushed the boxing-getScrutineeType branch from 81a0418 to 77a4c36 Compare July 14, 2025 01:03

zwarich force-pushed the boxing-getScrutineeType branch from 77a4c36 to c874073 Compare July 16, 2025 17:21

zwarich force-pushed the boxing-getScrutineeType branch from c874073 to fac2434 Compare July 27, 2025 22:04

zwarich marked this pull request as draft July 27, 2025 22:58

zwarich force-pushed the boxing-getScrutineeType branch from fac2434 to fa71853 Compare July 28, 2025 00:12

zwarich force-pushed the boxing-getScrutineeType branch from fa73ed7 to 63c7bdf Compare July 28, 2025 03:54

zwarich force-pushed the boxing-getScrutineeType branch from bbab333 to e4f2926 Compare July 28, 2025 16:06

zwarich force-pushed the boxing-getScrutineeType branch from e4f2926 to dee8ea1 Compare July 28, 2025 19:03

zwarich force-pushed the boxing-getScrutineeType branch from dee8ea1 to 3b5aeff Compare July 29, 2025 22:30

perf: use xType field rather than conservatively recomputing it

b26ef62

zwarich force-pushed the boxing-getScrutineeType branch from 97baebd to b26ef62 Compare July 30, 2025 03:36

zwarich changed the title ~~chore: rely on xType field rather than recomputing it~~ perf: use xType field rather than conservatively recomputing it Jul 30, 2025

zwarich marked this pull request as ready for review July 30, 2025 04:33

zwarich added this pull request to the merge queue Jul 30, 2025

Merged via the queue into leanprover:master with commit 7931e19 Jul 30, 2025
20 checks passed

perf: use xType field rather than conservatively recomputing it #9345

perf: use xType field rather than conservatively recomputing it #9345

Conversation

zwarich commented Jul 13, 2025

Uh oh!

zwarich commented Jul 13, 2025

Uh oh!

leanprover-community-bot commented Jul 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jul 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jul 13, 2025

Uh oh!

zwarich commented Jul 13, 2025

Uh oh!

leanprover-bot commented Jul 13, 2025

Uh oh!

zwarich commented Jul 13, 2025

Uh oh!

zwarich commented Jul 14, 2025

Uh oh!

leanprover-bot commented Jul 14, 2025

Uh oh!

zwarich commented Jul 16, 2025

Uh oh!

leanprover-bot commented Jul 16, 2025

Uh oh!

zwarich commented Jul 27, 2025

Uh oh!

zwarich commented Jul 27, 2025

Uh oh!

leanprover-bot commented Jul 27, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

zwarich commented Jul 28, 2025

Uh oh!

leanprover-bot commented Jul 28, 2025

Uh oh!

zwarich commented Jul 29, 2025

Uh oh!

leanprover-bot commented Jul 29, 2025

Uh oh!

zwarich commented Jul 30, 2025

Uh oh!

leanprover-bot commented Jul 30, 2025

Uh oh!

zwarich commented Jul 30, 2025

Uh oh!

leanprover-bot commented Jul 30, 2025

Uh oh!

zwarich commented Jul 30, 2025

Uh oh!

zwarich commented Jul 30, 2025

Uh oh!

leanprover-bot commented Jul 30, 2025

leanprover-community-bot commented Jul 13, 2025 •

edited

Loading

leanprover-bot commented Jul 13, 2025 •

edited

Loading