perf: consolidate all experimental typeclass inference optimisations by Kha · Pull Request #14339 · leanprover/lean4

Kha · 2026-07-09T13:38:11Z

No description provided.

Kha · 2026-07-09T13:38:27Z

!bench

leanprover-radar · 2026-07-09T13:38:37Z

Benchmark results for 61fc909 against da19ea0 are in. There are significant results. @Kha

✅ build//instructions: -273.4G (-2.46%)
🟥 other exited with code 1

Large changes (5✅)

✅ build//instructions: -273.4G (-2.46%)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -6.3G (-3.36%)
✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -7.3G (-12.55%)
✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -18.4G (-19.96%)
✅ build/profile/typeclass inference//wall-clock: -34s (-23.65%)

and 1 hidden

Medium changes (56✅)

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

Small changes (937✅, 14🟥)

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

Kha · 2026-07-09T14:12:48Z

!bench mathlib

leanprover-radar · 2026-07-09T14:13:11Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@742a28b against leanprover-community/mathlib4-nightly-testing@d87691e are in. There are significant results. @Kha

🟥 main exited with code 1

No significant changes detected.

leanprover-bot · 2026-07-09T14:17:02Z

Reference manual CI status:

✅ Reference manual branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-09 14:17:00) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-09 14:17:22) View Log
✅ Reference manual branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-09 16:41:50) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-09 16:43:41) View Log
✅ Reference manual branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-10 10:43:51) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-10 10:46:11) View Log
💥 Reference manual branch lean-pr-testing-14339 build failed against this PR. (2026-07-10 15:58:53) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-10 15:59:05) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-10 16:52:25) View Log
💥 Reference manual branch lean-pr-testing-14339 build failed against this PR. (2026-07-10 16:53:04) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-10 21:36:21) View Log
💥 Reference manual branch lean-pr-testing-14339 build failed against this PR. (2026-07-10 21:36:27) View Log
💥 Reference manual branch lean-pr-testing-14339 build failed against this PR. (2026-07-11 11:24:03) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-11 11:24:17) View Log
💥 Reference manual branch lean-pr-testing-14339 build failed against this PR. (2026-07-12 20:17:50) View Log
🟡 Reference manual branch lean-pr-testing-14339 build against this PR didn't complete normally. (2026-07-12 20:20:47) View Log

mathlib-lean-pr-testing · 2026-07-09T14:47:24Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-14339 build failed against this PR. (2026-07-09 14:47:22) View Log
✅ Mathlib branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-09 17:39:08) View Log
💥 Mathlib branch lean-pr-testing-14339 build failed against this PR. (2026-07-10 11:33:24) View Log
✅ Mathlib branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-10 16:52:10) View Log
✅ Mathlib branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-10 17:51:47) View Log
✅ Mathlib branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-10 22:28:45) View Log
✅ Mathlib branch lean-pr-testing-14339 has successfully built against this PR. (2026-07-11 12:13:48) View Log
💥 Mathlib branch lean-pr-testing-14339 build failed against this PR. (2026-07-12 21:04:27) View Log

Kha · 2026-07-09T15:44:32Z

!bench mathlib

leanprover-radar · 2026-07-09T15:49:06Z

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

🟥 main exited with code 1

No significant changes detected.

Kha · 2026-07-09T16:04:30Z

!bench mathlib

leanprover-radar · 2026-07-09T16:04:40Z

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

✅ build//instructions: -5.6T (-3.56%)

Large changes (26✅, 1🟥)

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

Medium changes (286✅, 1🟥)

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

Small changes (983✅, 3🟥)

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

Kha · 2026-07-10T09:53:28Z

!bench

Kha · 2026-07-10T09:53:35Z

!bench mathlib

leanprover-radar · 2026-07-10T09:53:37Z

Benchmark results for 922cb1f against da19ea0 are in. There are significant results. @Kha

✅ build//instructions: -322.0G (-2.90%)

Large changes (16✅)

✅ build//instructions: -322.0G (-2.90%)
✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -7.8G (-4.14%)
✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -7.4G (-12.59%)
✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -18.5G (-19.99%)
✅ build/profile/typeclass inference//wall-clock: -42s (-28.98%)
✅ compiled/incr_header_load//instructions: -447.7M (-38.42%)
✅ compiled/incr_header_load//maxrss: -59MiB (-9.45%)
✅ compiled/incr_header_load//wall-clock: -78ms (-52.53%)
✅ elab/big_omega//instructions: -2.1G (-10.05%)
✅ elab/big_omega_MT//instructions: -2.1G (-10.09%)
✅ elab/cbv_arm_ldst//instructions: -2.9G (-4.43%)
✅ elab/grind_bitvec2//instructions: -10.9G (-7.53%)
✅ elab/grind_list2//instructions: -3.7G (-8.58%)
✅ elab/riscv-ast//instructions: -4.9G (-5.48%)
✅ misc/import Init.Data.BitVec.Lemmas//instructions: -4.4G (-3.84%)
✅ vcgen/GetThrowSetGrind/200/vcgen//wall-clock: -29ms (-12.95%)

and 1 hidden

Medium changes (73✅, 2🟥)

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

Small changes (1029✅, 11🟥)

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

leanprover-radar · 2026-07-10T09:53:45Z

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

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Bench repo commit hashes for run main differ between commits.

🟥 main exited with code 1

No significant changes detected.

Kha · 2026-07-11T12:27:21Z

!bench mathlib

leanprover-radar · 2026-07-11T12:27:30Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@8998e87 against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. There are significant results. @Kha

✅ build//instructions: -10.6T (-6.99%)

Large changes (105✅)

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

Medium changes (662✅, 1🟥)

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

Small changes (1430✅, 2🟥)

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

Normalize the free variables of `.noMVars` type class resolution queries so that structurally identical queries in different local contexts can share a persistent cache entry. The free variables of the query type and `localInsts` are renamed to canonical positional variables for the cache key, and the result is stored abstracted over that closure as loose bound variables (`Expr.abstract`) and re-instantiated with the current context on a hit, analogously to how `abstractMVars` produces a closed schema. Checkpoint: on core algebra, order, and logic modules this cuts misses noticeably (e.g. `Algebra.Group.Basic` from 58% to 46%), but a `grind` instance-canonicalization regression in `Mathlib.Logic.Equiv.Prod` still needs fixing, where a reopened instance is not definitionally equal to a fresh synthesis. Set `LEAN_NO_FVAR_NORM=1` to disable it for A/B measurement. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

`SynthNorm.normExpr` and the `hasAnyFVar` escape check in `abstractOverClosure?` recursed over query terms as trees, so `.noMVars` queries whose types are heavily DAG-shared (as built by `grind`'s e-matching via substitution, e.g. nested `if`s in `Mathlib.Logic.Equiv.Prod`) burned exponential allocations, exhausting the heartbeat budget and failing `grind` with a deterministic `whnf` timeout. Memoize `normExpr` on `ExprStructEq`-keyed subterms (sound since canonical positions are assigned by first occurrence and never change) with a `hasFVar` fast path, and rewrite `abstractOverClosure?` to abstract first (DAG-cached in C++) and check the O(1) `hasFVar` flag of the result, keeping both linear in the DAG size of the query. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…tavariables This PR improves type class resolution cache reuse: instance queries whose local context mentions an already-solved metavariable now share a cache entry with structurally identical queries in other contexts, instead of falling back to a context-specific key. `SynthNorm.normExpr` gave up whenever a closure free variable's type satisfied `Expr.hasMVar`. That flag is syntactic and stays set for metavariables that are already assigned, whose values are context-free and normalize fine. Instantiate the type before deciding, and bail only on a metavariable that is still unassigned. On `Mathlib.Algebra.Group.Basic` this takes the number of queries that fall back to a raw key from 878 to 0: cache misses drop from 1676 to 1230, and the heartbeats spent inside missed searches drop by 35%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…normalization This PR speeds up type class resolution in contexts with many local instances, where normalizing the cache key dominated the cost of a cache lookup, including of the lookups that hit. The free-variable normalization runs on every `.noMVars` lookup, because its result *is* the key. Almost all of its cost is the closure of the local instances, which does not depend on the query: on `Mathlib.RingTheory.DedekindDomain.Different` it is 98% of the normalization, rebuilt on each of 84550 lookups over an average of 18 local instances. Normalize the local instances first, so their canonical positions do not depend on the query, and memoize the resulting closure in `Meta.Cache`. A memoized closure is reused while the local instances are unchanged and every closure variable whose type mentions a metavariable still instantiates to what the closure was built from; a `LocalDecl`'s type is otherwise immutable. Contexts that cannot be normalized memoize the failure, so they too cost a single lookup. The same file spends 62 heartbeats per normalization instead of 1587, a 25-fold reduction, with the closure served from the memo 98% of the time. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

This PR lets instance queries whose local context contains a `let` share a cache entry with structurally identical queries in other contexts, instead of falling back to a context-specific key. The free-variable normalization gave up on a let-bound closure variable, because its value is visible to definitional unfolding but was not part of the key. Record the normalized value alongside the normalized type, so that contexts agreeing on the types but not the values stay apart. A nondependent `ldecl` (a `have`) hides its value from unfolding and needs no value in the key. On `Mathlib.RingTheory.DedekindDomain.Different` this removes every let-induced fallback: the queries that fall back to a raw key drop from 32938 to 19192, cache misses from 15420 to 15023, and the heartbeats spent inside missed searches by 5.3%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Kha · 2026-07-12T19:01:42Z

!bench mathlib

leanprover-radar · 2026-07-12T19:01:52Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@8998e87 against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Kha

✅ build//instructions: -10.6T (-6.99%)

Large changes (104✅)

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

Medium changes (662✅, 1🟥)

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

Small changes (1424✅, 2🟥)

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

Kha · 2026-07-12T19:02:09Z

!bench mathlib

leanprover-radar · 2026-07-12T19:02:26Z

Benchmark results for leanprover-community/mathlib4-nightly-testing@a8784fe against leanprover-community/mathlib4-nightly-testing@5edfd4c are in. There are significant results. @Kha

✅ build//instructions: -10.6T (-7.04%)

Large changes (104✅)

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

Medium changes (673✅, 1🟥)

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

Small changes (1422✅, 1🟥)

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

Kha · 2026-07-23T11:47:34Z

!bench mathlib

leanprover-radar · 2026-07-23T11:48:00Z

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

✅ build//instructions: -10.6T (-7.04%)

Large changes (98✅)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -12.1G (-17.65%)
✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -13.8G (-31.33%)
✅ build/module/Mathlib.Algebra.Module.Torsion.PrimaryComponent//instructions: -29.5G (-44.85%)
✅ build/module/Mathlib.Algebra.MonoidAlgebra.PointwiseSMul//instructions: -12.1G (-49.74%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -9.0G (-16.99%)
✅ build/module/Mathlib.Algebra.Order.Monoid.Canonical.Basic//instructions: -10.5G (-33.88%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -21.3G (-27.76%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -19.0G (-34.05%)
✅ build/module/Mathlib.Algebra.Ring.CentroidHom//instructions: -9.0G (-26.25%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -27.6G (-25.76%)
✅ build/module/Mathlib.Algebra.TrivSqZeroExt.Basic//instructions: -12.8G (-17.77%)
✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap//instructions: -17.1G (-28.18%)
✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula//instructions: -57.1G (-35.08%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -50.3G (-41.33%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -23.2G (-45.42%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -21.6G (-42.03%)
✅ build/module/Mathlib.Analysis.Analytic.ChangeOrigin//instructions: -11.9G (-26.22%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -48.2G (-38.12%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -20.6G (-35.44%)
✅ build/module/Mathlib.Analysis.Analytic.Inverse//instructions: -14.6G (-19.11%)
and 77 more
and 1 hidden

Medium changes (639✅, 1🟥)

✅ build/module/Batteries.Data.BinomialHeap.Basic//instructions: -4.2G (-18.39%)
✅ build/module/Batteries.Data.List.Lemmas//instructions: -4.0G (-8.76%)
✅ build/module/Batteries.Data.Nat.Bisect//instructions: -3.3G (-24.02%) (reduced significance based on absolute threshold)
✅ build/module/Batteries.Data.String.Lemmas//instructions: -2.9G (-8.73%)
✅ build/module/Batteries.Recycling.RBTree.Lemmas//instructions: -3.8G (-11.22%)
✅ build/module/Batteries.Recycling.RBTree.WF//instructions: -4.8G (-14.26%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.4G (-14.68%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -4.5G (-16.66%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -5.9G (-11.05%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -4.0G (-11.86%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -4.1G (-31.62%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -2.9G (-12.14%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -6.6G (-14.04%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -6.8G (-12.53%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify//instructions: -6.5G (-12.15%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Sheaf.Free//instructions: -2.8G (-12.73%)
✅ build/module/Mathlib.Algebra.Colimit.Module//instructions: -3.5G (-10.72%)
✅ build/module/Mathlib.Algebra.ContinuedFractions.Computation.Approximations//instructions: -3.3G (-14.03%)
✅ build/module/Mathlib.Algebra.DirectSum.Internal//instructions: -5.0G (-13.25%)
✅ build/module/Mathlib.Algebra.DualQuaternion//instructions: -3.3G (-18.20%)
and 620 more

Small changes (1402✅, 1🟥)

✅ build/module/Aesop.Forward.State//instructions: -1.0G (-4.88%)
✅ build/module/Aesop.Saturate//instructions: -705.3M (-4.78%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -913.3M (-10.16%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -643.6M (-4.90%)
✅ build/module/Aesop.Search.Main//instructions: -389.5M (-3.78%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -500.0M (-8.52%)
✅ build/module/Aesop.Util.Basic//instructions: -791.3M (-9.56%)
✅ build/module/Batteries.Data.Array.Basic//instructions: -746.0M (-5.23%)
✅ build/module/Batteries.Data.Array.Merge//instructions: -418.2M (-7.27%)
✅ build/module/Batteries.Data.Fin.Basic//instructions: -352.5M (-10.72%)
✅ build/module/Batteries.Data.Fin.Coding//instructions: -460.8M (-3.49%)
✅ build/module/Batteries.Data.Fin.Lemmas//instructions: -491.6M (-5.99%)
✅ build/module/Batteries.Data.Random.MersenneTwister//instructions: -564.6M (-11.16%)
✅ build/module/Batteries.Data.String.Legacy//instructions: -333.5M (-6.81%)
✅ build/module/Batteries.Data.UnionFind.Basic//instructions: -1.2G (-9.13%)
✅ build/module/Batteries.Data.Vector.Basic//instructions: -683.3M (-8.36%)
✅ build/module/Batteries.Recycling.MonadSatisfying.Array//instructions: -733.8M (-7.53%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -532.2M (-4.30%)
✅ build/module/Batteries.Tactic.SqueezeScope//instructions: -714.3M (-8.25%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -2.4G (-9.59%)
and 1383 more

This PR lets an instance query whose class has output parameters share a cache entry with structurally identical queries in other local contexts, and persist across commands, as queries without metavariables already do. The free-variable normalization ran only on `.noMVars` queries, so every other key kept the free variables of the context that created it and could never be shared. Run it on all queries: metavariable identities are left exactly as they are, so only the free variables are canonicalized. The wildcard that `preprocess` puts in output-parameter positions is left alone, being a marker rather than a variable of the local context. The gate on persistence tested `.noMVars`, which is a proxy for what it actually requires: a key without metavariables. Test that directly. An `.mvarsOutputParams` key has its output parameters replaced by a wildcard, so it is metavariable-free whenever every metavariable sits in an output parameter, and is then as context-free as a `.noMVars` key: the wildcard stands for a value the input parameters determine, and a hit re-derives it by unifying the cached result against the query. On `Mathlib.Algebra.Group.Basic` the misses drop from 1230 to 944 and the heartbeats spent inside missed searches by 45%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

This PR fixes a slowdown in `grind` in the presence of the persistent type class resolution cache: a cached instance, reopened from an abstracted schema, is not maximally shared, so `grind` re-walked it on every `shareCommon` of a term containing it. `Sym.synthInstance?` now runs the synthesized instance through `Sym.shareCommon`, interning it into the local term store once, as `grind` already does for every other term it internalizes. Later `shareCommon` calls then find it shared by pointer. On `Mathlib.Logic.Equiv.Prod` this cuts elaboration from 93.7G to 43.1G instructions (the cost without the cache), with the alpha-hash-consing (`Sym.AlphaShareCommon`) share of runtime dropping from 28% back to near zero. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

github-actions Bot added 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 9, 2026

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

Kha force-pushed the push-nkopukwwvywz branch from 61fc909 to 623bf27 Compare July 9, 2026 15:44

Kha removed the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-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#14339

8134021

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

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

df4c7ab

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

Update lean-toolchain for leanprover/lean4#14339

410c8cf

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

Kha force-pushed the push-nkopukwwvywz branch from 623bf27 to 922cb1f Compare July 10, 2026 09:53

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

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

Update lean-toolchain for leanprover/lean4#14339

4d48278

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

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

Update lean-toolchain for leanprover/lean4#14339

8998e87

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

Update lean-toolchain for leanprover/lean4#14339

0913af8

Kha and others added 5 commits July 12, 2026 18:19

Kha force-pushed the push-nkopukwwvywz branch from 60acd8b to 6eac0c5 Compare July 12, 2026 19:01

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

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

Update lean-toolchain for leanprover/lean4#14339

f2de73e

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

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

Update lean-toolchain for leanprover/lean4#14339

a8784fe

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

Update lean-toolchain for leanprover/lean4#14339

8135582

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

Kha changed the title ~~[REBASED] experiment: consolidate all TC opts~~ perf: consolidate all TC opts Jul 23, 2026

Kha changed the base branch from nightly-with-mathlib to master July 23, 2026 11:50

Kha changed the title ~~perf: consolidate all TC opts~~ perf: consolidate all experimental typeclass inference optimisations Jul 23, 2026

Kha and others added 3 commits July 23, 2026 16:54

perf merge

38bd297

Kha force-pushed the push-nkopukwwvywz branch from 6eac0c5 to 7df05c9 Compare July 23, 2026 17:04

Conversation

Kha commented Jul 9, 2026

Uh oh!

Kha commented Jul 9, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 9, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-bot commented Jul 9, 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 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 9, 2026

Uh oh!

leanprover-radar commented Jul 9, 2026

Uh oh!

Kha commented Jul 9, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 10, 2026

Uh oh!

Kha commented Jul 10, 2026

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 11, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 12, 2026

Uh oh!

leanprover-radar commented Jul 12, 2026

Uh oh!

Kha commented Jul 12, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 23, 2026

Uh oh!

leanprover-radar commented Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-radar commented Jul 9, 2026 •

edited

Loading

leanprover-radar commented Jul 9, 2026 •

edited

Loading

leanprover-bot commented Jul 9, 2026 •

edited

Loading

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

edited

Loading

leanprover-radar commented Jul 9, 2026 •

edited

Loading

leanprover-radar commented Jul 10, 2026 •

edited

Loading

leanprover-radar commented Jul 10, 2026 •

edited

Loading

leanprover-radar commented Jul 11, 2026 •

edited

Loading

leanprover-radar commented Jul 12, 2026 •

edited

Loading