feat: non exponential codegen for reset-reuse by hargoniX · Pull Request #12665 · leanprover/lean4

hargoniX · 2026-02-23T21:08:01Z

This PR ports the expand reset/reuse pass from IR to LCNF. In addition it prevents exponential code generation unlike the old one. This results in a ~15% decrease in binary size and slight speedups across the board.

The change also removes the "is this reset actually used" syntactic approximation as the previous passes guarantee (at the moment) that all uses are in the continuation and will thus be caught by this.

hargoniX · 2026-02-23T21:08:03Z

!bench

leanprover-radar · 2026-02-23T21:08:10Z

Benchmark results for d851a15 against d20b6ec are in! @hargoniX

🟥 build//instructions: +360.2G (+2.85%)

Large changes (5✅, 38🟥)

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

Medium changes (7✅, 84🟥)

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

Small changes (20✅, 2113🟥)

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

hargoniX · 2026-02-23T22:14:12Z

!bench

leanprover-radar · 2026-02-23T22:14:19Z

Benchmark results for 1657843 against d20b6ec are in! @hargoniX

🟥 build//instructions: +78.6G (+0.62%)
🟥 other exited with code 1

Large changes (3✅)

✅ size/all/.ir//bytes: -25MiB (-7.14%)
✅ size/install//bytes: -94MiB (-3.76%)
✅ size/libleanshared.so//bytes: -26MiB (-15.51%)

Medium changes (3✅, 1🟥)

✅ build/module/Init.Meta//bytes .olean: -75kiB (-20.81%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -49kiB (-22.77%)
✅ build/module/Lake.Load.Toml//bytes .olean: -129kiB (-23.68%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.5G (+0.72%)

Small changes (51✅, 922🟥)

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

mathlib-lean-pr-testing · 2026-02-23T22:15:52Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d20b6ece5816d36041b5a8c7caaf17c99f7d3ea2 --onto e7e3588c973226e85d79ed0f3154cfca79b61c6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 22:15:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cd7f55b6c92b6d20fb2a0428abc097fa8be421b3 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 10:43:46)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1e0bfe931f28f0d73d40554aac2662815fac27ca --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-25 11:40:48)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e96d969d5935c1b026c0e80d60626c8da88d0922 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-25 14:49:00)

leanprover-bot · 2026-02-23T22:15:53Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d20b6ece5816d36041b5a8c7caaf17c99f7d3ea2 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 22:15:53)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cd7f55b6c92b6d20fb2a0428abc097fa8be421b3 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 10:43:48)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1e0bfe931f28f0d73d40554aac2662815fac27ca --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-25 11:40:50)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e96d969d5935c1b026c0e80d60626c8da88d0922 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-25 14:49:02)

hargoniX · 2026-02-23T22:40:11Z

!bench

leanprover-radar · 2026-02-23T22:40:17Z

Benchmark results for 1414e72 against d20b6ec are in! @hargoniX

🟥 build//instructions: +77.5G (+0.61%)
🟥 other exited with code 1

Large changes (3✅)

✅ size/all/.ir//bytes: -25MiB (-7.14%)
✅ size/install//bytes: -94MiB (-3.76%)
✅ size/libleanshared.so//bytes: -26MiB (-15.51%)

Medium changes (3✅, 1🟥)

✅ build/module/Init.Meta//bytes .olean: -75kiB (-20.81%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -49kiB (-22.77%)
✅ build/module/Lake.Load.Toml//bytes .olean: -129kiB (-23.68%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.5G (+0.70%)

Small changes (52✅, 919🟥)

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

hargoniX · 2026-02-23T23:24:24Z

!bench

leanprover-radar · 2026-02-23T23:24:28Z

Benchmark results for 49e4a0b against d20b6ec are in! @hargoniX

🟥 build//instructions: +78.0G (+0.62%)

Large changes (11✅, 16🟥)

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

Medium changes (5✅, 18🟥)

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

Small changes (54✅, 944🟥)

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

hargoniX · 2026-02-24T09:48:43Z

!bench

leanprover-radar · 2026-02-24T09:49:04Z

Benchmark results for d598d0a against cd7f55b are in! @hargoniX

🟥 build//instructions: +55.8G (+0.44%)

Large changes (11✅, 15🟥)

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

Medium changes (5✅, 13🟥)

🟥 Init.Data.BitVec.Lemmas//instructions: +562.5M (+0.45%)
🟥 Init.Data.List.Sublist async//instructions: +92.1M (+0.83%)
🟥 Init.Prelude async//instructions: +161.0M (+1.31%)
🟥 Std.Data.Internal.List.Associative//instructions: +641.0M (+0.80%)
✅ big_match_nat//instructions: -115.3M (-2.15%)
🟥 big_omega.lean//instructions: +169.7M (+0.71%)
🟥 big_struct_dep//instructions: +57.5M (+0.28%)
✅ build/module/Init.Meta//bytes .olean: -76kiB (-21.01%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -50kiB (-23.26%)
✅ build/module/Lake.Load.Toml//bytes .olean: -130kiB (-23.94%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.2G (+0.55%)
🟥 bv_decide_rewriter.lean//instructions: +106.6M (+0.98%)
🟥 deriv//instructions: +5.1M (+0.07%)
🟥 grind_bitvec2.lean//instructions: +1.2G (+0.61%)
🟥 grind_list2.lean//instructions: +384.0M (+0.66%)
✅ ilean roundtrip//instructions: -238.3M (-0.91%)
🟥 phashmap.lean//instructions: +168.5M (+1.69%)
🟥 simp_subexpr//instructions: +206.3M (+1.57%)

Small changes (72✅, 629🟥)

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

hargoniX · 2026-02-24T13:31:31Z

!bench

leanprover-radar · 2026-02-24T13:31:36Z

Benchmark results for 618677f against cd7f55b are in! @hargoniX

🟥 build//instructions: +61.9G (+0.49%)

Large changes (11✅, 15🟥)

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

Medium changes (5✅, 15🟥)

🟥 Init.Data.BitVec.Lemmas//instructions: +680.0M (+0.54%)
🟥 Init.Data.List.Sublist async//instructions: +99.0M (+0.89%)
🟥 Init.Prelude async//instructions: +159.5M (+1.30%)
🟥 Std.Data.Internal.List.Associative//instructions: +705.0M (+0.88%)
✅ big_match_nat//instructions: -111.5M (-2.08%)
🟥 big_omega.lean//instructions: +206.5M (+0.87%)
🟥 big_struct_dep//instructions: +60.3M (+0.29%)
✅ build/module/Init.Meta//bytes .olean: -76kiB (-20.99%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -49kiB (-22.97%)
✅ build/module/Lake.Load.Toml//bytes .olean: -129kiB (-23.77%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.3G (+0.62%)
🟥 bv_decide_rewriter.lean//instructions: +121.3M (+1.12%)
🟥 cbv tactic (leroy compiler verification course)//instructions: +287.8M (+0.59%)
🟥 charactersIn//instructions: +187.7M (+0.47%)
🟥 grind_bitvec2.lean//instructions: +1.5G (+0.75%)
🟥 grind_list2.lean//instructions: +467.0M (+0.81%)
🟥 identifier auto-completion//instructions: +356.4M (+0.49%)
✅ ilean roundtrip//instructions: -119.9M (-0.46%)
🟥 simp_subexpr//instructions: +228.5M (+1.74%)
🟥 tests/bench/ interpreted//instructions: +1.3G (+0.60%)

Small changes (71✅, 721🟥)

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

hargoniX · 2026-02-24T14:04:42Z

!bench

leanprover-radar · 2026-02-24T14:04:48Z

Benchmark results for 0a23f5b against cd7f55b are in! @hargoniX

🟥 build//instructions: +129.0G (+1.02%)

Large changes (5✅, 25🟥)

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

Medium changes (4✅, 27🟥)

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

Small changes (26✅, 1455🟥)

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

hargoniX · 2026-02-24T16:27:41Z

!bench

leanprover-radar · 2026-02-24T16:27:48Z

Benchmark results for 9bb5aa4 against cd7f55b are in! @hargoniX

🟥 build//instructions: +62.1G (+0.49%)

Large changes (11✅, 15🟥)

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

Medium changes (5✅, 16🟥)

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

Small changes (71✅, 719🟥)

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

hargoniX · 2026-02-24T17:38:52Z

!bench

leanprover-radar · 2026-02-24T17:38:58Z

Benchmark results for e6ae02b against cd7f55b are in! @hargoniX

🟥 build//instructions: +59.3G (+0.47%)

Large changes (11✅, 15🟥)

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

Medium changes (5✅, 15🟥)

✅ build/module/Init.Meta//bytes .olean: -76kiB (-20.99%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -49kiB (-22.97%)
✅ build/module/Lake.Load.Toml//bytes .olean: -129kiB (-23.77%)
🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.3G (+0.59%)
✅ compiled/ilean_roundtrip//instructions: -119.3M (-0.45%)
✅ elab/big_match_nat//instructions: -111.3M (-2.07%)
🟥 elab/big_omega//instructions: +203.4M (+0.86%)
🟥 elab/big_struct_dep//instructions: +58.1M (+0.28%)
🟥 elab/bv_decide_rewriter//instructions: +118.1M (+1.09%)
🟥 elab/cbv_leroy//instructions: +287.5M (+0.59%)
🟥 elab/charactersIn//instructions: +188.6M (+0.47%)
🟥 elab/grind_bitvec2//instructions: +1.4G (+0.72%)
🟥 elab/grind_list2//instructions: +462.4M (+0.80%)
🟥 elab/simp_subexpr//instructions: +234.6M (+1.79%)
🟥 interpreted/identifier_completion//instructions: +346.1M (+0.48%)
🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +657.3M (+0.52%)
🟥 misc/import Init.Data.List.Sublist//instructions: +97.2M (+0.87%)
🟥 misc/import Init.Prelude//instructions: +157.1M (+1.28%)
🟥 misc/import Std.Data.Internal.List.Associative//instructions: +693.1M (+0.87%)
🟥 tests/bench/ interpreted//instructions: +1.2G (+0.56%)

Small changes (74✅, 699🟥)

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

hargoniX · 2026-02-24T22:35:02Z

!bench

leanprover-radar · 2026-02-24T22:35:08Z

Benchmark results for 53d0803 against cd7f55b are in! @hargoniX

✅ build//instructions: -40.9G (-0.32%)

Large changes (15✅, 8🟥)

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

Medium changes (10✅)

✅ build/module/Init.Meta//bytes .olean: -76kiB (-21.16%)
✅ build/module/Lake.CLI.Translate.Lean//bytes .olean: -49kiB (-23.09%)
✅ build/module/Lake.Load.Toml//bytes .olean: -129kiB (-23.80%)
✅ compiled/watchdogRss//instructions: -255.5M (-0.99%)
✅ compiled/workspaceSymbolsNewRanges//instructions: -19.2M (-2.45%)
✅ elab/big_match_nat//instructions: -149.6M (-2.78%)
✅ elab/big_match_nat_split//instructions: -129.5M (-1.08%)
✅ elab/bv_decide_mul//instructions: -909.5M (-2.12%)
✅ elab/simp_local//instructions: -280.1M (-0.62%)
✅ interpreted/identifier_completion//instructions: -446.5M (-0.61%)

Small changes (374✅, 47🟥)

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

hargoniX · 2026-02-25T13:05:12Z

!bench

leanprover-radar · 2026-02-25T13:05:37Z

Benchmark results for 162e194 against e96d969 are in! @hargoniX

✅ build//instructions: -49.9G (-0.40%)

Large changes (15✅, 8🟥)

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

Medium changes (8✅, 1🟥)

✅ build/module/Lake.CLI.Main//instructions: -1.0G (-2.87%) (reduced significance based on absolute threshold)
✅ compiled/watchdogRss//instructions: -260.5M (-1.01%)
✅ compiled/workspaceSymbolsNewRanges//instructions: -19.2M (-2.44%)
✅ elab/big_match_nat//instructions: -152.9M (-2.84%)
✅ elab/big_match_nat_split//instructions: -130.8M (-1.09%)
🟥 elab/big_omega_MT//instructions: +66.8M (+0.28%)
✅ elab/bv_decide_mul//instructions: -904.4M (-2.10%)
✅ elab/simp_local//instructions: -286.4M (-0.63%)
✅ interpreted/identifier_completion//instructions: -459.2M (-0.63%)

Small changes (393✅, 6🟥)

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

hargoniX added the changelog-compiler Compiler, runtime, and FFI label Feb 23, 2026

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

hargoniX force-pushed the hbv/expand_reset_reuse_ctors branch from 49e4a0b to d598d0a Compare February 24, 2026 09:48

hargoniX force-pushed the hbv/expand_reset_reuse_ctors branch 3 times, most recently from f23e947 to 186b394 Compare February 25, 2026 12:20

hargoniX added the release-ci Enable all CI checks for a PR, like is done for releases label Feb 25, 2026

hargoniX added 3 commits February 26, 2026 09:13

feat: implement

4118999

chore: delete IR

5af146b

final

b738255

hargoniX force-pushed the hbv/expand_reset_reuse_ctors branch from 162e194 to b738255 Compare February 26, 2026 09:14

tests

c4f8d4d

hargoniX removed the release-ci Enable all CI checks for a PR, like is done for releases label Feb 26, 2026

hargoniX marked this pull request as ready for review February 26, 2026 09:28

hargoniX requested a review from leodemoura as a code owner February 26, 2026 09:28

hargoniX enabled auto-merge February 26, 2026 09:29

hargoniX added this pull request to the merge queue Feb 26, 2026

Merged via the queue into master with commit d88ac25 Feb 26, 2026
22 checks passed

hargoniX deleted the hbv/expand_reset_reuse_ctors branch February 26, 2026 10:13

Conversation

hargoniX commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 23, 2026

Uh oh!

leanprover-radar commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 23, 2026

Uh oh!

leanprover-radar commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 23, 2026

Uh oh!

leanprover-radar commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 23, 2026

Uh oh!

leanprover-radar commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented Feb 25, 2026

Uh oh!

leanprover-radar commented Feb 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hargoniX commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 23, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Feb 23, 2026 •

edited

Loading

leanprover-bot commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 25, 2026 •

edited

Loading