perf: assign synthesized instances directly when the goal type is ground by leodemoura · Pull Request #14330 · leanprover/lean4

leodemoura · 2026-07-08T17:34:06Z

This PR makes tryResolve assign the goal metavariable directly after successfully unifying the goal type with the candidate instance type, instead of re-checking the types with isDefEq. The recheck is redundant for metavariable-free goals and can be expensive.

This PR makes `tryResolve` assign the goal metavariable directly after successfully unifying the goal type with the candidate instance type, instead of re-checking the types with `isDefEq`. The recheck is redundant for metavariable-free goals and can be expensive.

leodemoura · 2026-07-08T17:36:11Z

The experiment in #14318 was successful, but I need to clean up the PR and break it into smaller pieces. This is the first PR.

leodemoura · 2026-07-08T17:36:30Z

!bench

leanprover-radar · 2026-07-08T17:36:36Z

Benchmark results for 669b426 against e90c70f are in. There are significant results. @leodemoura

✅ build//instructions: -94.1G (-0.84%)

Large changes (1✅)

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

Medium changes (9✅)

✅ build//instructions: -94.1G (-0.84%)
✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.85%)
✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.2G (-2.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.93%) (reduced significance based on absolute threshold)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.2G (-1.14%)
✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -1.0G (-1.54%) (reduced significance based on absolute threshold)
✅ elab/grind_bitvec2//instructions: -2.2G (-1.48%)
✅ elab/grind_list2//instructions: -867.2M (-1.95%)
✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.90%)

and 1 hidden

Small changes (757✅, 1🟥)

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

leodemoura · 2026-07-08T17:36:45Z

!bench mathlib

leanprover-radar · 2026-07-08T17:36:51Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@aa69f08 against leanprover-community/mathlib4-nightly-testing@55b60c6 are in. There are significant results. @leodemoura

✅ build//instructions: -5.9T (-3.66%)

Large changes (3✅)

✅ build//instructions: -5.9T (-3.66%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -17.3G (-16.66%)
✅ build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: -21.4G (-18.01%)

and 1 hidden

Medium changes (312✅)

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

Small changes (1129✅)

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

leanprover-bot · 2026-07-08T18:08:04Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-08 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 18:08:04)
✅ Reference manual branch lean-pr-testing-14330 has successfully built against this PR. (2026-07-08 22:57:40) View Log
🟡 Reference manual branch lean-pr-testing-14330 build against this PR didn't complete normally. (2026-07-08 22:58:53) View Log
✅ Reference manual branch lean-pr-testing-14330 has successfully built against this PR. (2026-07-09 00:06:54) View Log
🟡 Reference manual branch lean-pr-testing-14330 build against this PR didn't complete normally. (2026-07-09 00:08:20) View Log

mathlib-lean-pr-testing · 2026-07-08T19:09:08Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-14330 has successfully built against this PR. (2026-07-08 19:09:06) View Log
💥 Mathlib branch lean-pr-testing-14330 build failed against this PR. (2026-07-08 23:18:59) View Log
✅ Mathlib branch lean-pr-testing-14330 has successfully built against this PR. (2026-07-09 01:06:42) View Log

Falsified by tests/elab/12172_regression.lean: MeasurableSpace-style classes are deliberately multi-instance, and eager synthesis commits goal metavariables that unification must determine later.

The previous commit's message is inaccurate: it describes an earlier experiment (synthesizing pending class metavariables at synthInstance entry) that was abandoned because it broke tests/elab/12172_regression.lean. What the commit actually implements is the final design: tryResolve assigns the synthesized instance directly (no recheck, no guard) and explicitly synthesizes the goal-type class metavariables that unification left undetermined (synthPendingClassMVars). This commit moves the accompanying repro from tests/leo/ (not run by ctest) into tests/elab/ and updates its docstring to describe the current code. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

leodemoura · 2026-07-08T22:30:51Z

!bench

leanprover-radar · 2026-07-08T22:30:58Z

Benchmark results for 0eb00fd against e90c70f are in. There are significant results. @leodemoura

🟥 build exited with code 1
🟥 other exited with code 1

No significant changes detected.

leodemoura · 2026-07-08T22:31:22Z

!bench mathlib

leanprover-radar · 2026-07-08T22:31:30Z

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

✅ build//instructions: -5.9T (-3.66%)

Large changes (3✅)

✅ build//instructions: -5.9T (-3.66%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -17.3G (-16.66%)
✅ build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: -21.4G (-18.01%)

and 1 hidden

Medium changes (312✅)

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

Small changes (1129✅)

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

This PR restores the `isDefEq mvar instVal` recheck at the end of `tryResolve` for goals whose type bodies contain metavariables, keeping direct assignment only for metavariable-free goals, and documents why the recheck is load-bearing. The recheck's unification side effects synthesize pending class metavariables in the goal (e.g. `IsPredArchimedean ι ?pre ?pd`, created when elaborating class projections) via `isDefEqArgs`'s `trySynthPending` pass. The synthesized set depends on how the two compared types are spelled, so it cannot be recomputed after a direct assignment: synthesizing all pending class metavariables breaks stage2 (a higher-order `[Nonempty ε]` metavariable in `Init/Internal/Order/Basic.lean` must be left to unification), and synthesizing none breaks Mathlib (`Mathlib/Order/SuccPred/LinearLocallyFinite.lean`). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

leodemoura · 2026-07-08T23:36:25Z

!bench

leanprover-radar · 2026-07-08T23:36:31Z

Benchmark results for 7d378d7 against e90c70f are in. There are significant results. @leodemoura

✅ build//instructions: -94.5G (-0.84%)

Large changes (1✅)

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

Medium changes (11✅)

✅ build//instructions: -94.5G (-0.84%)
✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.1G (-0.89%)
✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.2G (-2.47%) (reduced significance based on absolute threshold)
✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.2G (-2.95%) (reduced significance based on absolute threshold)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.1G (-1.12%)
✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -1.0G (-1.53%) (reduced significance based on absolute threshold)
✅ build/profile/typeclass inference//wall-clock: -13s (-8.48%)
✅ elab/grind_bitvec2//instructions: -2.2G (-1.50%)
✅ elab/grind_list2//instructions: -859.0M (-1.93%)
✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.1G (-0.91%)
✅ misc/import Std.Data.Internal.List.Associative//instructions: -979.9M (-1.42%)

and 1 hidden

Small changes (755✅)

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

leodemoura · 2026-07-08T23:36:54Z

!bench mathlib

leanprover-radar · 2026-07-08T23:37:01Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@541fcad against leanprover-community/mathlib4-nightly-testing@55b60c6 are in. There are significant results. @leodemoura

✅ build//instructions: -6.0T (-3.68%)

Large changes (3✅)

✅ build//instructions: -6.0T (-3.68%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -17.2G (-16.59%)
✅ build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: -21.5G (-18.10%)

and 1 hidden

Medium changes (312✅)

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

Small changes (1132✅)

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

…und (#14330) This PR makes `tryResolve` assign the goal metavariable directly after successfully unifying the goal type with the candidate instance type, instead of re-checking the types with `isDefEq`. The recheck is redundant for metavariable-free goals and can be expensive. --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

leodemoura added the changelog-language Language features and metaprograms 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

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

leodemoura added this pull request to the merge queue Jul 8, 2026

leodemoura removed this pull request from the merge queue due to a manual request Jul 8, 2026

mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 8, 2026

leodemoura and others added 2 commits July 8, 2026 22:14

wip: synthesize pending class mvars at synthInstance entry

cb7dee0

Falsified by tests/elab/12172_regression.lean: MeasurableSpace-style classes are deliberately multi-instance, and eager synthesis commits goal metavariables that unification must determine later.

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#14330

70f1125

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#14330

af3f41e

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jul 8, 2026

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

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 9, 2026

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

Update lean-toolchain for leanprover/lean4#14330

e2b121b

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

Update lean-toolchain for leanprover/lean4#14330

541fcad

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 9, 2026

Update lean-toolchain for leanprover/lean4#14330

c8a4127

leodemoura added this pull request to the merge queue Jul 9, 2026

Merged via the queue into master with commit da19ea0 Jul 9, 2026
22 checks passed

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 9, 2026

Uh oh!

Conversation

leodemoura commented Jul 8, 2026

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!

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 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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!

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!

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!

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

leanprover-bot 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