[#14970] perf: give currRecDepth its own ReaderT layer in CoreM

[downstream-lean4]

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

[Kha]

!bench

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for 8f70635 against 92e8256 are in. There are significant results. @Kha

• ✅ build//instructions: -1.6T (-1.10%)

Large changes (1✅)

• 1 hidden

Medium changes (7✅)

• ✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -1.1G (-2.38%)
• ✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: -2.0G (-2.09%)
• ✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -1.2G (-1.85%)
• ✅ build/module/Mathlib.Analysis.Distribution.SchwartzSpace.Fourier//instructions: -1.3G (-2.29%)
• ✅ build/module/Mathlib.Geometry.Convex.ConvexSpace.Module//instructions: -1.9G (-3.21%)
• ✅ build/module/Mathlib.Geometry.Manifold.VectorBundle.Hom//instructions: -1.3G (-1.80%)
• ✅ build/module/Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas//instructions: -1.7G (-2.10%)

Small changes (623✅, 4🟥)

• ✅ build/module/Aesop.Options.Public//instructions: -25.7M (-1.22%)
• 🟥 build/module/Aesop.Saturate//instructions: +80.3M (+0.57%)
• ✅ build/module/Aesop.Script.OptimizeSyntax//instructions: -25.0M (-1.14%)
• ✅ build/module/Aesop.Stats.Report//instructions: -36.5M (-1.30%)
• ✅ build/module/Aesop.Tree.Data//instructions: -80.2M (-1.37%)
• ✅ build/module/Aesop.Tree.State//instructions: -30.9M (-1.18%)
• 🟥 build/module/Aesop.Tree.Tracing//instructions: +30.0M (+0.60%)
• ✅ build/module/Aesop.Util.Basic//instructions: -69.0M (-0.91%)
• ✅ build/module/Batteries.CodeAction.Basic//instructions: -23.9M (-0.85%)
• ✅ build/module/Batteries.CodeAction.Match//instructions: -46.6M (-1.29%)
• ✅ build/module/Batteries.CodeAction.Misc//instructions: -88.7M (-1.14%)
• ✅ build/module/Batteries.Control.AlternativeMonad//instructions: -37.2M (-1.40%)
• ✅ build/module/Batteries.Control.LawfulMonadState//instructions: -81.2M (-1.94%)
• ✅ build/module/Batteries.Control.OptionT//instructions: -17.8M (-1.15%)
• ✅ build/module/Batteries.Data.Array.Match//instructions: -36.4M (-1.26%)
• ✅ build/module/Batteries.Data.Array.Merge//instructions: -53.0M (-0.99%)
• ✅ build/module/Batteries.Data.Array.Scan//instructions: -153.2M (-1.54%)
• ✅ build/module/Batteries.Data.AssocList//instructions: -94.5M (-1.48%)
• ✅ build/module/Batteries.Data.BinaryHeap.Basic//instructions: -90.5M (-1.17%)
• ✅ build/module/Batteries.Data.BinomialHeap.Basic//instructions: -359.4M (-1.75%)
• and 607 more

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for dedf608 against dfa0830 are in. There are significant results. @Kha

• 🟥 main exited with code 1

No significant changes detected.

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for cff711a against dfa0830 are in. There are significant results. @Kha

• ✅ build//instructions: -854.1G (-0.60%)

Large changes (1✅)

• 1 hidden

Medium changes (1✅)

• ✅ build/module/Mathlib.Geometry.Convex.ConvexSpace.Module//instructions: -1.2G (-1.96%)

Small changes (141✅, 31🟥)

• 🟥 build/module/Aesop.Builder.Forward//instructions: +52.1M (+1.02%)
• 🟥 build/module/Aesop.Forward.Match//instructions: +42.7M (+0.82%)
• 🟥 build/module/Aesop.Index//instructions: +37.5M (+0.84%)
• 🟥 build/module/Aesop.Main//instructions: +49.8M (+1.36%)
• 🟥 build/module/Aesop.RuleSet//instructions: +88.8M (+0.76%)
• 🟥 build/module/Aesop.RuleTac.Apply//instructions: +23.4M (+1.05%)
• 🟥 build/module/Aesop.RuleTac.Forward//instructions: +38.3M (+0.63%)
• 🟥 build/module/Aesop.Saturate//instructions: +178.8M (+1.29%)
• 🟥 build/module/Aesop.Script.StructureDynamic//instructions: +41.5M (+0.79%)
• 🟥 build/module/Aesop.Search.Expansion.Norm//instructions: +84.7M (+0.70%)
• 🟥 build/module/Aesop.Search.Expansion//instructions: +78.5M (+1.02%)
• 🟥 build/module/Aesop.Search.Main//instructions: +91.7M (+0.99%)
• 🟥 build/module/Aesop.Search.RuleSelection//instructions: +19.7M (+0.84%)
• 🟥 build/module/Aesop.Tree.Check//instructions: +58.0M (+1.18%)
• 🟥 build/module/Aesop.Tree.ExtractProof//instructions: +25.4M (+0.66%)
• 🟥 build/module/Aesop.Tree.ExtractScript//instructions: +58.9M (+1.07%)
• 🟥 build/module/Aesop.Tree.Tracing//instructions: +61.4M (+1.24%)
• 🟥 build/module/Aesop.Util.EqualUpToIds//instructions: +68.2M (+0.77%)
• ✅ build/module/Batteries.CodeAction.Match//instructions: -26.4M (-0.74%)
• ✅ build/module/Batteries.CodeAction.Misc//instructions: -47.7M (-0.62%)
• and 152 more

[downstream-lean4]

Build report for downstream: follow upstream PR

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 18s	✅ in 4s	⏭️
batteries	✅	✅ in 13s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 3s	✅ in 0s	⏭️
mathlib4	✅	✅ in 1051s	✅ in 43s	✅ in 94s
plausible	✅	✅ in 3s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 5s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 75s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
cslib		✅ in 34s	✅ in 9s	✅ in 3s
doc-gen4		✅ in 16s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 4s	⏭️	⏭️
lean4export		✅ in 3s	✅ in 7s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 10s	✅ in 19s	⏭️
repl		✅ in 4s	✅ in 60s	⏭️
verso		✅ in 130s	✅ in 87s	⏭️
verso-slides		✅ in 19s	✅ in 6s	⏭️
verso-web-components		✅ in 37s	⏭️	⏭️

View run