perf: share depth-invariant type class cache entries across `synthPendingDepth` by Kha · Pull Request #14298 · leanprover/lean4

Kha · 2026-07-06T20:20:59Z

The type class resolution cache is keyed by synthPendingDepth (issue #2522), which partitions the whole cache by depth even though the depth can only influence a query through the synthPending give-up check. Track whether a query ever reached a synthPending decision (via a non-backtrackable IO.Ref in Meta.Context, so discarded search branches still count); results of queries that never did are now cached with synthPendingDepth := none and shared across all depths. Depth-sensitive results remain keyed by their exact depth as before. The Meta.synthInstance.cache trace now includes the depth when it is nonzero.

Kha · 2026-07-06T20:21:05Z

!bench

Kha · 2026-07-06T20:21:09Z

!bench mathlib

leanprover-radar · 2026-07-06T20:21:11Z

Benchmark results for 888c16a against 41b2fe8 are in. No significant results found. @Kha

🟥 build//instructions: +8.0G (+0.07%)

Small changes (7✅, 4🟥)

✅ build/module/Init.Grind.Ordered.Field//instructions: -23.1M (-0.87%)
✅ build/module/Init.Grind.Ordered.Ring//instructions: -26.5M (-0.66%)
✅ build/module/Init.Grind.Ring.Field//instructions: -30.0M (-1.17%)
✅ build/module/Init.Internal.Order.Lemmas//instructions: -43.7M (-1.34%)
🟥 build/module/Lean.Elab.DocString//instructions: +79.0M (+0.18%)
🟥 build/module/Lean.Meta.Basic//instructions: +64.4M (+0.30%)
🟥 build/module/Lean.Meta.SynthInstance//instructions: +356.4M (+2.83%) (reduced significance based on *//lines)
🟥 elab/cbv_decide//instructions: +99.7M (+0.23%)
✅ vcgen/MatchIota/1000/kernel//wall-clock: -76ms (-17.35%)
✅ vcgen/MatchIota/1500/kernel//wall-clock: -188ms (-20.35%)
✅ vcgen/MatchIota/500/kernel//wall-clock: -17ms (-11.97%)

leanprover-radar · 2026-07-06T20:21:17Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@164b1c9 against leanprover-community/mathlib4-nightly-testing@ce52fd1 are in. There are significant results. @Kha

🟥 main exited with code 1

No significant changes detected.

leanprover-bot · 2026-07-06T20:58:11Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-03 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-06 20:58:11)
✅ Reference manual branch lean-pr-testing-14298 has successfully built against this PR. (2026-07-07 22:02:34) View Log
🟡 Reference manual branch lean-pr-testing-14298 build against this PR didn't complete normally. (2026-07-07 22:04:34) View Log
✅ Reference manual branch lean-pr-testing-14298 has successfully built against this PR. (2026-07-08 14:45:13) View Log
🟡 Reference manual branch lean-pr-testing-14298 build against this PR didn't complete normally. (2026-07-08 14:46:53) View Log
❗ 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 16:20:30)

mathlib-lean-pr-testing · 2026-07-06T21:51:31Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-14298 build failed against this PR. (2026-07-06 21:51:29) View Log
💥 Mathlib branch lean-pr-testing-14298 build failed against this PR. (2026-07-07 09:33:54) View Log
✅ Mathlib branch lean-pr-testing-14298 has successfully built against this PR. (2026-07-07 10:43:07) View Log
💥 Mathlib branch lean-pr-testing-14298 build failed against this PR. (2026-07-07 14:01:34) View Log
✅ Mathlib branch lean-pr-testing-14298 has successfully built against this PR. (2026-07-07 18:17:55) View Log
💥 Mathlib branch lean-pr-testing-14298 build failed against this PR. (2026-07-07 22:47:59) View Log
💥 Mathlib branch lean-pr-testing-14298 build failed against this PR. (2026-07-08 15:33:50) View Log

Kha · 2026-07-07T08:50:29Z

!bench mathlib

leanprover-radar · 2026-07-07T08:50:37Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@25a481d against leanprover-community/mathlib4-nightly-testing@8d815fe are in. There are significant results. @Kha

🟥 main exited with code 1

No significant changes detected.

Kha · 2026-07-07T09:45:42Z

!bench mathlib

leanprover-radar · 2026-07-07T09:45:50Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@bce7bc3 against leanprover-community/mathlib4-nightly-testing@8d815fe are in. There are significant results. @Kha

✅ build//instructions: -826.9G (-0.51%)

Large changes (1✅)

1 hidden

Medium changes (5✅)

✅ build/module/Mathlib.Algebra.Module.Equiv.Basic//instructions: -4.2G (-6.34%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -4.3G (-5.21%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -6.1G (-5.89%)
✅ build/module/Mathlib.Geometry.Manifold.ContMDiff.NormedSpace//instructions: -4.0G (-5.04%)
✅ build/module/Mathlib.RingTheory.QuasiFinite.Basic//instructions: -5.4G (-4.03%)

Small changes (98✅, 1🟥)

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

Kha · 2026-07-07T16:40:39Z

!bench

leanprover-radar · 2026-07-07T16:40:45Z

Benchmark results for 898391e against 41b2fe8 are in. No significant results found. @Kha

🟥 build//instructions: +8.6G (+0.08%)

Small changes (9✅, 2🟥)

✅ build/module/Init.Grind.Ordered.Field//instructions: -22.4M (-0.85%)
✅ build/module/Init.Grind.Ordered.Ring//instructions: -26.8M (-0.67%)
✅ build/module/Init.Grind.Ring.Basic//instructions: -36.8M (-0.57%)
✅ build/module/Init.Grind.Ring.Field//instructions: -27.6M (-1.08%)
✅ build/module/Init.Internal.Order.Lemmas//instructions: -42.1M (-1.29%)
🟥 build/module/Lean.Meta.Basic//instructions: +129.3M (+0.60%)
🟥 build/module/Lean.Meta.SynthInstance//instructions: +549.4M (+4.36%) (reduced significance based on *//lines)
✅ vcgen/GetThrowSet/200/kernel//wall-clock: -3ms (-6.12%)
✅ vcgen/MatchIota/1000/kernel//wall-clock: -70ms (-15.98%)
✅ vcgen/MatchIota/1500/kernel//wall-clock: -160ms (-17.32%)
✅ vcgen/MatchIota/500/kernel//wall-clock: -15ms (-10.56%)

Kha · 2026-07-07T17:15:23Z

!bench mathlib

leanprover-radar · 2026-07-07T17:15:31Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@fb458b8 against leanprover-community/mathlib4-nightly-testing@8d815fe are in. There are significant results. @Kha

✅ build//instructions: -1.3T (-0.78%)

Large changes (1✅)

1 hidden

Medium changes (16✅)

✅ build/module/Mathlib.Algebra.Module.Equiv.Basic//instructions: -4.3G (-6.40%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -3.7G (-6.12%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Bounds//instructions: -4.6G (-5.39%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Convolution//instructions: -5.3G (-6.57%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -8.7G (-8.84%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -7.6G (-9.31%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -6.1G (-5.86%)
✅ build/module/Mathlib.Analysis.Normed.Operator.Bilinear//instructions: -7.3G (-7.33%)
✅ build/module/Mathlib.Geometry.Manifold.ContMDiff.NormedSpace//instructions: -4.8G (-6.01%)
✅ build/module/Mathlib.Geometry.Manifold.MFDeriv.NormedSpace//instructions: -10.7G (-7.76%)
✅ build/module/Mathlib.RingTheory.DedekindDomain.LinearDisjoint//instructions: -5.9G (-3.44%)
✅ build/module/Mathlib.RingTheory.LocalRing.ResidueField.Fiber//instructions: -3.9G (-4.54%)
✅ build/module/Mathlib.RingTheory.QuasiFinite.Basic//instructions: -8.7G (-6.42%)
✅ build/module/Mathlib.RingTheory.QuasiFinite.Weakly//instructions: -3.1G (-4.93%)
✅ build/module/Mathlib.RingTheory.Spectrum.Prime.Polynomial//instructions: -3.0G (-7.06%)
✅ build/module/Mathlib.RingTheory.Unramified.LocalStructure//instructions: -6.6G (-4.03%)

Small changes (164✅)

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

Kha · 2026-07-08T14:11:12Z

!bench

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

Benchmark results for e7b4775 against 41b2fe8 are in. No significant results found. @Kha

🟥 build//instructions: +11.6G (+0.10%)

Small changes (9✅, 10🟥)

✅ build/module/Init.Grind.Ordered.Field//instructions: -23.3M (-0.88%)
✅ build/module/Init.Grind.Ordered.Ring//instructions: -30.9M (-0.77%)
✅ build/module/Init.Grind.Ring.Basic//instructions: -37.0M (-0.57%)
✅ build/module/Init.Grind.Ring.Field//instructions: -27.2M (-1.06%)
✅ build/module/Init.Internal.Order.Lemmas//instructions: -37.1M (-1.13%)
🟥 build/module/Lean.Elab.DocString//instructions: +86.0M (+0.20%)
🟥 build/module/Lean.Meta.Basic//instructions: +115.1M (+0.53%)
🟥 build/module/Lean.Meta.SynthInstance//instructions: +545.3M (+4.33%) (reduced significance based on *//lines)
🟥 build/profile/typeclass inference//wall-clock: +5s (+3.76%)
🟥 elab/bv_decide_realworld//wall-clock: +50ms (+4.38%)
🟥 elab/cbv_aes//task-clock: +174ms (+4.48%)
🟥 elab/cbv_aes//wall-clock: +145ms (+4.00%)
🟥 elab/cbv_decide//task-clock: +127ms (+3.08%)
🟥 elab/charactersIn//task-clock: +180ms (+10.36%)
🟥 elab/charactersIn//wall-clock: +181ms (+10.33%)
✅ vcgen/GetThrowSet/200/kernel//wall-clock: -3ms (-6.12%)
✅ vcgen/MatchIota/1000/kernel//wall-clock: -68ms (-15.53%)
✅ vcgen/MatchIota/1500/kernel//wall-clock: -163ms (-17.64%)
✅ vcgen/MatchIota/500/kernel//wall-clock: -13ms (-9.15%)

Kha · 2026-07-08T14:12:28Z

!bench mathlib

leanprover-radar · 2026-07-08T14:12:35Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@79f909f against leanprover-community/mathlib4-nightly-testing@8d815fe are in. There are significant results. @Kha

🟥 main exited with code 1

No significant changes detected.

…dingDepth` The type class resolution cache is keyed by `synthPendingDepth` (issue #2522), which partitions the whole cache by depth even though the depth can only influence a query through the `synthPending` give-up check. Track whether a query ever reached a `synthPending` decision (via a non-backtrackable `IO.Ref` in `Meta.Context`, so discarded search branches still count); results of queries that never did are now cached with `synthPendingDepth := none` and shared across all depths. Depth-sensitive results remain keyed by their exact depth as before. The `Meta.synthInstance.cache` trace now includes the depth when it is nonzero. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…epth Instead of a single depth-invariant class, each shared type class resolution cache entry now records the maximal `synthPendingDepth` (relative to the query) at which a `synthPending` decision was reached during synthesis, and is reused at any depth at which no such decision can reach the `maxSynthPendingDepth` give-up threshold. Only results whose synthesis actually hit the threshold remain keyed to their exact depth. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Drop `synthPendingDepth` from the type class resolution cache key: an entry now pairs an optional shared result (bounded by its relative `synthPending` activity depth) with an optional depth-exact result (from syntheses that hit the `maxSynthPendingDepth` give-up). Each query thus performs a single cache lookup, and both kinds of result for the same query can coexist without evicting each other. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Kha · 2026-07-08T15:10:40Z

!bench

Kha · 2026-07-08T15:10:51Z

!bench mathlib

leanprover-radar · 2026-07-08T15:11:00Z

Benchmark results for 8b0a880 against 1422c82 are in. No significant results found. @Kha

🟥 build//instructions: +10.9G (+0.10%)

Small changes (8✅, 3🟥)

✅ build/module/Init.Grind.Ordered.Field//instructions: -23.2M (-0.88%)
✅ build/module/Init.Grind.Ordered.Ring//instructions: -31.9M (-0.79%)
✅ build/module/Init.Grind.Ring.Basic//instructions: -43.0M (-0.66%)
✅ build/module/Init.Grind.Ring.Field//instructions: -27.5M (-1.07%)
✅ build/module/Init.Internal.Order.Lemmas//instructions: -44.9M (-1.37%)
🟥 build/module/Lean.Meta.Basic//instructions: +104.1M (+0.48%)
🟥 build/module/Lean.Meta.SynthInstance//instructions: +562.3M (+4.46%) (reduced significance based on *//lines)
✅ compiled/nat_repr//task-clock: -142ms (-10.50%)
✅ compiled/nat_repr//wall-clock: -142ms (-10.49%)
🟥 elab/bv_decide_realworld//wall-clock: +58ms (+5.13%)
✅ vcgen/MatchIota/1500/vcgen//wall-clock: -16ms (-7.88%)

leanprover-radar · 2026-07-08T15:11:01Z

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

🟥 main exited with code 1

No significant changes detected.

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 6, 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 6, 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 6, 2026

Kha pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 7, 2026

Update lean-toolchain for testing leanprover/lean4#14298

25a481d

Kha pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 7, 2026

Update lean-toolchain for testing leanprover/lean4#14298

bce7bc3

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

Kha force-pushed the tc-cache-opt branch from 888c16a to 898391e Compare July 7, 2026 12:21

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

Update lean-toolchain for leanprover/lean4#14298

15e030f

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

Update lean-toolchain for leanprover/lean4#14298

8fb2c99

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

Kha pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 7, 2026

Update lean-toolchain for leanprover/lean4#14298

fb458b8

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

Kha force-pushed the tc-cache-opt branch from 898391e to 0356412 Compare July 7, 2026 21:16

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

Update lean-toolchain for leanprover/lean4#14298

724670c

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

Update lean-toolchain for leanprover/lean4#14298

14fb5ce

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jul 7, 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 7, 2026

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

leanprover deleted a comment from leanprover-radar 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#14298

1743524

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

79f909f

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

Update lean-toolchain for leanprover/lean4#14298

0818aa7

Kha and others added 3 commits July 8, 2026 15:10

Kha force-pushed the tc-cache-opt branch from e7b4775 to 8b0a880 Compare July 8, 2026 15:10

Kha removed 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/batteries that referenced this pull request Jul 8, 2026

Update lean-toolchain for leanprover/lean4#14298

5418d1e

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

a7ee3d2

Uh oh!

Conversation

Kha commented Jul 6, 2026

Uh oh!

Kha commented Jul 6, 2026

Uh oh!

Kha commented Jul 6, 2026

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 7, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 7, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 7, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 7, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha 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!

Kha 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!

Kha commented Jul 8, 2026

Uh oh!

Kha 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 • 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 6, 2026 •

edited

Loading

leanprover-radar commented Jul 6, 2026 •

edited

Loading

leanprover-bot commented Jul 6, 2026 •

edited

Loading

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

edited

Loading

leanprover-radar commented Jul 7, 2026 •

edited

Loading

leanprover-radar commented Jul 7, 2026 •

edited

Loading

leanprover-radar commented Jul 7, 2026 •

edited

Loading

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