perf: move `ref` into the `Core.Context` cold subobject This PR removes the last per-recursion-step reference count increment on a thread-shared object, leaving `withIncRecDepth` copying only the cold subobject pointer. The instruction saving is small, but the increment it removes is expected to be a contended atomic one, so the effect on wall-clock should be larger than on instructions. `ref` points into the command's parsed syntax tree, which is shared with async elaboration tasks and therefore marked multi-threaded, making each increment on it a locked read-modify-write. The cold subobject is instead rebuilt often enough (about 18k times per module, by `withFreshMacroScope` and `withCurrHeartbeats`) that its instances are usually fresh, single-threaded and cheap to increment. Moving `ref` across therefore trades roughly 1.0M contended increments on the recursion path for about 155k on the 31k `withRef` calls that now rebuild the cold record. Measured on a representative module, `withIncRecDepth` drops from three increments to two and `withRef` rises from three to fourteen; the `Context` constructor becomes `(0, 2, 2)`. The trade rests on `withRef` staying far rarer than `withIncRecDepth` — about 31k against 1.0M there — so it should be checked on syntax-heavy workloads before being relied upon. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.