[#14369] perf: normalize free variables in the type class resolution cache key by downstream-lean4[bot] · Pull Request #15 · leanprover/downstream-lean4

downstream-lean4 · 2026-07-24T14:27:57Z

This is the adaptation PR for leanprover/lean4#14369.

Kha · 2026-07-24T14:32:36Z

!bench mathlib

leanprover-radar · 2026-07-24T14:32:41Z

Benchmark results for 19e564b against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -6.9T (-4.82%)

Large changes (52✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.6G (-20.43%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -7.5G (-14.87%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -19.8G (-27.21%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -12.2G (-25.82%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.2G (-24.76%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -44.0G (-38.64%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -19.2G (-41.28%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -19.0G (-40.21%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -42.3G (-36.12%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.9G (-33.34%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -19.2G (-28.28%)
✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity//instructions: -19.3G (-19.77%)
✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances//instructions: -15.9G (-20.43%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -18.5G (-28.56%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -45.6G (-42.24%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -40.1G (-33.39%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -42.9G (-37.90%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Basic//instructions: -14.4G (-27.32%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Comp//instructions: -15.5G (-34.69%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -22.0G (-27.50%)
and 32 more
and 1 hidden

Medium changes (356✅, 1🟥)

✅ build/lakeprof/longest build path//instructions: -564.5G (-12.45%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -4.1G (-16.08%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.8G (-16.62%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.8G (-9.52%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.4G (-10.51%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.01%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.6G (-12.29%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify//instructions: -5.4G (-10.70%)
✅ build/module/Mathlib.Algebra.DirectSum.Internal//instructions: -3.5G (-9.72%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.7G (-7.07%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.2G (-15.53%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.1G (-12.34%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.6G (-11.66%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.3G (-14.26%)
✅ build/module/Mathlib.Algebra.Lie.Submodule//instructions: -5.2G (-9.42%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.9G (-11.12%)
✅ build/module/Mathlib.Algebra.Lie.Weights.IsSimple//instructions: -4.5G (-6.62%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Killing//instructions: -8.8G (-10.90%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -7.8G (-12.57%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.5G (-11.45%)
and 337 more

Small changes (1047✅, 6🟥)

✅ build/module/Aesop.Saturate//instructions: -571.4M (-3.98%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -791.5M (-9.12%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -498.7M (-3.90%)
✅ build/module/Aesop.Search.Main//instructions: -404.5M (-4.01%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -425.0M (-7.48%)
✅ build/module/Batteries.Data.List.Lemmas//instructions: -1.6G (-3.95%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -406.0M (-3.39%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.9G (-8.10%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.95%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.6G (-4.16%)
✅ build/module/Mathlib.Algebra.Algebra.Hom//instructions: -700.3M (-3.60%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.5G (-5.85%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Lattice//instructions: -1.2G (-3.03%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.5G (-6.80%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.59%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.4G (-8.77%)
✅ build/module/Mathlib.Algebra.BigOperators.Expect//instructions: -1.2G (-6.27%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -3.2G (-6.52%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -2.8G (-5.62%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.91%)
and 1033 more

leanprover-radar · 2026-07-24T14:32:44Z

This command can only be used in the lean4 repository.

_{You can edit the original message until the command succeeds.}

downstream-lean4 · 2026-07-24T15:58:56Z

Build report for downstream: follow upstream PR

Stayed red

Repo	Critical	Build	Test	Lint
verso-slides		🟥 in 0m	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 0m	✅ in 0m	⏭️
batteries	✅	✅ in 0m	✅ in 0m	✅ in 0m
import-graph	✅	✅ in 0m	✅ in 0m	⏭️
lean4-cli	✅	✅ in 0m	✅ in 0m	⏭️
mathlib4	✅	✅ in 19m	✅ in 1m	✅ in 1m
plausible	✅	✅ in 0m	✅ in 0m	⏭️
ProofWidgets4	✅	✅ in 0m	✅ in 0m	⏭️
quote4	✅	✅ in 0m	✅ in 0m	⏭️
reference-manual	✅	✅ in 1m	⏭️	⏭️
BibtexQuery		✅ in 0m	⏭️	⏭️
comparator		✅ in 0m	⏭️	⏭️
cslib		✅ in 1m	✅ in 0m	✅ in 0m
doc-gen4		✅ in 0m	⏭️	⏭️
illuminate		✅ in 0m	✅ in 0m	⏭️
lean4-unicode-basic		✅ in 0m	✅ in 0m	⏭️
lean4export		✅ in 0m	✅ in 0m	⏭️
LeanSearchClient		✅ in 0m	✅ in 0m	⏭️
leansqlite		✅ in 0m	✅ in 0m	⏭️
repl		✅ in 0m	✅ in 0m	⏭️
verso		✅ in 2m	✅ in 1m	⏭️
verso-web-components		✅ in 0m	⏭️	⏭️

View run

Kha · 2026-07-24T17:59:57Z

!bench mathlib

leanprover-radar · 2026-07-24T18:01:35Z

Benchmark results for f519b24 against 428f06e are in. There are significant results. @Kha

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

Large changes (35✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.4G (-20.08%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.6G (-22.72%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.2G (-24.71%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.8G (-35.02%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.2G (-37.08%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.9G (-37.79%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.5G (-33.66%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.4G (-32.34%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.7G (-24.61%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.9G (-24.48%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -40.0G (-37.06%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -34.3G (-28.56%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -40.0G (-35.33%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -17.0G (-21.21%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -21.1G (-28.71%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -25.3G (-33.84%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -13.2G (-23.41%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.3G (-19.42%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -28.2G (-34.63%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.3G (-24.84%)
and 15 more
and 1 hidden

Medium changes (255✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.19%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.5G (-16.10%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.1G (-9.64%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.21%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.16%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.6G (-6.89%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.0G (-14.62%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.3G (-12.45%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.2G (-10.66%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.66%)
✅ build/module/Mathlib.Algebra.Lie.Submodule//instructions: -4.4G (-7.92%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.46%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -6.4G (-10.31%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.3G (-10.75%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -2.4G (-5.22%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.7G (-12.34%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.2G (-8.25%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.09%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.9G (-10.69%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.9G (-5.69%)
and 236 more

Small changes (840✅, 6🟥)

✅ build/lakeprof/longest build path//instructions: -523.9G (-11.56%)
✅ build/module/Aesop.Saturate//instructions: -568.9M (-3.96%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -838.0M (-9.65%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -514.1M (-4.02%)
✅ build/module/Aesop.Search.Main//instructions: -415.0M (-4.12%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -437.0M (-7.69%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -425.3M (-3.55%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.7G (-7.26%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-13.10%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.5G (-3.78%)
✅ build/module/Mathlib.Algebra.Algebra.Hom//instructions: -694.3M (-3.57%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.0G (-7.88%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.2G (-4.85%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.21%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.54%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.5G (-9.38%)
✅ build/module/Mathlib.Algebra.BigOperators.Expect//instructions: -877.1M (-4.41%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.8G (-3.64%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.30%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.89%)
and 826 more

Kha · 2026-07-26T13:20:55Z

!bench mathlib

leanprover-radar · 2026-07-26T13:22:16Z

Benchmark results for 73ebb47 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.4T (-3.77%)

Large changes (35✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.3G (-19.82%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.1G (-22.11%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -24.8G (-24.37%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.2G (-34.45%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.1G (-36.77%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.3G (-36.61%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.3G (-33.50%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -16.9G (-31.52%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.5G (-24.39%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.3G (-23.66%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.7G (-36.81%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -32.0G (-26.59%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.8G (-35.18%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.5G (-20.70%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.2G (-27.55%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.4G (-32.69%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.7G (-22.39%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -25.9G (-19.07%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -27.8G (-34.15%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.0G (-23.99%)
and 15 more
and 1 hidden

Medium changes (223✅, 2🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.17%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.2G (-15.75%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.41%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.07%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.4G (-11.91%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.56%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.0G (-14.74%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.0G (-12.19%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.65%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.4G (-8.73%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.8G (-9.20%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.03%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.0G (-7.81%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.23%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.23%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.6G (-5.25%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.5G (-12.00%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.0G (-13.36%)
✅ build/module/Mathlib.Algebra.Polynomial.Module.Basic//instructions: -5.7G (-13.93%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -10.0G (-21.19%)
and 205 more

Small changes (817✅, 7🟥)

✅ build/lakeprof/longest build path//instructions: -539.2G (-11.89%)
✅ build/module/Aesop.Saturate//instructions: -539.2M (-3.76%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -810.2M (-9.33%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -498.2M (-3.89%)
✅ build/module/Aesop.Search.Main//instructions: -397.0M (-3.94%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -418.9M (-7.37%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -402.5M (-3.36%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.63%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.85%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.4G (-3.61%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.7G (-7.31%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.48%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.14%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.18%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.05%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.25%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.78%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -1.0G (-2.14%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.72%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.8G (-5.69%)
and 804 more

Kha · 2026-07-26T15:12:30Z

!bench mathlib

leanprover-radar · 2026-07-26T15:13:47Z

Benchmark results for c1515c8 against 428f06e are in. There are significant results. @Kha

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

Large changes (34✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.4G (-19.90%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.2G (-22.26%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.0G (-24.56%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.2G (-34.45%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.3G (-37.13%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.5G (-36.90%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.4G (-33.61%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.1G (-31.81%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.7G (-24.58%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.3G (-23.58%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.8G (-36.89%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -32.0G (-26.63%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.9G (-35.26%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.7G (-20.85%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.5G (-27.93%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.8G (-33.10%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.8G (-22.63%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.2G (-19.32%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -28.1G (-34.47%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.0G (-24.01%)
and 13 more
and 1 hidden

Medium changes (234✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.27%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.4G (-15.92%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.49%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.7G (-29.95%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.20%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.67%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.1G (-15.24%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.5G (-12.70%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.73%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.32%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.6G (-9.04%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.9G (-9.32%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -2.3G (-5.05%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.7G (-12.23%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.1G (-8.05%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.6G (-15.62%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.39%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.7G (-5.39%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.8G (-12.24%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.1G (-13.96%)
and 215 more

Small changes (830✅, 6🟥)

✅ build/lakeprof/longest build path//instructions: -517.5G (-11.42%)
✅ build/module/Aesop.Saturate//instructions: -540.1M (-3.76%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -810.2M (-9.33%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -493.2M (-3.86%)
✅ build/module/Aesop.Search.Main//instructions: -402.1M (-3.99%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -418.6M (-7.37%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -401.4M (-3.35%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.87%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.97%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.5G (-3.71%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.0G (-7.87%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.50%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.19%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.25%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.10%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.19%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.7G (-6.33%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -1.0G (-2.20%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.76%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.7G (-5.53%)
and 816 more

downstream: follow upstream PR

19e564b

downstream-lean4 Bot added the adaptation This is an adaptation PR for a PR in the lean4 repository. label Jul 24, 2026

downstream-lean4 Bot mentioned this pull request Jul 24, 2026

perf: normalize free variables in the type class resolution cache key leanprover/lean4#14369

Draft

downstream-lean4 Bot added the toolchain-available label Jul 24, 2026

downstream-lean4 Bot removed the toolchain-available label Jul 24, 2026

downstream: follow upstream PR

f519b24

downstream-lean4 Bot added toolchain-available and removed toolchain-available labels Jul 24, 2026

downstream: follow upstream PR

73ebb47

downstream-lean4 Bot added toolchain-available and removed toolchain-available labels Jul 26, 2026

downstream: follow upstream PR

c1515c8

downstream-lean4 Bot added the toolchain-available label Jul 26, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[#14369] perf: normalize free variables in the type class resolution cache key - #15

[#14369] perf: normalize free variables in the type class resolution cache key#15
downstream-lean4[bot] wants to merge 4 commits into
masterfrom
adaptation-14369

downstream-lean4 Bot commented Jul 24, 2026

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026 •

edited

Loading

Uh oh!

leanprover-radar commented Jul 24, 2026

Uh oh!

downstream-lean4 Bot commented Jul 24, 2026 •

edited

Loading

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026 •

edited

Loading

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

leanprover-radar commented Jul 26, 2026 •

edited

Loading

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

leanprover-radar commented Jul 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

downstream-lean4 Bot commented Jul 24, 2026

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

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

Uh oh!

Uh oh!

leanprover-radar commented Jul 24, 2026

Uh oh!

downstream-lean4 Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build report for downstream: follow upstream PR

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

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

Uh oh!

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

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

2 participants

leanprover-radar commented Jul 24, 2026 •

edited

Loading

downstream-lean4 Bot commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 26, 2026 •

edited

Loading

leanprover-radar commented Jul 26, 2026 •

edited

Loading