perf: move currRecDepth from Core.Context into Core.State

[Kha]

No description provided.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 6e75456 against 696e847 are in. There are significant results. @Kha

• 🟥 build//instructions: +44.1G (+0.39%)

Large changes (2🟥)

• 🟥 compiled/phashmap//task-clock: +145ms (+33.34%)
• 🟥 compiled/phashmap//wall-clock: +145ms (+33.25%)

Medium changes (1🟥)

• 🟥 elab/big_do//instructions: +100.0M (+0.55%)

Small changes (335🟥)

• 🟥 build/module/Init.CbvSimproc//instructions: +12.3M (+0.59%)
• 🟥 build/module/Init.Control.Basic//instructions: +13.1M (+0.61%)
• 🟥 build/module/Init.Control.Lawful.Instances//instructions: +29.3M (+0.44%)
• 🟥 build/module/Init.Core//instructions: +67.5M (+0.69%)
• 🟥 build/module/Init.Data.Array.Attach//instructions: +57.6M (+0.57%)
• 🟥 build/module/Init.Data.Array.Basic//instructions: +56.8M (+0.53%)
• 🟥 build/module/Init.Data.Array.Erase//instructions: +30.5M (+0.43%)
• 🟥 build/module/Init.Data.Array.Find//instructions: +40.2M (+0.42%)
• 🟥 build/module/Init.Data.Array.Lemmas//instructions: +288.8M (+0.55%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Array.Lex.Lemmas//instructions: +35.9M (+0.38%)
• 🟥 build/module/Init.Data.Array.MapIdx//instructions: +51.9M (+0.60%)
• 🟥 build/module/Init.Data.Array.Monadic//instructions: +35.8M (+0.60%)
• 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +32.5M (+0.33%)
• 🟥 build/module/Init.Data.Array.Sort.Lemmas//instructions: +13.5M (+0.43%)
• 🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +159.7M (+0.32%)
• 🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +457.1M (+0.40%)
• 🟥 build/module/Init.Data.ByteArray.Lemmas//instructions: +22.8M (+0.42%)
• 🟥 build/module/Init.Data.Char.Ordinal//instructions: +24.8M (+0.43%)
• 🟥 build/module/Init.Data.Fin.Lemmas//instructions: +48.4M (+0.45%)
• 🟥 build/module/Init.Data.Int.DivMod.Lemmas//instructions: +180.0M (+0.49%)
• and 314 more
• and 1 hidden

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 696e847a6c079637186e492f37e22dedf4faf679 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-29 13:50:35)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 696e847a6c079637186e492f37e22dedf4faf679 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force reference manual CI using the force-manual-ci label. (2026-08-29 13:50:37)