perf: dec specialization

[hargoniX]

This PR generates specialized code for invoking dec on values whose shape is known. This puts branch prediction pressure off lean_dec_ref_cold as the shape of the constructor should now be compiled into the executable.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for b5ce70c against e09155b are in. There are significant results. @hargoniX

• ✅ build//instructions: -219.4G (-1.91%)

Large changes (14✅, 3🟥)

• ✅ compiled/deriv//instructions: -182.9M (-2.63%)
• ✅ compiled/hashmap//instructions: -40.3M (-1.19%)
• ✅ compiled/ilean_roundtrip//instructions: -373.2M (-1.58%)
• ✅ compiled/liasolver//instructions: -106.7M (-2.60%)
• ✅ compiled/parser//instructions: -145.9M (-0.42%)
• ✅ compiled/phashmap//instructions: -71.0M (-0.80%)
• ✅ compiled/rbmap//instructions: -173.4M (-2.05%)
• ✅ compiled/rbmap_checkpoint2//instructions: -109.8M (-1.22%)
• ✅ compiled/rbmap_fbip//instructions: -62.2M (-0.86%)
• ✅ compiled/rbmap_library//instructions: -73.4M (-0.77%)
• ✅ compiled/unionfind//instructions: -376.4M (-1.39%)
• ✅ compiled/watchdogRss//instructions: -425.4M (-1.66%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -16.7M (-2.33%)
• ✅ elab/big_do//instructions: -503.5M (-2.28%)
• 🟥 size/compile/.out//bytes: +87MiB (+4.35%)
• 🟥 size/install//bytes: +19MiB (+0.64%)
• 🟥 size/libleanshared.so//bytes: +7MiB (+4.80%)

Medium changes (58✅, 1🟥)

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

Small changes (2028✅, 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 e09155b6f91642c2e50c3eb476823947200a90d0 --onto 43ef70db63e2c1c1720b84fd153125c96a00c5d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-19 13:31:59)

[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 e09155b6f91642c2e50c3eb476823947200a90d0 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-19 13:32:01)

[hargoniX]

!bench

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d13536b against e09155b are in. (These commits have already been benchmarked in a previous command.) There are significant results. @hargoniX

• ✅ build//instructions: -197.6G (-1.72%)

Large changes (13✅, 3🟥)

• ✅ compiled/deriv//instructions: -182.7M (-2.62%)
• ✅ compiled/hashmap//instructions: -40.6M (-1.20%)
• ✅ compiled/ilean_roundtrip//instructions: -378.1M (-1.61%)
• ✅ compiled/liasolver//instructions: -106.8M (-2.60%)
• ✅ compiled/parser//instructions: -143.3M (-0.41%)
• ✅ compiled/phashmap//instructions: -70.9M (-0.80%)
• ✅ compiled/rbmap//instructions: -177.3M (-2.09%)
• ✅ compiled/rbmap_checkpoint2//instructions: -78.0M (-0.87%)
• ✅ compiled/rbmap_fbip//instructions: -62.5M (-0.87%)
• 🟥 compiled/rbmap_library//instructions: +61.6M (+0.65%)
• ✅ compiled/unionfind//instructions: -376.6M (-1.39%)
• ✅ compiled/watchdogRss//instructions: -424.2M (-1.66%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -17.0M (-2.37%)
• ✅ elab/big_do//instructions: -453.0M (-2.06%)
• 🟥 size/compile/.out//bytes: +63MiB (+3.14%)
• 🟥 size/libleanshared.so//bytes: +5MiB (+3.56%)

Medium changes (53✅, 1🟥)

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

Small changes (1988✅)

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

[leanprover-radar]

Benchmark results for d13536b against e09155b are in. (These commits have already been benchmarked in a previous command.) There are significant results. @hargoniX

• ✅ build//instructions: -197.6G (-1.72%)

Large changes (13✅, 3🟥)

• ✅ compiled/deriv//instructions: -182.7M (-2.62%)
• ✅ compiled/hashmap//instructions: -40.6M (-1.20%)
• ✅ compiled/ilean_roundtrip//instructions: -378.1M (-1.61%)
• ✅ compiled/liasolver//instructions: -106.8M (-2.60%)
• ✅ compiled/parser//instructions: -143.3M (-0.41%)
• ✅ compiled/phashmap//instructions: -70.9M (-0.80%)
• ✅ compiled/rbmap//instructions: -177.3M (-2.09%)
• ✅ compiled/rbmap_checkpoint2//instructions: -78.0M (-0.87%)
• ✅ compiled/rbmap_fbip//instructions: -62.5M (-0.87%)
• 🟥 compiled/rbmap_library//instructions: +61.6M (+0.65%)
• ✅ compiled/unionfind//instructions: -376.6M (-1.39%)
• ✅ compiled/watchdogRss//instructions: -424.2M (-1.66%)
• ✅ compiled/workspaceSymbolsNewRanges//instructions: -17.0M (-2.37%)
• ✅ elab/big_do//instructions: -453.0M (-2.06%)
• 🟥 size/compile/.out//bytes: +63MiB (+3.14%)
• 🟥 size/libleanshared.so//bytes: +5MiB (+3.56%)

Medium changes (53✅, 1🟥)

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

Small changes (1988✅)

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