perf: experiment: separate defeq/whnf kernel diagnostics

[nomeata]

No description provided.

[nomeata]

!radar

[leanprover-radar]

Benchmark results for a4409f9 against ec60620 are in! @nomeata

• ✅ build//instructions: -591.4M (-0.00%)

Large changes (2✅, 2🟥)

• ✅ Init.Data.BitVec.Lemmas//instructions: -1.6G (-1.29%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: +18.5G (+71.04%)
• ✅ leanchecker --fresh Init//instructions: -9.9G (-2.97%)
• 🟥 mut_rec_wf//instructions: +375.1M (+1.32%)

Medium changes (7✅)

• ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.6G (-1.19%)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv//instructions: -1.3G (-9.85%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: -1.0G (-5.47%) (reduced significance based on absolute threshold)
• ✅ grind_bitvec2.lean//instructions: -1.2G (-0.59%)
• ✅ grind_ring_5.lean//instructions: -92.6M (-1.02%)
• ✅ omega_stress.lean async//instructions: -55.1M (-1.18%)
• ✅ simp_arith1//instructions: -85.3M (-3.25%)

Small changes (108✅, 12🟥)

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

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 1564e99 against ec60620 are in! @nomeata

• ✅ build//instructions: -243.3M (-0.00%)

Large changes (3✅, 2🟥)

• ✅ Init.Data.BitVec.Lemmas//instructions: -1.6G (-1.26%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: +18.5G (+71.02%)
• ✅ grind_ring_5.lean//instructions: -93.2M (-1.03%)
• ✅ leanchecker --fresh Init//instructions: -10.1G (-3.03%)
• 🟥 mut_rec_wf//instructions: +383.2M (+1.35%)

Medium changes (5✅)

• ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.5G (-1.17%)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv//instructions: -1.3G (-9.91%) (reduced significance based on absolute threshold)
• ✅ grind_bitvec2.lean//instructions: -1.2G (-0.58%)
• ✅ omega_stress.lean async//instructions: -51.2M (-1.10%)
• ✅ simp_arith1//instructions: -84.9M (-3.23%)

Small changes (111✅, 9🟥)

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-02-01 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-02-04 11:31:18)