perf: no need to specialize the debugging slow path

[hargoniX]

No description provided.

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for e709b2f against dd28f00 are in! @hargoniX

Major changes (40)

• 🟥 Init.Data.BitVec.Lemmas re-elab//instructions: +184.9G (+21.7%)
• 🟥 Init.Data.BitVec.Lemmas//instructions: +42.2G (+26.3%)
• 🟥 Init.Data.List.Basic re-elab//instructions: +29.0G (+16.7%)
• 🟥 Init.Data.List.Sublist async//instructions: +3.5G (+27.3%)
• 🟥 Init.Data.List.Sublist re-elab -j4 (watchdog rss)//instructions: +38.5G (+20.0%)
• 🟥 Init.Data.List.Sublist re-elab -j4//instructions: +97.3G (+26.6%)
• 🟥 Init.Prelude async//instructions: +2.1G (+15.9%)
• 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +40.6G (+15.6%)
• 🟥 Std.Data.Internal.List.Associative//instructions: +29.2G (+32.2%)
• 🟥 big_beq//instructions: +854.1M (+7.1%)
• 🟥 big_beq_rec//instructions: +1.1G (+5.2%)
• 🟥 big_deceq//instructions: +342.3M (+6.4%)
• 🟥 big_deceq_rec//instructions: +537.3M (+7.2%)
• 🟥 big_do//instructions: +1.5G (+4.7%)
• 🟥 big_match//instructions: +372.8M (+3.0%)
• 🟥 big_match_partial//instructions: +1.5G (+8.4%)
• 🟥 big_omega.lean MT//instructions: +4.5G (+16.2%)
• 🟥 big_omega.lean//instructions: +4.5G (+16.3%)
• 🟥 build//instructions: +2.2T (+16.2%)
• 🟥 bv_decide_realworld//instructions: +760.0M (+2.9%)
• 🟥 bv_decide_rewriter.lean//instructions: +6.0G (+31.4%)
• 🟥 grind_bitvec2.lean//instructions: +75.3G (+36.0%)
• 🟥 grind_list2.lean//instructions: +31.0G (+47.2%)
• 🟥 grind_ring_5.lean//instructions: +345.9M (+3.6%)
• 🟥 iterators (elab)//instructions: +411.4M (+10.8%)
• 🟥 iterators (interpreted)//instructions: +411.7M (+1.2%)
• 🟥 lake config elab//instructions: +313.6M (+9.7%)
• 🟥 mut_rec_wf//instructions: +3.3G (+10.2%)
• 🟥 omega_stress.lean async//instructions: +608.4M (+11.3%)
• 🟥 reduceMatch//instructions: +2.0G (+10.7%)
• 🟥 riscv-ast.lean//instructions: +19.8G (+14.2%)
• 🟥 simp_arith1//instructions: +137.1M (+4.2%)
• 🟥 simp_bubblesort_256//instructions: +9.3G (+59.1%)
• 🟥 simp_congr//instructions: +2.6G (+13.3%)
• 🟥 simp_local//instructions: +50.5G (+83.4%)
• 🟥 simp_subexpr//instructions: +9.3G (+57.6%)
• 🟥 size/all/.c//lines: +1.6M (+14.2%)
• 🟥 size/all/.ir//bytes: +50MiB (+15.3%)
• 🟥 size/libleanshared.so//bytes: +22MiB (+11.5%)
• 🟥 tests/compiler//sum binary sizes: +185.9M (+10.1%)

Minor changes (5)

• 🟥 bv_decide_inequality.lean//instructions: +803.7M (+0.7%)
• 🟥 lake startup//instructions: +1.7M (+0.6%)
• 🟥 language server startup//instructions: +2.5M (+0.5%)
• 🟥 size/all/.olean.private//bytes: +5MiB (+0.5%)
• 🟥 tests/bench/ interpreted//instructions: +1.8G (+0.8%)

[hargoniX]

Guess there is a need 🙃