perf: use a cache in hasAssignableMVar

[JovanGerb]

This PR lets hasAssignableMVar traverse the given expression with a cache, rather than traversing the expression entirely. This is an important performance fix, because the current slowest declaration in mathlib (in Mathlib.Algebra.Category.ModuleCat.Stalk) spends more that half the time running hasAssignableMVar.

The mathlib speedup is -332.4G (-0.19%)

See also #13037

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 06073c5 against 90b5e31 are in. There are no significant changes. @JovanGerb

• ✅ build//instructions: -1.3G (-0.01%)

Medium changes (1✅)

• ✅ interpreted/identifier_completion//instructions: -1.2G (-1.60%)

Small changes (7✅, 1🟥)

• ✅ build/module/Lean.Meta.AppBuilder//instructions: -138.8M (-1.48%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.LevelDefEq//instructions: -51.7M (-2.09%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Contradiction//instructions: -149.3M (-2.62%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.MatchCond//instructions: -561.2M (-3.19%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Simp.Main//instructions: -325.0M (-1.52%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Simp.Rewrite//instructions: -342.9M (-1.83%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.MetavarContext//instructions: -464.2M (-4.43%) (reduced significance based on absolute threshold)
• 🟥 compiled/rbmap_checkpoint//instructions: +2.8M (+0.02%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-19-rev1 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-03-22 12:49:24)

[JovanGerb]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@e161197 against leanprover-community/mathlib4-nightly-testing@5a62ef1 are in. There are no significant changes. @JovanGerb

• 🟥 build//instructions: +48.2G (+0.03%)

Medium changes (1🟥)

• 🟥 build/module/Mathlib.Algebra.Category.ModuleCat.Stalk//instructions: +12.3G (+4.76%)

Small changes (2✅, 4🟥)

• ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated//instructions: -1.9G (-3.68%)
• 🟥 build/module/Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax//instructions: +3.4G (+3.65%)
• 🟥 build/module/Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo//instructions: +4.8G (+6.70%)
• 🟥 build/module/Mathlib.CategoryTheory.FiberedCategory.Grothendieck//instructions: +836.9M (+3.81%)
• 🟥 build/module/Mathlib.Lean.Elab.Term//instructions: +253.1M (+11.23%)
• ✅ build/module/Mathlib.RingTheory.Morita.Matrix//instructions: -2.3G (-2.07%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13036 has successfully built against this PR. (2026-03-22 13:45:01) View Log

[JovanGerb]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@8529154 against leanprover-community/mathlib4-nightly-testing@5a62ef1 are in. Significant changes detected! @JovanGerb

• ✅ build//instructions: -332.4G (-0.19%)

Large changes (4✅)

• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Stalk//instructions: -188.0G (-72.71%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo//instructions: -25.9G (-36.12%)
• ✅ build/module/Mathlib.CategoryTheory.FiberedCategory.Grothendieck//instructions: -5.3G (-24.16%)
• ✅ build/module/Mathlib.RingTheory.Morita.Matrix//instructions: -23.8G (-21.83%)

Medium changes (6✅)

• ✅ build/module/Mathlib.Algebra.Exact//instructions: -5.6G (-10.84%)
• ✅ build/module/Mathlib.Algebra.Lie.Extension//instructions: -11.9G (-10.33%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor//instructions: -11.8G (-17.56%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax//instructions: -17.0G (-18.40%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor//instructions: -12.3G (-23.42%)
• ✅ build/module/Mathlib.CategoryTheory.Sites.Hypercover.One//instructions: -32.5G (-23.61%)

Small changes (7✅, 1🟥)

• ✅ build/module/Mathlib.AlgebraicGeometry.Cover.Directed//instructions: -2.2G (-6.67%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated//instructions: -2.0G (-3.87%)
• ✅ build/module/Mathlib.CategoryTheory.Action.Basic//instructions: -1.2G (-3.89%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.Functor.Lax//instructions: -5.7G (-14.40%)
• 🟥 build/module/Mathlib.CategoryTheory.HomCongr//instructions: +401.0M (+6.02%)
• ✅ build/module/Mathlib.CategoryTheory.Thin//instructions: -537.6M (-10.18%)
• ✅ build/module/Mathlib.Geometry.RingedSpace.PresheafedSpace//instructions: -1.2G (-2.66%)
• ✅ build/profile/C code generation//wall-clock: -61ms (-0.54%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13036 has successfully built against this PR. (2026-03-22 16:08:21) View Log