refactor: new LRAT checker by hargoniX · Pull Request #14842 · leanprover/lean4

hargoniX · 2026-08-19T15:00:42Z

No description provided.

hargoniX · 2026-08-19T15:00:49Z

!bench

leanprover-radar · 2026-08-19T15:00:57Z

Benchmark results for c18ef71 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -117.5G (-1.02%)

Large changes (17✅)

✅ build/profile/grind ematch//wall-clock: -483ms (-91.57%)
✅ build/profile/grind mark subsingleton//wall-clock: -437ms (-92.49%)
✅ build/profile/grind simp//wall-clock: -2s (-89.50%)
✅ build/profile/grind//wall-clock: -3s (-88.77%)
✅ build/profile/sym canon//wall-clock: -459ms (-91.35%)
✅ build/profile/sym typeclass inference//wall-clock: -524ms (-83.65%)
✅ elab/bv_decide_mod//instructions: -15.5G (-7.89%)
✅ elab/bv_decide_mul//instructions: -8.5G (-26.32%)
✅ elab/bv_decide_mul//maxrss: -79MiB (-8.17%)
✅ elab/bv_decide_mul//task-clock: -354ms (-15.40%)
✅ elab/bv_decide_realworld//instructions: -5.8G (-12.15%)
✅ elab/bv_decide_realworld//task-clock: -329ms (-10.10%)
✅ elab/bv_stress_replicate//instructions: -951.6M (-5.81%)
✅ elab/sym_let_to_have_nested//maxrss: -14MiB (-0.74%)
✅ size/all/.ilean//bytes: -772kiB (-0.91%)
✅ size/all/.olean.private//bytes: -10MiB (-0.74%)
✅ size/all/.olean//bytes: -2MiB (-0.66%)

Medium changes (13✅, 2🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-90.95%)
✅ build/stat/imported consts//amount: -975.4k (-1.15%)
🟥 elab/bv_decide_inequality//instructions: +3.2G (+6.62%)
🟥 elab/bv_decide_inequality//task-clock: +305ms (+7.65%)
✅ elab/bv_decide_large_aig//maxrss: -16MiB (-1.06%)
✅ elab/bv_decide_mul//wall-clock: -380ms (-16.10%)
✅ elab/charactersIn//instructions: -161.8M (-0.51%)
✅ elab/delayed_lift//maxrss: -16MiB (-0.91%)
✅ elab/delayed_sharing//maxrss: -15MiB (-0.83%)
✅ elab/let_to_have_chain//maxrss: -12MiB (-0.67%)
✅ elab/let_to_have_closed_body//maxrss: -14MiB (-0.80%)
✅ elab/lift_lets_parallel//maxrss: -15MiB (-0.85%)
✅ elab/string_simp_ne//maxrss: -15MiB (-0.81%)
✅ elab/sym_let_to_have_chain//maxrss: -14MiB (-0.79%)
✅ size/install//bytes: -14MiB (-0.44%)

Small changes (62✅, 4🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -58.0M (-1.31%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -38.0M (-1.98%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -55.1M (-1.67%)
✅ build/module/Lean.Elab.Tactic//instructions: -39.8M (-3.03%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -24.4M (-1.80%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -52.1M (-2.19%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -53.0M (-6.91%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.8M (-2.78%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -49.3M (-1.56%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -44.8M (-0.86%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.3M (-4.37%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -44.9M (-2.87%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -41.2M (-2.11%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -41.4M (-2.53%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -42.6M (-2.41%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -41.1M (-0.57%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -41.3M (-2.41%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -48.1M (-4.86%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -44.6M (-4.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -37.1M (-3.22%) (reduced significance based on absolute threshold)
and 45 more
and 1 hidden

hargoniX · 2026-08-19T15:17:47Z

!bench

leanprover-radar · 2026-08-19T15:18:01Z

Benchmark results for 8fe2aec against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -117.0G (-1.02%)

Large changes (17✅)

✅ build/profile/grind ematch//wall-clock: -484ms (-91.64%)
✅ build/profile/grind mark subsingleton//wall-clock: -438ms (-92.73%)
✅ build/profile/grind simp//wall-clock: -2s (-89.93%)
✅ build/profile/grind//wall-clock: -3s (-88.80%)
✅ build/profile/sym canon//wall-clock: -460ms (-91.64%)
✅ build/profile/sym typeclass inference//wall-clock: -522ms (-83.22%)
✅ elab/bv_decide_mod//instructions: -15.5G (-7.87%)
✅ elab/bv_decide_mul//instructions: -8.5G (-26.29%)
✅ elab/bv_decide_mul//maxrss: -77MiB (-7.97%)
✅ elab/bv_decide_mul//task-clock: -348ms (-15.11%)
✅ elab/bv_decide_realworld//instructions: -5.8G (-12.10%)
✅ elab/bv_decide_realworld//task-clock: -310ms (-9.51%)
✅ elab/bv_stress_replicate//instructions: -947.3M (-5.78%)
✅ elab/sym_let_to_have_nested//maxrss: -13MiB (-0.72%)
✅ size/all/.ilean//bytes: -771kiB (-0.91%)
✅ size/all/.olean.private//bytes: -10MiB (-0.74%)
✅ size/all/.olean//bytes: -2MiB (-0.66%)

Medium changes (12✅, 2🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-91.18%)
✅ build/stat/imported consts//amount: -975.4k (-1.15%)
🟥 elab/bv_decide_inequality//instructions: +3.2G (+6.68%)
🟥 elab/bv_decide_inequality//task-clock: +292ms (+7.33%)
✅ elab/bv_decide_large_aig//maxrss: -15MiB (-1.01%)
✅ elab/bv_decide_mul//wall-clock: -374ms (-15.86%)
✅ elab/charactersIn//instructions: -158.7M (-0.50%)
✅ elab/delayed_sharing//maxrss: -14MiB (-0.77%)
✅ elab/let_to_have_chain//maxrss: -13MiB (-0.72%)
✅ elab/let_to_have_closed_body//maxrss: -14MiB (-0.76%)
✅ elab/lift_lets_parallel//maxrss: -14MiB (-0.79%)
✅ elab/string_simp_ne//maxrss: -13MiB (-0.72%)
✅ elab/sym_let_to_have_chain//maxrss: -14MiB (-0.74%)
✅ size/install//bytes: -14MiB (-0.44%)

Small changes (61✅, 4🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -58.5M (-1.32%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -37.6M (-1.96%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -55.1M (-1.67%)
✅ build/module/Lean.Elab.Tactic//instructions: -40.3M (-3.07%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -25.4M (-1.87%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -49.6M (-2.09%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -51.7M (-6.74%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.6M (-2.77%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -46.8M (-1.48%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -44.4M (-0.85%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.6M (-4.40%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -43.9M (-2.81%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -37.4M (-1.92%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -43.3M (-2.65%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -42.2M (-2.38%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -39.4M (-0.54%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -42.2M (-2.46%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -45.9M (-4.63%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -46.9M (-4.70%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -37.9M (-3.29%) (reduced significance based on absolute threshold)
and 44 more
and 1 hidden

hargoniX · 2026-08-21T19:20:39Z

!bench

leanprover-radar · 2026-08-21T19:20:45Z

Benchmark results for f5b6dae against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -97.3G (-0.85%)

Large changes (9✅, 10🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-90.90%)
✅ build/profile/grind ematch//wall-clock: -484ms (-91.78%)
✅ build/profile/grind mark subsingleton//wall-clock: -436ms (-92.39%)
✅ build/profile/grind simp//wall-clock: -2s (-89.95%)
✅ build/profile/grind//wall-clock: -3s (-88.72%)
✅ build/profile/sym canon//wall-clock: -458ms (-91.22%)
🟥 elab/bv_decide_inequality//instructions: +11.9G (+24.57%)
🟥 elab/bv_decide_inequality//task-clock: +951ms (+23.84%)
🟥 elab/bv_decide_inequality//wall-clock: +921ms (+22.60%)
🟥 elab/bv_decide_mod//instructions: +125.3G (+63.70%)
🟥 elab/bv_decide_mod//task-clock: +8s (+38.71%)
🟥 elab/bv_decide_mod//wall-clock: +8s (+38.70%)
🟥 elab/bv_decide_mul//instructions: +3.7G (+11.50%)
✅ elab/bv_decide_mul//maxrss: -70MiB (-7.28%)
🟥 elab/bv_decide_mul//task-clock: +663ms (+28.79%)
🟥 elab/bv_decide_mul//wall-clock: +631ms (+26.74%)
🟥 elab/bv_decide_realworld//instructions: +2.8G (+5.87%)
✅ size/all/.ilean//bytes: -624kiB (-0.73%)
✅ size/all/.olean.private//bytes: -9MiB (-0.65%)

Medium changes (8✅, 3🟥)

✅ build/profile/sym typeclass inference//wall-clock: -519ms (-82.77%)
✅ elab/big_beq_rec//maxrss: -16MiB (-0.87%)
✅ elab/big_deceq_rec//maxrss: -14MiB (-0.79%)
🟥 elab/bv_decide_realworld//task-clock: +200ms (+6.15%)
🟥 elab/bv_stress_replicate//instructions: +1.8G (+11.18%)
🟥 elab/bv_stress_replicate//wall-clock: +82ms (+8.47%)
✅ elab/charactersIn//instructions: -154.1M (-0.49%)
✅ elab/let_to_have_closed_body//maxrss: -13MiB (-0.74%)
✅ elab/string_simp_ne//maxrss: -12MiB (-0.65%)
✅ size/all/.lean//lines: -3.8k (-0.53%)
✅ size/all/.olean//bytes: -2MiB (-0.56%)

Small changes (54✅, 4🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -56.2M (-1.27%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -29.8M (-1.55%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -54.9M (-1.67%)
✅ build/module/Lean.Elab.Tactic//instructions: -40.9M (-3.11%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -36.0M (-2.66%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -73.8M (-3.11%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -74.0M (-9.64%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.7M (-2.77%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -47.2M (-1.50%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -44.0M (-0.85%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.2M (-4.36%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -44.1M (-2.82%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -41.0M (-2.10%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -42.3M (-2.59%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -43.2M (-2.44%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -43.8M (-0.60%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -40.9M (-2.38%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -45.3M (-4.57%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -44.6M (-4.48%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -37.1M (-3.23%) (reduced significance based on absolute threshold)
and 37 more
and 1 hidden

hargoniX · 2026-08-21T20:01:00Z

!bench

leanprover-radar · 2026-08-21T20:01:09Z

Benchmark results for 6a77bdf against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -98.2G (-0.85%)

Large changes (10✅, 6🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-90.84%)
✅ build/profile/grind ematch//wall-clock: -483ms (-91.42%)
✅ build/profile/grind mark subsingleton//wall-clock: -436ms (-92.44%)
✅ build/profile/grind simp//wall-clock: -2s (-89.64%)
✅ build/profile/grind//wall-clock: -3s (-88.47%)
✅ build/profile/sym canon//wall-clock: -457ms (-90.91%)
🟥 elab/bv_decide_inequality//instructions: +7.1G (+14.58%)
🟥 elab/bv_decide_inequality//task-clock: +531ms (+13.31%)
🟥 elab/bv_decide_inequality//wall-clock: +507ms (+12.44%)
🟥 elab/bv_decide_mod//instructions: +13.7G (+6.97%)
🟥 elab/bv_decide_mod//task-clock: +1s (+8.51%)
🟥 elab/bv_decide_mod//wall-clock: +1s (+8.69%)
✅ elab/bv_decide_mul//instructions: -3.5G (-10.63%)
✅ elab/bv_decide_mul//maxrss: -69MiB (-7.14%)
✅ size/all/.ilean//bytes: -624kiB (-0.73%)
✅ size/all/.olean.private//bytes: -8MiB (-0.65%)

Medium changes (5✅)

✅ build/profile/sym typeclass inference//wall-clock: -518ms (-82.67%)
✅ elab/charactersIn//instructions: -155.4M (-0.49%)
✅ elab/let_to_have_closed_body//maxrss: -12MiB (-0.66%)
✅ size/all/.lean//lines: -3.8k (-0.53%)
✅ size/all/.olean//bytes: -2MiB (-0.56%)

Small changes (55✅, 3🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -60.6M (-1.37%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -36.5M (-1.90%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -53.2M (-1.62%)
✅ build/module/Lean.Elab.Tactic//instructions: -41.2M (-3.14%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -35.4M (-2.61%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -74.0M (-3.11%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -73.9M (-9.63%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.6M (-2.77%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -46.3M (-1.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -43.9M (-0.84%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.9M (-4.43%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -42.1M (-2.69%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -40.4M (-2.07%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -42.7M (-2.61%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -37.8M (-2.13%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -38.8M (-0.54%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -41.8M (-2.44%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -45.6M (-4.60%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -44.7M (-4.49%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -38.3M (-3.32%) (reduced significance based on absolute threshold)
and 37 more
and 1 hidden

hargoniX · 2026-08-21T20:32:04Z

!bench

leanprover-radar · 2026-08-21T20:32:11Z

Benchmark results for a7b78c6 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -97.3G (-0.85%)

Large changes (10✅, 6🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-89.79%)
✅ build/profile/grind ematch//wall-clock: -483ms (-91.42%)
✅ build/profile/grind mark subsingleton//wall-clock: -437ms (-92.53%)
✅ build/profile/grind simp//wall-clock: -2s (-89.51%)
✅ build/profile/grind//wall-clock: -3s (-88.76%)
✅ build/profile/sym canon//wall-clock: -460ms (-91.60%)
🟥 elab/bv_decide_inequality//instructions: +6.9G (+14.34%)
🟥 elab/bv_decide_inequality//task-clock: +540ms (+13.54%)
🟥 elab/bv_decide_inequality//wall-clock: +516ms (+12.67%)
🟥 elab/bv_decide_mod//instructions: +12.9G (+6.54%)
🟥 elab/bv_decide_mod//task-clock: +1s (+8.67%)
🟥 elab/bv_decide_mod//wall-clock: +1s (+8.88%)
✅ elab/bv_decide_mul//instructions: -3.6G (-11.04%)
✅ elab/bv_decide_mul//maxrss: -69MiB (-7.08%)
✅ size/all/.ilean//bytes: -634kiB (-0.75%)
✅ size/all/.olean.private//bytes: -9MiB (-0.65%)

Medium changes (6✅)

✅ build/profile/sym typeclass inference//wall-clock: -529ms (-84.40%)
✅ elab/bv_stress_replicate//instructions: -734.9M (-4.49%)
✅ elab/charactersIn//instructions: -157.2M (-0.50%)
✅ elab/let_to_have_closed_body//maxrss: -12MiB (-0.65%)
✅ size/all/.lean//lines: -3.8k (-0.53%)
✅ size/all/.olean//bytes: -2MiB (-0.56%)

Small changes (51✅, 4🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -57.6M (-1.30%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -36.9M (-1.92%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -54.7M (-1.66%)
✅ build/module/Lean.Elab.Tactic//instructions: -40.5M (-3.08%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -37.3M (-2.75%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -74.3M (-3.13%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -73.2M (-9.54%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.6M (-2.77%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -47.6M (-1.51%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -43.4M (-0.84%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -44.4M (-4.49%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -44.6M (-2.85%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -41.4M (-2.12%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -44.0M (-2.69%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -42.8M (-2.42%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -43.7M (-0.60%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -42.0M (-2.45%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -45.4M (-4.59%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -45.2M (-4.53%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -39.5M (-3.43%) (reduced significance based on absolute threshold)
and 34 more
and 1 hidden

hargoniX · 2026-08-21T21:26:07Z

!bench

leanprover-radar · 2026-08-21T21:26:15Z

Benchmark results for 43771c4 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -97.3G (-0.85%)

Large changes (8✅, 2🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-89.76%)
✅ build/profile/grind ematch//wall-clock: -484ms (-91.66%)
✅ build/profile/grind mark subsingleton//wall-clock: -437ms (-92.62%)
✅ build/profile/grind simp//wall-clock: -2s (-90.06%)
✅ build/profile/grind//wall-clock: -3s (-89.22%)
✅ build/profile/sym canon//wall-clock: -460ms (-91.61%)
🟥 compiled/rbmap_checkpoint//instructions: +964.9M (+7.60%)
🟥 elab/bv_decide_mul//instructions: +531.4M (+1.64%)
✅ size/all/.ilean//bytes: -634kiB (-0.75%)
✅ size/all/.olean.private//bytes: -9MiB (-0.65%)

Medium changes (8✅)

✅ build/profile/sym typeclass inference//wall-clock: -530ms (-84.57%)
✅ elab/bv_decide_inequality//instructions: -1.0G (-2.08%)
✅ elab/bv_decide_realworld//instructions: -1.1G (-2.31%)
✅ elab/bv_stress_replicate//instructions: -715.3M (-4.37%)
✅ elab/charactersIn//instructions: -153.9M (-0.49%)
✅ elab/let_to_have_closed_body//maxrss: -12MiB (-0.67%)
✅ size/all/.lean//lines: -3.8k (-0.53%)
✅ size/all/.olean//bytes: -2MiB (-0.56%)

Small changes (55✅, 8🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -57.2M (-1.29%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -38.3M (-2.00%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -55.4M (-1.68%)
✅ build/module/Lean.Elab.Tactic//instructions: -39.5M (-3.00%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -35.5M (-2.62%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -73.4M (-3.09%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -73.6M (-9.59%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -43.2M (-2.68%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -46.7M (-1.48%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -42.8M (-0.82%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.3M (-4.37%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -43.2M (-2.76%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -40.8M (-2.09%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -43.4M (-2.66%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -40.7M (-2.30%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -42.8M (-0.59%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -42.1M (-2.45%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -42.7M (-4.32%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -45.0M (-4.52%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -38.9M (-3.38%) (reduced significance based on absolute threshold)
and 42 more
and 1 hidden

hargoniX · 2026-08-21T21:43:55Z

!bench

leanprover-radar · 2026-08-21T21:44:10Z

Benchmark results for 82f0876 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -93.6G (-0.81%)

Large changes (11✅, 9🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-91.51%)
✅ build/profile/grind ematch//wall-clock: -486ms (-91.98%)
✅ build/profile/grind mark subsingleton//wall-clock: -437ms (-92.51%)
✅ build/profile/grind simp//wall-clock: -2s (-89.84%)
✅ build/profile/grind//wall-clock: -3s (-88.88%)
✅ build/profile/sym canon//wall-clock: -460ms (-91.58%)
🟥 compiled/rbmap_checkpoint//instructions: +1.4G (+11.14%)
🟥 elab/bv_decide_inequality//instructions: +10.5G (+21.73%)
🟥 elab/bv_decide_inequality//task-clock: +671ms (+16.83%)
🟥 elab/bv_decide_inequality//wall-clock: +644ms (+15.81%)
🟥 elab/bv_decide_large_aig//instructions: +6.4G (+18.25%)
✅ elab/bv_decide_large_aig//maxrss: -186MiB (-12.27%)
🟥 elab/bv_decide_mod//instructions: +24.6G (+12.51%)
🟥 elab/bv_decide_mod//task-clock: +2s (+10.74%)
🟥 elab/bv_decide_mod//wall-clock: +2s (+10.80%)
✅ elab/bv_decide_mul//instructions: -1.3G (-3.98%)
✅ elab/bv_decide_mul//maxrss: -67MiB (-6.95%)
🟥 elab/bv_decide_realworld//instructions: +4.7G (+9.74%)
✅ size/all/.ilean//bytes: -608kiB (-0.72%)
✅ size/all/.olean.private//bytes: -8MiB (-0.62%)

Medium changes (5✅, 3🟥)

✅ build/profile/sym typeclass inference//wall-clock: -519ms (-82.76%)
🟥 compiled/rbmap_checkpoint//task-clock: +181ms (+12.27%)
🟥 compiled/rbmap_checkpoint//wall-clock: +185ms (+12.51%)
🟥 elab/bv_decide_large_aig//task-clock: +202ms (+6.00%)
✅ elab/charactersIn//instructions: -141.2M (-0.45%)
✅ elab/let_to_have_closed_body//maxrss: -11MiB (-0.64%)
✅ size/all/.lean//lines: -3.6k (-0.51%)
✅ size/all/.olean//bytes: -2MiB (-0.51%)

Small changes (50✅, 7🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -56.2M (-1.27%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -38.9M (-2.03%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -51.5M (-1.56%)
✅ build/module/Lean.Elab.Tactic//instructions: -40.0M (-3.05%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -36.5M (-2.69%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -74.3M (-3.13%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -72.8M (-9.48%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -43.8M (-2.72%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -48.0M (-1.52%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -48.4M (-0.93%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -43.9M (-4.44%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -43.5M (-2.78%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -40.0M (-2.05%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -43.5M (-2.66%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -40.5M (-2.28%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -43.4M (-0.60%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -41.1M (-2.40%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -42.6M (-4.30%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -45.0M (-4.51%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -38.1M (-3.31%) (reduced significance based on absolute threshold)
and 36 more
and 1 hidden

hargoniX · 2026-08-21T23:03:21Z

!bench

leanprover-radar · 2026-08-21T23:03:44Z

Benchmark results for 0d81801 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -93.1G (-0.81%)

Large changes (9✅, 6🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-89.32%)
✅ build/profile/grind ematch//wall-clock: -482ms (-91.32%)
✅ build/profile/grind mark subsingleton//wall-clock: -438ms (-92.68%)
✅ build/profile/grind simp//wall-clock: -2s (-90.19%)
✅ build/profile/grind//wall-clock: -3s (-89.04%)
✅ build/profile/sym canon//wall-clock: -460ms (-91.65%)
🟥 compiled/nat_repr//task-clock: +1s (+88.30%)
🟥 compiled/nat_repr//wall-clock: +1s (+88.32%)
🟥 elab/bv_decide_large_aig//instructions: +6.2G (+17.78%)
✅ elab/bv_decide_large_aig//maxrss: -171MiB (-11.31%)
🟥 elab/bv_decide_mod//instructions: +10.1G (+5.13%)
🟥 elab/bv_decide_mul//instructions: +2.6G (+8.06%)
🟥 elab/bv_decide_realworld//instructions: +2.4G (+4.94%)
✅ size/all/.ilean//bytes: -606kiB (-0.71%)
✅ size/all/.olean.private//bytes: -8MiB (-0.62%)

Medium changes (7✅, 3🟥)

✅ build/profile/sym typeclass inference//wall-clock: -527ms (-84.05%)
🟥 compiled/nat_repr//instructions: +11.1M (+0.03%)
🟥 elab/bv_decide_inequality//instructions: +796.6M (+1.64%)
🟥 elab/bv_decide_large_aig//task-clock: +239ms (+7.09%)
✅ elab/charactersIn//instructions: -148.5M (-0.47%)
✅ elab/delayed_sharing//maxrss: -13MiB (-0.74%)
✅ elab/let_to_have_closed_body//maxrss: -15MiB (-0.83%)
✅ elab/string_simp_ne//maxrss: -13MiB (-0.71%)
✅ size/all/.lean//lines: -3.6k (-0.50%)
✅ size/all/.olean//bytes: -2MiB (-0.52%)

Small changes (58✅, 5🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -56.8M (-1.29%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -40.4M (-2.11%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -54.1M (-1.64%)
✅ build/module/Lean.Elab.Tactic//instructions: -40.7M (-3.10%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -34.9M (-2.57%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -74.0M (-3.12%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -73.4M (-9.56%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -44.3M (-2.74%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -48.2M (-1.53%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -46.9M (-0.90%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -42.6M (-4.30%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -44.6M (-2.85%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -41.5M (-2.13%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -43.2M (-2.64%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -40.9M (-2.31%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -41.6M (-0.57%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -41.9M (-2.44%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -43.2M (-4.36%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -44.1M (-4.42%)
✅ build/module/Lean.Meta.Tactic//instructions: -38.9M (-3.38%) (reduced significance based on absolute threshold)
and 42 more
and 1 hidden

hargoniX · 2026-08-22T09:16:27Z

!bench

leanprover-radar · 2026-08-22T09:16:35Z

Benchmark results for eead1ff against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -88.3G (-0.77%)

Large changes (44✅, 8🟥)

✅ build/profile/grind dsimp//wall-clock: -3ms (-91.87%)
✅ build/profile/grind ematch//wall-clock: -487ms (-92.26%)
✅ build/profile/grind mark subsingleton//wall-clock: -438ms (-92.83%)
✅ build/profile/grind simp//wall-clock: -2s (-89.08%)
✅ build/profile/grind//wall-clock: -3s (-89.21%)
✅ build/profile/sym canon//wall-clock: -459ms (-91.46%)
🟥 compiled/binarytrees//instructions: +95.5M (+0.17%)
🟥 compiled/const_fold//instructions: +718.4M (+10.01%)
🟥 compiled/deriv//instructions: +208.8M (+3.17%)
✅ compiled/incr_header_save//maxrss: -34MiB (-1.62%)
🟥 compiled/rbmap_checkpoint//instructions: +5.8G (+45.43%)
🟥 compiled/rbmap_checkpoint//task-clock: +840ms (+57.08%)
🟥 compiled/rbmap_checkpoint//wall-clock: +882ms (+59.63%)
✅ elab/big_beq//maxrss: -55MiB (-3.08%)
✅ elab/big_beq_rec//maxrss: -60MiB (-3.30%)
✅ elab/big_deceq//maxrss: -55MiB (-3.08%)
✅ elab/big_deceq_rec//maxrss: -56MiB (-3.16%)
✅ elab/big_match//maxrss: -55MiB (-3.02%)
✅ elab/big_match_nat//maxrss: -55MiB (-3.11%)
✅ elab/big_match_nat_split//maxrss: -56MiB (-3.09%)
and 32 more

Medium changes (5✅, 3🟥)

✅ build/profile/sym typeclass inference//wall-clock: -520ms (-82.99%)
🟥 compiled/const_fold//task-clock: +150ms (+13.83%)
🟥 compiled/const_fold//wall-clock: +151ms (+13.89%)
🟥 elab/bv_decide_large_aig//wall-clock: +384ms (+11.37%)
✅ elab/cbv_decide//maxrss: -57MiB (-3.11%)
✅ elab/charactersIn//instructions: -141.8M (-0.45%)
✅ size/all/.lean//lines: -3.5k (-0.49%)
✅ size/all/.olean//bytes: -2MiB (-0.50%)

Small changes (41✅, 5🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -55.4M (-1.25%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -39.5M (-2.06%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -54.1M (-1.64%)
✅ build/module/Lean.Elab.Tactic//instructions: -39.4M (-3.00%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -36.8M (-2.71%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -74.0M (-3.11%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -72.6M (-9.46%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -45.3M (-2.81%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -46.4M (-1.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -46.7M (-0.90%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -44.3M (-4.48%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -45.3M (-2.90%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -40.6M (-2.08%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -42.1M (-2.57%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -42.2M (-2.38%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -44.1M (-0.61%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -41.5M (-2.42%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -43.0M (-4.34%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -46.3M (-4.65%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -38.2M (-3.32%) (reduced significance based on absolute threshold)
and 25 more
and 1 hidden

hargoniX · 2026-08-22T09:49:23Z

!bench

leanprover-radar · 2026-08-22T09:50:02Z

Benchmark results for 7f90729 against e4be9b5 are in. There are significant results. @hargoniX

✅ build//instructions: -91.0G (-0.79%)

Large changes (12✅)

✅ build/profile/grind dsimp//wall-clock: -3ms (-89.29%)
✅ build/profile/grind ematch//wall-clock: -483ms (-91.55%)
✅ build/profile/grind mark subsingleton//wall-clock: -436ms (-92.38%)
✅ build/profile/grind simp//wall-clock: -2s (-89.71%)
✅ build/profile/grind//wall-clock: -3s (-88.66%)
✅ build/profile/sym canon//wall-clock: -459ms (-91.48%)
✅ elab/bv_decide_inequality//instructions: -1.5G (-3.14%)
✅ elab/bv_decide_large_aig//maxrss: -65MiB (-4.28%)
✅ elab/bv_decide_mul//instructions: -429.5M (-1.32%)
✅ elab/bv_decide_realworld//instructions: -2.4G (-5.00%)
✅ size/all/.ilean//bytes: -585kiB (-0.69%)
✅ size/all/.olean.private//bytes: -8MiB (-0.60%)

Medium changes (4✅, 1🟥)

✅ build/profile/sym typeclass inference//wall-clock: -519ms (-82.83%)
✅ elab/charactersIn//instructions: -140.5M (-0.45%)
🟥 interpreted/identifier_completion//instructions: +649.7M (+0.98%)
✅ size/all/.lean//lines: -3.5k (-0.48%)
✅ size/all/.olean//bytes: -2MiB (-0.50%)

Small changes (52✅, 5🟥)

✅ build/module/Lean.Elab.Tactic.BVDecide//instructions: -54.0M (-1.22%)
✅ build/module/Lean.Elab.Tactic.Cbv//instructions: -39.5M (-2.06%)
✅ build/module/Lean.Elab.Tactic.Grind.BVDecide//instructions: -55.2M (-1.67%)
✅ build/module/Lean.Elab.Tactic//instructions: -39.5M (-3.01%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab//instructions: -36.8M (-2.71%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT.Cert//instructions: -73.6M (-3.10%)
✅ build/module/Lean.Meta.Tactic.BVDecide.LRAT//instructions: -73.4M (-9.56%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: -45.4M (-2.82%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Basic//instructions: -49.3M (-1.57%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover.Bitblast//instructions: -47.4M (-0.91%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Prover//instructions: -44.3M (-4.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr//instructions: -42.7M (-2.73%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVLogical//instructions: -39.6M (-2.03%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVPred//instructions: -43.1M (-2.63%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: -42.0M (-2.37%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.Reify//instructions: -43.0M (-0.59%)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect.SatAtBVLogical//instructions: -40.9M (-2.39%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: -44.4M (-4.48%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic.BVDecide//instructions: -45.8M (-4.59%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Meta.Tactic//instructions: -38.1M (-3.31%) (reduced significance based on absolute threshold)
and 36 more
and 1 hidden

hargoniX force-pushed the hbv/new_lrat branch from c18ef71 to 8fe2aec Compare August 19, 2026 15:17

hargoniX force-pushed the hbv/new_lrat branch 2 times, most recently from 5110bd3 to f5b6dae Compare August 21, 2026 19:20

hargoniX force-pushed the hbv/new_lrat branch from f5b6dae to 6a77bdf Compare August 21, 2026 20:00

hargoniX force-pushed the hbv/new_lrat branch from 6a77bdf to a7b78c6 Compare August 21, 2026 20:31

hargoniX force-pushed the hbv/new_lrat branch from a7b78c6 to 43771c4 Compare August 21, 2026 21:26

hargoniX force-pushed the hbv/new_lrat branch from 82f0876 to 0d81801 Compare August 21, 2026 23:03

hargoniX force-pushed the hbv/new_lrat branch from 0d81801 to eead1ff Compare August 22, 2026 09:16

hargoniX force-pushed the hbv/new_lrat branch from eead1ff to 7f90729 Compare August 22, 2026 09:49

hargoniX force-pushed the hbv/new_lrat branch from 7f90729 to ad0dcd6 Compare August 22, 2026 12:49

hargoniX force-pushed the hbv/new_lrat branch from ad0dcd6 to a6da351 Compare August 24, 2026 09:12

hargoniX added 5 commits August 25, 2026 07:49

feat: more SAT API

9d95769

refactor: new LRAT checker

76748fd

refactor: tricks in the rup checker

ab5cc5c

perf: compact literal representation

08c2fdd

feat: RAT component

3d84d06

hargoniX force-pushed the hbv/new_lrat branch from a6da351 to 3d84d06 Compare August 25, 2026 14:27

Uh oh!

Conversation

hargoniX commented Aug 19, 2026

Uh oh!

hargoniX commented Aug 19, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 19, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 21, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 22, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented Aug 22, 2026

Uh oh!

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

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

leanprover-radar commented Aug 19, 2026 •

edited

Loading

leanprover-radar commented Aug 19, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 21, 2026 •

edited

Loading

leanprover-radar commented Aug 22, 2026 •

edited

Loading

leanprover-radar commented Aug 22, 2026 •

edited

Loading