Skip to content

perf: move ref into the Core.Context cold subobject #15027

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Kha wants to merge 2 commits into
base: master
Choose a base branch
from
+18 −12
Draft

perf: move ref into the Core.Context cold subobject #15027

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a05f18d
perf: move every rarely-updated `Core.Context` field into the cold su…
Kha Sep 4, 2026
1ed4f9a
perf: move `ref` into the `Core.Context` cold subobject
Kha Sep 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 18 additions & 12 deletions src/Lean/CoreM.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -214,18 +214,32 @@ 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 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` 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
ref : Syntax := Syntax.missing
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`. -/
Expand All @@ -234,15 +248,7 @@ 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.
Expand Down
Loading