From a05f18dc5aa0c849ba9782de347ac27b62b6302f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Sep 2026 09:49:24 +0000 Subject: [PATCH 1/2] 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 | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index c625885b98b7..c1b3e6c5891f 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -214,18 +214,31 @@ 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-valued 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. + +Membership follows measured update frequency, not the number of update sites: on a representative +module, `withIncRecDepth` runs about 1.0M times and `withRef` about 31k, while `withOptions` runs +*once*. Fields updated only on such rare paths belong here even where they have many syntactic +update sites, and rebuilding this record on those paths is far cheaper than copying its fields on +every recursion step. -/ 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 +247,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. From 1ed4f9a86b70dcb072363b1f1b6bcaf5746ca3f5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Sep 2026 12:03:15 +0000 Subject: [PATCH 2/2] perf: move `ref` into the `Core.Context` cold subobject MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/Lean/CoreM.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index c1b3e6c5891f..16557ee3d037 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -214,10 +214,10 @@ structure State where deriving Nonempty /-- -The pointer-valued fields of `Core.Context` that are not updated on a recursion or `withRef` step. +The pointer-valued fields of `Core.Context` that are not updated on a recursion step. -`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 +`withReader` can never reuse the `Context` record, so every `withIncRecDepth` pays one reference +count increment per pointer field. Grouping the remaining fields into a subobject makes them cost a single increment together. Membership follows measured update frequency, not the number of update sites: on a representative @@ -237,6 +237,7 @@ structure Context.Cold where openDecls : List OpenDecl := [] initHeartbeats : Nat := 0 maxHeartbeats : Nat := getMaxHeartbeats options + ref : Syntax := Syntax.missing quotContext : Name := .anonymous currMacroScope : MacroScope := firstFrontendMacroScope /-- If set, used to cancel elaboration from outside when results are not needed anymore. -/ @@ -248,7 +249,6 @@ structure Context.Cold where /-- Context for the CoreM monad. -/ structure Context extends Context.Cold where currRecDepth : Nat := 0 - ref : Syntax := Syntax.missing /-- If `diag := true`, different parts of the system collect diagnostics. Use the `set_option diag true` to set it to true.