[#14316] experiment: persist type class resolution cache across commands

[downstream-lean4]

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

[downstream-lean4]

Build report for downstream: follow upstream PR

Turned red:

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 19s	🟥 in 5s	⏭️
mathlib4	✅	🟥 in 7s	⏭️	⏭️
cslib		⏭️	⏭️	⏭️
lean4export		✅ in 3s	🟥 in 7s	⏭️

Stayed red

Repo	Critical	Build	Test	Lint
verso-slides		🟥 in 22s	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
batteries	✅	✅ in 15s	✅ in 4s	✅ in 1s
import-graph	✅	✅ in 3s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 4s	✅ in 0s	⏭️
plausible	✅	✅ in 4s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 4s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 82s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
doc-gen4		✅ in 16s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 4s	✅ in 9s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 10s	✅ in 20s	⏭️
repl		✅ in 4s	✅ in 19s	⏭️
verso		✅ in 99s	✅ in 78s	⏭️
verso-web-components		✅ in 8s	⏭️	⏭️

View run

[Kha]

!bench

[leanprover-radar]

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

• ✅ build//instructions: -226.1G (-0.16%)

Medium changes (8✅)

• ✅ build/module/Mathlib.Analysis.Calculus.DerivativeTest//instructions: -4.0G (-8.80%)
• ✅ build/module/Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle//instructions: -11.6G (-20.49%)
• ✅ build/module/Mathlib.Analysis.SumIntegralComparisons//instructions: -4.1G (-12.89%)
• ✅ build/module/Mathlib.Computability.AkraBazzi.GrowsPolynomially//instructions: -4.9G (-10.73%)
• ✅ build/module/Mathlib.Data.List.Sym//instructions: -3.7G (-16.96%)
• ✅ build/module/Mathlib.NumberTheory.Chebyshev//instructions: -7.5G (-10.80%)
• ✅ build/module/Mathlib.NumberTheory.Modular//instructions: -21.9G (-16.84%)
• and 1 hidden

Small changes (72✅)

• ✅ build/module/Aesop.Saturate//instructions: -538.7M (-3.75%)
• ✅ build/module/Aesop.Script.SpecificTactics//instructions: -547.2M (-6.30%)
• ✅ build/module/Aesop.Search.Expansion.Norm//instructions: -418.6M (-3.27%)
• ✅ build/module/Aesop.Tree.ExtractScript//instructions: -394.8M (-6.95%)
• ✅ build/module/Batteries.Data.List.Lemmas//instructions: -998.0M (-2.49%)
• ✅ build/module/Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms//instructions: -2.2G (-7.48%)
• ✅ build/module/Mathlib.Analysis.Asymptotics.LinearGrowth//instructions: -2.0G (-7.71%)
• ✅ build/module/Mathlib.Analysis.Calculus.Deriv.MeanValue//instructions: -1.3G (-5.50%)
• ✅ build/module/Mathlib.Analysis.Calculus.LHopital//instructions: -2.5G (-10.13%)
• ✅ build/module/Mathlib.Analysis.Complex.AbelLimit//instructions: -1.7G (-7.98%)
• ✅ build/module/Mathlib.Analysis.Complex.Harmonic.Poisson//instructions: -2.6G (-14.90%)
• ✅ build/module/Mathlib.Analysis.Complex.JensenFormula//instructions: -3.7G (-7.88%)
• ✅ build/module/Mathlib.Analysis.Complex.UnitDisc.Basic//instructions: -1.5G (-5.57%)
• ✅ build/module/Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints//instructions: -2.8G (-12.47%)
• ✅ build/module/Mathlib.Analysis.Complex.UpperHalfPlane.Manifold//instructions: -1.9G (-7.28%)
• ✅ build/module/Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction//instructions: -2.1G (-5.96%)
• ✅ build/module/Mathlib.Analysis.Complex.ValueDistribution.Cartan//instructions: -1.5G (-10.18%)
• ✅ build/module/Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation//instructions: -1.2G (-5.26%)
• ✅ build/module/Mathlib.Analysis.Convex.Deriv//instructions: -2.0G (-5.46%)
• ✅ build/module/Mathlib.Analysis.MeanInequalities//instructions: -2.8G (-4.48%)
• and 52 more