perf: type class experiment by leodemoura · Pull Request #14318 · leanprover/lean4

leodemoura · 2026-07-08T01:00:40Z

This PR is just an experiment for testing a modification in the type class resolution procedure. It tries to postpone some isDefEq tests at tryResolve. It addresses problematic cases such as trying to synthesize

AddRightCancel (Kernel α Ω)

using candidate

IsRightCancelAdd.toGrindAddRightCancel

This PR is just an experiment for testing a modification in the type class resolution procedure. It tries to postpone some `isDefEq` tests at `tryResolve`. It addresses problematic cases such as trying to synthesize ``` AddRightCancel (Kernel α Ω) ``` using candidate ``` IsRightCancelAdd.toGrindAddRightCancel ```

leodemoura · 2026-07-08T01:02:07Z

!bench

leanprover-radar · 2026-07-08T01:02:15Z

Benchmark results for 6679791 against 1422c82 are in. There are significant results. @leodemoura

✅ build//instructions: -47.5G (-0.42%)

Large changes (2✅, 2🟥)

✅ elab/cbv_decide//instructions: -2.0G (-4.63%)
✅ elab/grind_list2//instructions: -1.3G (-2.85%)
🟥 vcgen/AddSubCancelSimp/700/kernel//wall-clock: +26ms (+23.21%)
🟥 vcgen/AddSubCancelSimp/700/vcgen//wall-clock: +150ms (+15.59%)

Medium changes (7✅, 6🟥)

✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.3G (-1.21%)
✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -1.6G (-2.38%) (reduced significance based on absolute threshold)
✅ build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: -1.0G (-2.59%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: +2.7G (+4.66%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +1.3G (+6.40%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +4.7G (+5.09%) (reduced significance based on absolute threshold)
✅ elab/big_do//instructions: -59.0M (-0.31%)
🟥 elab/big_omega//instructions: +226.1M (+1.06%)
🟥 elab/big_omega_MT//instructions: +232.2M (+1.08%)
✅ elab/grind_bitvec2//instructions: -2.4G (-1.61%)
✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.0G (-1.49%)
🟥 vcgen/AddSubCancelSimp/400/vcgen//wall-clock: +80ms (+14.98%)
✅ vcgen/MatchIota/1500/vcgen//wall-clock: -19ms (-9.36%)

Small changes (511✅, 71🟥)

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

leodemoura · 2026-07-08T01:02:16Z

!bench mathlib

leanprover-radar · 2026-07-08T01:02:25Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@94e88be against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

🟥 main exited with code 1

No significant changes detected.

leanprover-bot · 2026-07-08T03:06:01Z

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 03:06:01)

mathlib-lean-pr-testing · 2026-07-08T03:26:36Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-14318 build failed against this PR. (2026-07-08 03:26:34) View Log
💥 Mathlib branch lean-pr-testing-14318 build failed against this PR. (2026-07-08 14:56:54) View Log
✅ Mathlib branch lean-pr-testing-14318 has successfully built against this PR. (2026-07-08 17:49:26) View Log

leodemoura · 2026-07-08T13:41:48Z

!bench

leodemoura · 2026-07-08T13:41:58Z

!bench mathlib

leanprover-radar · 2026-07-08T13:42:09Z

Benchmark results for 9f1bdd8 against 1422c82 are in. There are significant results. @leodemoura

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

Large changes (1✅)

✅ elab/cbv_decide//instructions: -2.0G (-4.59%)

Medium changes (11✅)

✅ build//instructions: -86.4G (-0.77%)
✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.83%)
✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.2G (-2.38%) (reduced significance based on absolute threshold)
✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.81%) (reduced significance based on absolute threshold)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.0G (-1.06%)
✅ build/module/Std.Data.Internal.List.Associative//instructions: -1.1G (-1.39%)
✅ build/profile/typeclass inference//wall-clock: -11s (-7.21%)
✅ elab/grind_bitvec2//instructions: -1.5G (-1.05%)
✅ elab/grind_list2//instructions: -688.6M (-1.54%)
✅ misc/import Init.Data.BitVec.Lemmas//instructions: -950.7M (-0.83%)
✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.1G (-1.61%)

and 1 hidden

Small changes (710✅, 3🟥)

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

leanprover-radar · 2026-07-08T13:42:09Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@94e88be against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. (These commits have already been benchmarked in a previous command.) There are significant results. @leodemoura

🟥 main exited with code 1

No significant changes detected.

leodemoura · 2026-07-08T13:54:50Z

!bench mathlib

leanprover-radar · 2026-07-08T13:54:58Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@e2f5e42 against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

🟥 main exited with code 1

No significant changes detected.

leodemoura · 2026-07-08T14:25:09Z

!bench mathlib

leanprover-radar · 2026-07-08T14:25:19Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@e2f5e42 against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. (These commits have already been benchmarked in a previous command.) There are significant results. @leodemoura

🟥 main exited with code 1

No significant changes detected.

leodemoura · 2026-07-08T15:46:28Z

!bench

leanprover-radar · 2026-07-08T15:53:16Z

Benchmark results for f0d26ed against 1422c82 are in. There are significant results. @leodemoura

✅ build//instructions: -85.3G (-0.76%)

Large changes (1✅)

✅ elab/cbv_decide//instructions: -2.0G (-4.57%)

Medium changes (10✅)

✅ build//instructions: -85.3G (-0.76%)
✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.83%)
✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.1G (-2.36%) (reduced significance based on absolute threshold)
✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.81%) (reduced significance based on absolute threshold)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.0G (-1.06%)
✅ build/module/Std.Data.Internal.List.Associative//instructions: -1.1G (-1.35%)
✅ elab/grind_bitvec2//instructions: -1.4G (-0.93%)
✅ elab/grind_list2//instructions: -629.2M (-1.41%)
✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.89%)
✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.1G (-1.64%)

and 1 hidden

Small changes (703✅, 5🟥)

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

leodemoura · 2026-07-08T16:39:29Z

!bench mathlib

leanprover-radar · 2026-07-08T16:39:37Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@e058bab against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

✅ build//instructions: -5.2T (-3.21%)

Large changes (2✅)

✅ build//instructions: -5.2T (-3.21%)
✅ build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: -19.7G (-16.52%)

and 1 hidden

Medium changes (230✅, 2🟥)

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

Small changes (1039✅, 2🟥)

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

leodemoura added the changelog-language Language features and metaprograms label Jul 8, 2026

leodemoura marked this pull request as draft July 8, 2026 01:00

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 8, 2026

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jul 8, 2026

mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 8, 2026

chore: fixes for Mathlib

9f1bdd8

leodemoura removed toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Jul 8, 2026

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 8, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 8, 2026

Update lean-toolchain for leanprover/lean4#14318

16bdbb1

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jul 8, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 8, 2026

Update lean-toolchain for leanprover/lean4#14318

e2f5e42

chore: another mathlib fix

f0d26ed

leodemoura removed the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 8, 2026

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 8, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 8, 2026

Update lean-toolchain for leanprover/lean4#14318

4c96345

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 8, 2026

Update lean-toolchain for leanprover/lean4#14318

e058bab

leodemoura mentioned this pull request Jul 8, 2026

perf: assign synthesized instances directly when the goal type is ground #14330

Merged

mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jul 8, 2026

Uh oh!

Conversation

leodemoura commented Jul 8, 2026

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

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

Uh oh!

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-bot commented Jul 8, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-radar commented Jul 8, 2026

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

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

Uh oh!

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

leanprover-radar commented Jul 8, 2026

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

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

Uh oh!

Uh oh!

leodemoura commented Jul 8, 2026

Uh oh!

leanprover-radar commented Jul 8, 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!

3 participants

leanprover-radar commented Jul 8, 2026 •

edited

Loading

leanprover-radar commented Jul 8, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Jul 8, 2026 •

edited

Loading

leanprover-radar commented Jul 8, 2026 •

edited

Loading

leanprover-radar commented Jul 8, 2026 •

edited

Loading

leanprover-radar commented Jul 8, 2026 •

edited

Loading

leanprover-radar commented Jul 8, 2026 •

edited

Loading