perf: cache inside matcher WHNFs at reducible/instances/implicit

[datokrat]

No description provided.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for b3f7fd4 against 1422c82 are in. There are significant results. @datokrat

• 🟥 build//instructions: +17.0G (+0.15%)

Large changes (2✅)

• ✅ build/module/Lake.Config.ConfigDecl//instructions: -8.4G (-62.87%)
• ✅ elab/cbv_decide//instructions: -3.9G (-9.11%)

Medium changes (2✅, 1🟥)

• ✅ elab/cbv_decide//task-clock: -255ms (-6.11%)
• ✅ elab/cbv_decide//wall-clock: -254ms (-6.11%)
• 🟥 elab/grind_list2//instructions: +430.4M (+0.96%)

Small changes (3✅, 96🟥)

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

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-08 12:18:59)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14323 build failed against this PR. (2026-07-08 13:03:44) View Log
• ✅ Mathlib branch lean-pr-testing-14323 has successfully built against this PR. (2026-07-08 16:58:05) View Log

[datokrat]

!radar

[leanprover-radar]

Benchmark results for f407c93 against 1422c82 are in. There are significant results. @datokrat

• ✅ build//instructions: -2.9G (-0.03%)

Large changes (2✅)

• ✅ build/module/Lake.Config.ConfigDecl//instructions: -8.5G (-63.01%)
• ✅ elab/cbv_decide//instructions: -3.9G (-9.20%)

Medium changes (2✅)

• ✅ elab/cbv_decide//task-clock: -267ms (-6.41%)
• ✅ elab/cbv_decide//wall-clock: -267ms (-6.42%)

Small changes (7✅, 2🟥)

• 🟥 build/module/Lean.Meta.Basic//instructions: +104.7M (+0.48%)
• ✅ build/module/Std.Do.WP.Monad//instructions: -23.7M (-0.90%)
• ✅ build/module/Std.Do.WP.SimpLemmas//instructions: -106.7M (-1.01%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Do.WP.Sound//instructions: -47.6M (-1.57%)
• ✅ build/module/Std.Time.Date.Unit.Month//instructions: -42.0M (-0.46%)
• ✅ compiled/nat_repr//task-clock: -122ms (-9.03%)
• ✅ compiled/nat_repr//wall-clock: -122ms (-9.04%)
• 🟥 elab/bv_decide_realworld//wall-clock: +59ms (+5.15%)
• ✅ vcgen/MatchIota/1500/vcgen//wall-clock: -13ms (-6.40%)

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 8dcde24 against 1422c82 are in. There are significant results. @datokrat

• ✅ build//instructions: -4.4G (-0.04%)

Large changes (2✅)

• ✅ build/module/Lake.Config.ConfigDecl//instructions: -8.5G (-63.05%)
• ✅ elab/cbv_decide//instructions: -4.0G (-9.29%)

Small changes (9✅, 3🟥)

• 🟥 build/module/Lean.Meta.Basic//instructions: +93.6M (+0.43%)
• ✅ build/module/Std.Do.WP.Monad//instructions: -22.1M (-0.84%)
• ✅ build/module/Std.Do.WP.SimpLemmas//instructions: -99.2M (-0.94%)
• ✅ build/module/Std.Do.WP.Sound//instructions: -41.8M (-1.38%)
• ✅ build/module/Std.Time.Date.Unit.Month//instructions: -36.3M (-0.40%)
• ✅ compiled/nat_repr//task-clock: -123ms (-9.09%)
• ✅ compiled/nat_repr//wall-clock: -122ms (-9.06%)
• 🟥 compiled/phashmap//task-clock: +37ms (+8.46%)
• 🟥 compiled/phashmap//wall-clock: +37ms (+8.53%)
• ✅ elab/cbv_decide//task-clock: -236ms (-5.67%)
• ✅ elab/cbv_decide//wall-clock: -240ms (-5.76%)
• ✅ vcgen/MatchIota/1500/vcgen//wall-clock: -14ms (-6.90%)