From 82db66b161ce99127d3f152bdaf9dab367a48a18 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Sep 2026 09:49:24 +0000 Subject: [PATCH] perf: move every rarely-updated `Core.Context` field into the cold subobject This PR cuts the reference count traffic paid by the recursion-depth and `withRef` steps that dominate elaboration, from ten increments per reconstruction to three. Measured against master it saves between 0.35% and 1.24% of elaboration instructions across match-, simp- and grind-heavy workloads. `withReader` can never reuse the `Context` record, so every reconstruction pays one increment per pointer field. The original split classified fields by their number of update *sites*; this classifies them by measured update *frequency* instead. On a representative module `withIncRecDepth` runs about 1.0M times and `withRef` about 31k, while `withOptions` runs once, so `options`, `maxRecDepth`, `currNamespace`, `openDecls`, `initHeartbeats`, `maxHeartbeats` and `currMacroScope` join the cold group and only `currRecDepth` and `ref` stay hot. The `Context` constructor goes from `(0, 10, 2)` to `(0, 3, 2)`. Rebuilding the wider cold record does make the rare paths that update those fields more expensive: `withCurrHeartbeats` goes from ten increments to fourteen. At roughly 4.9k such calls against 1.05M reconstructions, the trade is strongly positive. Co-Authored-By: Claude Opus 5 --- src/Lean/CoreM.lean | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index c625885b98b7..ce7c6379fa56 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -214,18 +214,29 @@ structure State where deriving Nonempty /-- -The pointer-valued fields of `Core.Context` that are updated at most a handful of times per command. +The pointer-typed fields of `Core.Context` that are not updated on a recursion or `withRef` step. -`withReader` can never reuse the `Context` record, so every `withRef`, `withOptions` or -`withIncRecDepth` pays one reference count increment per pointer field. Grouping these fields into a -subobject makes them cost a single increment together. +`withReader` can never reuse the `Context` record, so every `withIncRecDepth` and `withRef` pays one +reference count increment per pointer field. Grouping the remaining fields into a subobject makes +them cost a single increment together. + +Rarely-updated fields in particular tend to be MT during async elaboration, which makes RC traffic +elisions on them even more valueable, explaining an outsized task-clock vs instrs impact of this +optimization. -/ structure Context.Cold where /-- Name of the file being compiled. -/ fileName : String /-- Auxiliary datastructure for converting `String.Pos` into Line/Column number. -/ fileMap : FileMap + options : Options := {} + maxRecDepth : Nat := 1000 + currNamespace : Name := Name.anonymous + openDecls : List OpenDecl := [] + initHeartbeats : Nat := 0 + maxHeartbeats : Nat := getMaxHeartbeats options quotContext : Name := .anonymous + currMacroScope : MacroScope := firstFrontendMacroScope /-- If set, used to cancel elaboration from outside when results are not needed anymore. -/ cancelTk? : Option IO.CancelToken := none /-- Cache of `Lean.inheritedTraceOptions`. -/ @@ -234,15 +245,8 @@ structure Context.Cold where /-- Context for the CoreM monad. -/ structure Context extends Context.Cold where - options : Options := {} currRecDepth : Nat := 0 - maxRecDepth : Nat := 1000 ref : Syntax := Syntax.missing - currNamespace : Name := Name.anonymous - openDecls : List OpenDecl := [] - initHeartbeats : Nat := 0 - maxHeartbeats : Nat := getMaxHeartbeats options - currMacroScope : MacroScope := firstFrontendMacroScope /-- If `diag := true`, different parts of the system collect diagnostics. Use the `set_option diag true` to set it to true.