From a0dab163efd9e7cb4fab302eb2a5a230bef59981 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 17 Oct 2025 21:18:44 +0200
Subject: [PATCH 1/8] refactor: add `MonadLift CoreM CommandElabM`

---
 src/Lean/Elab/Command.lean           | 130 +++++++++++++++++----------
 src/Lean/Elab/DocString/Builtin.lean |   4 +-
 src/Lean/Elab/Frontend.lean          |   2 +-
 src/Lean/Language/Lean.lean          |  10 +--
 src/Lean/Server/Snapshots.lean       |   2 +-
 5 files changed, 92 insertions(+), 56 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index ff08a186d2bd..fac1bbc9a575 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -31,6 +31,10 @@ structure State where
   snapshotTasks  : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
+structure DerivedState extends State where
+  private coreCtx : Core.Context
+  private coreState : Core.State
+
 structure Context where
   fileName       : String
   fileMap        : FileMap
@@ -59,7 +63,7 @@ structure Context where
   -/
   suppressElabErrors : Bool := false
 
-abbrev CommandElabM := ReaderT Context $ StateRefT State $ EIO Exception
+abbrev CommandElabM := ReaderT Context $ StateRefT DerivedState $ EIO Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 structure Linter where
   run : Syntax → CommandElabM Unit
@@ -74,6 +78,70 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
+private def DerivedState.derive (ctx : Context) (s : State) : DerivedState where
+  toState := s
+  coreCtx := {
+    fileName           := ctx.fileName
+    fileMap            := ctx.fileMap
+    currRecDepth       := ctx.currRecDepth
+    maxRecDepth        := s.maxRecDepth
+    ref                := ctx.ref
+    currNamespace      := scope.currNamespace
+    openDecls          := scope.openDecls
+    initHeartbeats     := 0
+    quotContext        := ctx.quotContext?.getD s.env.mainModule
+    currMacroScope     := ctx.currMacroScope
+    options            := scope.opts
+    cancelTk?          := ctx.cancelTk?
+    suppressElabErrors := ctx.suppressElabErrors }
+  coreState := {
+    env := s.env
+    ngen := s.ngen
+    auxDeclNGen := s.auxDeclNGen
+    nextMacroScope := s.nextMacroScope
+    infoState := s.infoState
+    traceState := s.traceState
+    snapshotTasks := s.snapshotTasks
+    messages := s.messages
+  }
+where
+  scope := s.scopes.head!
+
+private def State.updateCore (s : State) (coreS : Core.State) : State :=
+  { s with
+    env                      := coreS.env
+    nextMacroScope           := coreS.nextMacroScope
+    ngen                     := coreS.ngen
+    auxDeclNGen              := coreS.auxDeclNGen
+    infoState                := coreS.infoState
+    traceState               := coreS.traceState
+    snapshotTasks            := coreS.snapshotTasks
+    messages                 := coreS.messages }
+
+instance : MonadStateOf State CommandElabM where
+  get := return (← getThe DerivedState).toState
+  set s := private do set (DerivedState.derive (← read) s)
+  modifyGet f := private do
+    let ctx ← read
+    modifyGetThe DerivedState fun ds =>
+      let (a, s') := f ds.toState
+      (a, DerivedState.derive ctx s')
+
+instance : MonadLift CoreM CommandElabM where
+  monadLift x := private do
+    let ds ← getThe DerivedState
+    let (a, coreS) ← x.run ds.coreCtx ds.coreState
+    modify fun s => s.updateCore coreS
+    return a
+
+protected nonrec def CommandElabM.run (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception (α × State) := do
+  let ds := DerivedState.derive ctx s
+  let (a, ds') ← x.run ctx |>.run ds
+  return (a, ds'.toState)
+
+protected def CommandElabM.run' (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception α := do
+  (·.1) <$> x.run ctx s
+
 /--
 Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
 want to catch and process them at the command level.
@@ -161,49 +229,15 @@ instance : MonadQuotation CommandElabM where
   withFreshMacroScope := Command.withFreshMacroScope
 
 private def runCore (x : CoreM α) : CommandElabM α := do
-  let s ← get
+  let s ← getThe DerivedState
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
   let env := Kernel.resetDiag s.env
-  let scope := s.scopes.head!
-  let coreCtx : Core.Context := {
-    fileName           := ctx.fileName
-    fileMap            := ctx.fileMap
-    currRecDepth       := ctx.currRecDepth
-    maxRecDepth        := s.maxRecDepth
-    ref                := ctx.ref
-    currNamespace      := scope.currNamespace
-    openDecls          := scope.openDecls
-    initHeartbeats     := heartbeats
-    quotContext        := (← MonadQuotation.getMainModule)
-    currMacroScope     := ctx.currMacroScope
-    options            := scope.opts
-    cancelTk?          := ctx.cancelTk?
-    suppressElabErrors := ctx.suppressElabErrors }
-  let x : EIO _ _ := x.run coreCtx {
-    env
-    ngen := s.ngen
-    auxDeclNGen := s.auxDeclNGen
-    nextMacroScope := s.nextMacroScope
-    infoState.enabled := s.infoState.enabled
-    -- accumulate lazy assignments from all `CoreM` lifts
-    infoState.lazyAssignment := s.infoState.lazyAssignment
-    traceState := s.traceState
-    snapshotTasks := s.snapshotTasks
-  }
+  let coreCtx : Core.Context := { s.coreCtx with initHeartbeats := heartbeats }
+  let x : EIO _ _ := x.run coreCtx { s.coreState with env }
   let (ea, coreS) ← liftM x
-  modify fun s => { s with
-    env                      := coreS.env
-    nextMacroScope           := coreS.nextMacroScope
-    ngen                     := coreS.ngen
-    auxDeclNGen              := coreS.auxDeclNGen
-    infoState.trees          := s.infoState.trees.append coreS.infoState.trees
-    -- we assume substitution of `assignment` has already happened, but for lazy assignments we only
-    -- do it at the very end
-    infoState.lazyAssignment := coreS.infoState.lazyAssignment
+  modify fun s => s.updateCore { coreS with
     traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    snapshotTasks            := coreS.snapshotTasks
-    messages                 := s.messages ++ coreS.messages
   }
   return ea
 
@@ -278,7 +312,7 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
   setDeclNGen parentNGen
   let st ← get
   let st := { st with auxDeclNGen := childNGen }
-  return (act · |>.run ctx |>.run' st)
+  return (act · |>.run' ctx st)
 
 open Language in
 @[inherit_doc Core.wrapAsyncAsSnapshot]
@@ -598,8 +632,13 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
   -- initialize quotation context using hash of input string
   let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false)
   withInitQuotContext (ss?.map (hash ·.toString.trim)) do
-  -- Reset messages and info state, which are both per-command
-  modify fun st => { st with messages := {}, infoState := { enabled := st.infoState.enabled } }
+  -- Reset per-command state
+  modify fun st => { st with
+    messages := {}
+    infoState := { enabled := st.infoState.enabled }
+    traceState := {}
+    snapshotTasks := #[]
+  }
   try
     -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error
     -- recovery more coarse. In particular, if `c` in `set_option ... in $c` fails, the remaining
@@ -801,8 +840,8 @@ open Elab Command MonadRecDepth
 private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) : CoreM α := do
   let s : Core.State ← get
   let ctx : Core.Context ← read
-  let (a, commandState) ←
-    cmd.run {
+  let (a, commandState) ← do
+    let cmdCtx := {
       fileName := ctx.fileName
       fileMap := ctx.fileMap
       currRecDepth := ctx.currRecDepth
@@ -811,7 +850,8 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
       snap? := none
       cancelTk? := ctx.cancelTk?
       suppressElabErrors := ctx.suppressElabErrors
-    } |>.run {
+    }
+    cmd.run cmdCtx {
       env := s.env
       nextMacroScope := s.nextMacroScope
       maxRecDepth := ctx.maxRecDepth
diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean
index 27366f4252a1..78dfdea6a6b5 100644
--- a/src/Lean/Elab/DocString/Builtin.lean
+++ b/src/Lean/Elab/DocString/Builtin.lean
@@ -696,7 +696,7 @@ where
       (cctx : Command.Context) (cmdState : Command.State) :
       DocM Command.State := do
     let (output, cmdState) ←
-      match (← liftM <| IO.FS.withIsolatedStreams <| EIO.toIO' <| (act.run cctx).run cmdState) with
+      match (← liftM <| IO.FS.withIsolatedStreams <| EIO.toIO' <| act.run cctx cmdState) with
       | (output, .error e) => Lean.logError e.toMessageData; pure (output, cmdState)
       | (output, .ok ((), cmdState)) => pure (output, cmdState)
 
@@ -706,7 +706,7 @@ where
       if let some tok := firstToken? stx then logInfoAt tok
       else logInfo
 
-    match (← liftM <| EIO.toIO' <| ((log output).run cctx).run cmdState) with
+    match (← liftM <| EIO.toIO' <| (log output).run cctx cmdState) with
     | .error _ => pure cmdState
     | .ok ((), cmdState) => pure cmdState
 
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 6328da4221d7..73a8a9bab347 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -39,7 +39,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
     snap?        := none
     cancelTk?    := none
   }
-  match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
+  match (← liftM <| EIO.toIO' <| x.run cmdCtx s.commandState) with
   | Except.error e      => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
   | Except.ok (a, sNew) => setCommandState sNew; return a
 
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index ab3beca6cbe5..1af8421ed565 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -746,21 +746,17 @@ where
       LeanProcessingM Command.State := do
     let ctx ← read
     let scope := cmdState.scopes.head!
-    -- reset per-command state
-    let cmdStateRef ← IO.mkRef { cmdState with
-      messages := .empty, traceState := {}, snapshotTasks := #[] }
     let cmdCtx : Elab.Command.Context := { ctx with
       cmdPos       := beginPos
       snap?        := if internal.cmdlineSnapshots.get scope.opts then none else snap
       cancelTk?    := some cancelTk
     }
-    let (output, _) ←
+    let (output, .ok ((), cmdState)) ←
       IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get scope.opts) do
-        EIO.toBaseIO do
+        EIO.toBaseIO <| CommandElabM.run cmdCtx cmdState do
           withLoggingExceptions
             (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
-            cmdCtx cmdStateRef
-    let cmdState ← cmdStateRef.get
+      | let _ : Inhabited Command.State := ⟨cmdState⟩; unreachable!
     let mut messages := cmdState.messages
     if !output.isEmpty then
       messages := messages.add {
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index e3b0fe5a8b3c..0333a0be1d74 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -61,7 +61,7 @@ def runCommandElabM (snap : Snapshot) (doc : DocumentMeta) (c : CommandElabM α)
     snap? := none
     cancelTk? := none
   }
-  c.run ctx |>.run' snap.cmdState
+  c.run' ctx snap.cmdState
 
 /-- Run a `CoreM` computation using the data in the given snapshot.-/
 def runCoreM (snap : Snapshot) (doc : DocumentMeta) (c : CoreM α) : EIO Exception α :=

From 7a432fb0ff3fe980136bc015598e38d17bba4eae Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 17 Oct 2025 23:01:52 +0200
Subject: [PATCH 2/8] de-classify `ExtraModUses`

---
 src/Lean/Elab/Attributes.lean          |  6 +++---
 src/Lean/Elab/Command.lean             |  4 ----
 src/Lean/Elab/DeclModifiers.lean       | 10 ++++------
 src/Lean/Elab/RecommendedSpelling.lean |  2 +-
 src/Lean/Elab/Term/TermElabM.lean      |  4 ----
 src/Lean/Elab/Util.lean                | 18 ++++--------------
 src/Lean/ExtraModUses.lean             | 10 ++++------
 7 files changed, 16 insertions(+), 38 deletions(-)

diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 29205a81499d..2e07a2fedf50 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -44,7 +44,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr (attrInstance : Syntax) : CoreM Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
@@ -60,7 +60,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs (attrInstances : Array Syntax) : CoreM (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -70,7 +70,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs (stx : Syntax) : CoreM (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index fac1bbc9a575..5e8805db87b3 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -446,10 +446,6 @@ def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : Com
   withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
     withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
-instance : MonadMacroAdapter CommandElabM where
-  getNextMacroScope := return (← get).nextMacroScope
-  setNextMacroScope next := modify fun s => { s with nextMacroScope := next }
-
 instance : MonadRecDepth CommandElabM where
   withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
   getRecDepth      := return (← read).currRecDepth
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index b72741257895..fe481362e933 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -164,10 +164,8 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m (
 
 section Methods
 
-variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadFinally m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
-
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `meta`, `noncomputable`, doc string)-/
-def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
+def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : CoreM Modifiers := do
   let docCommentStx := stx.raw[0]
   let attrsStx      := stx.raw[1]
   let visibilityStx := stx.raw[2]
@@ -209,7 +207,7 @@ Ensure the function has not already been declared, and apply the given visibilit
 If `private`, return the updated name using our internal encoding for private names.
 If `protected`, register `declName` as protected in the environment.
 -/
-def applyVisibility (modifiers : Modifiers) (declName : Name) : m Name := do
+def applyVisibility (modifiers : Modifiers) (declName : Name) : CoreM Name := do
   let mut declName := declName
   if !modifiers.visibility.isInferredPublic (← getEnv) then
     declName := mkPrivateName (← getEnv) declName
@@ -218,7 +216,7 @@ def applyVisibility (modifiers : Modifiers) (declName : Name) : m Name := do
     modifyEnv fun env => addProtected env declName
   pure declName
 
-def checkIfShadowingStructureField (declName : Name) : m Unit := do
+def checkIfShadowingStructureField (declName : Name) : CoreM Unit := do
   match declName with
   | Name.str pre .. =>
     if isStructure (← getEnv) pre then
@@ -228,7 +226,7 @@ def checkIfShadowingStructureField (declName : Name) : m Unit := do
           throwError "invalid declaration name `{.ofConstName declName}`, structure `{pre}` has field `{fieldName}`"
   | _ => pure ()
 
-def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do
+def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : CoreM (Name × Name) := do
   let mut shortName := shortName
   let mut currNamespace := currNamespace
   let view := extractMacroScopes shortName
diff --git a/src/Lean/Elab/RecommendedSpelling.lean b/src/Lean/Elab/RecommendedSpelling.lean
index 7aa62c1bc6f8..e9122870b099 100644
--- a/src/Lean/Elab/RecommendedSpelling.lean
+++ b/src/Lean/Elab/RecommendedSpelling.lean
@@ -19,7 +19,7 @@ open Lean.Parser.Command
 @[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab
   | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $spelling:str for $«notation»:str in [$[$decls:ident],*]) => do
     let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl)
-    declNames.forM (recordExtraModUseFromDecl (isMeta := false))
+    declNames.forM (recordExtraModUseFromDecl (isMeta := false) ·)
     let recommendedSpelling : RecommendedSpelling := {
       «notation» := «notation».getString
       recommendedSpelling := spelling.getString
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 0428f7818aee..688f829e9908 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -1457,10 +1457,6 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
   | []      => throwError "elaboration function for `{k}` has not been implemented{indentD stx}"
   | elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
 
-instance : MonadMacroAdapter TermElabM where
-  getNextMacroScope := return (← getThe Core.State).nextMacroScope
-  setNextMacroScope next := modifyThe Core.State fun s => { s with nextMacroScope := next }
-
 private def isExplicit (stx : Syntax) : Bool :=
   match stx with
   | `(@$_) => true
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index a4bd3108b24a..81b9ec5afe8d 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -166,17 +166,7 @@ def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Ex
       | ex                                => return (e.declName, Except.error ex)
   return none
 
-class MonadMacroAdapter (m : Type → Type) extends MonadQuotation m where
-  getNextMacroScope                  : m MacroScope
-  setNextMacroScope                  : MacroScope → m Unit
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadQuotation n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
-  getNextMacroScope := liftM (MonadMacroAdapter.getNextMacroScope : m _)
-  setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
-}
-
-def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do
+def liftMacroM (x : MacroM α) : CoreM α := do
   let env  ← getEnv
   let opts ← getOptions
   let currNamespace ← getCurrNamespace
@@ -198,7 +188,7 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
             quotContext    := ← MonadQuotation.getContext
             currRecDepth   := ← MonadRecDepth.getRecDepth
             maxRecDepth    := ← MonadRecDepth.getMaxRecDepth
-          } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
+          } { macroScope := (← get).nextMacroScope } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
   | EStateM.Result.error (Macro.Exception.error ref msg) _   =>
     if msg == maxRecDepthErrorMessage then
@@ -209,11 +199,11 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
   | EStateM.Result.ok a s =>
     for n in s.expandedMacroDecls do
       recordExtraModUseFromDecl (isMeta := true) n
-    MonadMacroAdapter.setNextMacroScope s.macroScope
+    modify ({ · with nextMacroScope :=  s.macroScope })
     s.traceMsgs.reverse.forM fun (clsName, msg) => trace clsName fun _ => msg
     return a
 
-@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m]  [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : Macro) (stx : Syntax) : m Syntax :=
+@[inline] def adaptMacro (x : Macro) (stx : Syntax) : CoreM Syntax :=
   liftMacroM (x stx)
 
 partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
diff --git a/src/Lean/ExtraModUses.lean b/src/Lean/ExtraModUses.lean
index 28f151b9c929..0219a31a4a16 100644
--- a/src/Lean/ExtraModUses.lean
+++ b/src/Lean/ExtraModUses.lean
@@ -49,9 +49,7 @@ public def copyExtraModUses (src dest : Environment) : Environment := Id.run do
       env := extraModUses.addEntry env entry
   env
 
-variable [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m]
-
-def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymous) : m Unit := do
+def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymous) : CoreM Unit := do
   let entry := { module := mod, isExported := (← getEnv).isExporting, isMeta }
   if !(extraModUses.getState (asyncMode := .local) (← getEnv)).contains entry then
     trace[extraModUses] "recording {if entry.isExported then "public" else "private"} \
@@ -63,7 +61,7 @@ def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymou
 Records an additional import dependency for the current module, using `Environment.isExporting` as
 the visibility level.
 -/
-public def recordExtraModUse (modName : Name) (isMeta : Bool) : m Unit := do
+public def recordExtraModUse (modName : Name) (isMeta : Bool) : CoreM Unit := do
   if modName != (← getEnv).mainModule then
     recordExtraModUseCore modName isMeta
 
@@ -72,7 +70,7 @@ Records the module of the given declaration as an additional import dependency f
 module, using `Environment.isExporting` as the visibility level. If the declaration itself is
 already `meta`, the module dependency is recorded as a non-`meta` dependency.
 -/
-public def recordExtraModUseFromDecl (declName : Name) (isMeta : Bool) : m Unit := do
+public def recordExtraModUseFromDecl (declName : Name) (isMeta : Bool) : CoreM Unit := do
   let env ← getEnv
   if let some mod := env.getModuleIdxFor? declName |>.bind (env.header.modules[·]?) then
     -- If the declaration itself is already `meta`, no need to mark the import.
@@ -91,7 +89,7 @@ public def isExtraRevModUse (env : Environment) (modIdx : ModuleIdx) : Bool :=
   !(isExtraRevModUseExt.getModuleEntries env modIdx |>.isEmpty)
 
 /-- Records this module to be preserved as an import by `shake`. -/
-public def recordExtraRevUseOfCurrentModule : m Unit := do
+public def recordExtraRevUseOfCurrentModule : CoreM Unit := do
   if isExtraRevModUseExt.getEntries (asyncMode := .local) (← getEnv) |>.isEmpty then
     modifyEnv (isExtraRevModUseExt.addEntry · ())
 

From b18bd211b2133382069168844280df196a4f809a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 14:01:48 +0200
Subject: [PATCH 3/8] perf: avoid repeated lifts

---
 src/Lean/Elab/Command.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 5e8805db87b3..608c7fc95302 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -611,7 +611,7 @@ def withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) : Comm
   finally
     modify ({ · with nextMacroScope })
 
-private partial def recordUsedSyntaxKinds (stx : Syntax) : CommandElabM Unit := do
+private partial def recordUsedSyntaxKinds (stx : Syntax) : CoreM Unit := do
   if let .node _ k .. := stx then
     -- do not record builtin parsers, they do not have to be imported
     if !(← Parser.builtinSyntaxNodeKindSetRef.get).contains k then

From 2d9bffbc314e432d77ddce1701a14c526edd1c59 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 15:38:07 +0200
Subject: [PATCH 4/8] fix `resetMessageLog` use

---
 src/Lean/Elab/BuiltinCommand.lean | 4 ----
 src/Lean/Elab/Command.lean        | 6 +++---
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index f93329e1762d..2140181818a4 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -543,10 +543,6 @@ open Lean.Parser.Command.InternalSyntax in
     -- TODO: this really shouldn't have to re-elaborate section vars... they should come
     -- pre-elaborated
     let omittedVars ← runTermElabM fun vars => do
-      Term.synthesizeSyntheticMVarsNoPostponing
-      -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
-      -- So, we use `Core.resetMessageLog`.
-      Core.resetMessageLog
       -- resolve each omit to variable user name or type pattern
       let elaboratedOmits : Array (Sum Name Expr) ← omits.mapM fun
         | `(ident| $id:ident) => pure <| Sum.inl id.getId
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 608c7fc95302..2e47c72fbc52 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -769,16 +769,16 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
   liftTermElabM <|
     Term.withAutoBoundImplicit <|
       Term.elabBinders scope.varDecls fun xs => do
+        let msgs ← Core.getMessageLog
         -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature
         -- If we don't use this checkpoint here, then auto-bound implicits in the postponed terms will not be handled correctly.
         Term.synthesizeSyntheticMVarsNoPostponing
+        -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
+        Core.setMessageLog msgs
         let mut sectionFVars := {}
         for uid in scope.varUIds, x in xs do
           sectionFVars := sectionFVars.insert uid x
         withReader ({ · with sectionFVars := sectionFVars }) do
-          -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
-          -- So, we use `Core.resetMessageLog`.
-          Core.resetMessageLog
           let xs ← Term.addAutoBoundImplicits xs none
           if xs.all (·.isFVar) then
             Term.withoutAutoBoundImplicit <| elabFn xs

From 5e29c8d79ccabfa118d57c5842bb6a36bb0f468b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 15:38:07 +0200
Subject: [PATCH 5/8] perf: optimize `monadLift`

---
 src/Lean/Elab/Command.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 2e47c72fbc52..1f4f872c466f 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -131,7 +131,7 @@ instance : MonadLift CoreM CommandElabM where
   monadLift x := private do
     let ds ← getThe DerivedState
     let (a, coreS) ← x.run ds.coreCtx ds.coreState
-    modify fun s => s.updateCore coreS
+    set { ds with toState := ds.toState.updateCore coreS, coreState := coreS }
     return a
 
 protected nonrec def CommandElabM.run (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception (α × State) := do

From 6b1418659b0226f5f531503e5d1e945b44da7f36 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 15:38:21 +0200
Subject: [PATCH 6/8] simplify

---
 src/Lean/Elab/Command.lean | 82 ++++++++++++++++----------------------
 1 file changed, 34 insertions(+), 48 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 1f4f872c466f..ef70ddd28f55 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -31,10 +31,6 @@ structure State where
   snapshotTasks  : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
-structure DerivedState extends State where
-  private coreCtx : Core.Context
-  private coreState : Core.State
-
 structure Context where
   fileName       : String
   fileMap        : FileMap
@@ -63,7 +59,7 @@ structure Context where
   -/
   suppressElabErrors : Bool := false
 
-abbrev CommandElabM := ReaderT Context $ StateRefT DerivedState $ EIO Exception
+abbrev CommandElabM := ReaderT Context $ StateRefT State $ EIO Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 structure Linter where
   run : Syntax → CommandElabM Unit
@@ -78,9 +74,22 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-private def DerivedState.derive (ctx : Context) (s : State) : DerivedState where
-  toState := s
-  coreCtx := {
+private def State.updateCore (s : State) (coreS : Core.State) : State :=
+  { s with
+    env                      := coreS.env
+    nextMacroScope           := coreS.nextMacroScope
+    ngen                     := coreS.ngen
+    auxDeclNGen              := coreS.auxDeclNGen
+    infoState                := coreS.infoState
+    traceState               := coreS.traceState
+    snapshotTasks            := coreS.snapshotTasks
+    messages                 := coreS.messages }
+
+private def liftCoreMDirect (x : CoreM α) : CommandElabM α := do
+  let ctx ← read
+  let s ← get
+  let scope := s.scopes.head!
+  let coreCtx := {
     fileName           := ctx.fileName
     fileMap            := ctx.fileMap
     currRecDepth       := ctx.currRecDepth
@@ -94,7 +103,7 @@ private def DerivedState.derive (ctx : Context) (s : State) : DerivedState where
     options            := scope.opts
     cancelTk?          := ctx.cancelTk?
     suppressElabErrors := ctx.suppressElabErrors }
-  coreState := {
+  let coreState := {
     env := s.env
     ngen := s.ngen
     auxDeclNGen := s.auxDeclNGen
@@ -104,40 +113,17 @@ private def DerivedState.derive (ctx : Context) (s : State) : DerivedState where
     snapshotTasks := s.snapshotTasks
     messages := s.messages
   }
-where
-  scope := s.scopes.head!
-
-private def State.updateCore (s : State) (coreS : Core.State) : State :=
-  { s with
-    env                      := coreS.env
-    nextMacroScope           := coreS.nextMacroScope
-    ngen                     := coreS.ngen
-    auxDeclNGen              := coreS.auxDeclNGen
-    infoState                := coreS.infoState
-    traceState               := coreS.traceState
-    snapshotTasks            := coreS.snapshotTasks
-    messages                 := coreS.messages }
-
-instance : MonadStateOf State CommandElabM where
-  get := return (← getThe DerivedState).toState
-  set s := private do set (DerivedState.derive (← read) s)
-  modifyGet f := private do
-    let ctx ← read
-    modifyGetThe DerivedState fun ds =>
-      let (a, s') := f ds.toState
-      (a, DerivedState.derive ctx s')
+  let (a, coreS) ← x.run coreCtx coreState
+  modify (·.updateCore coreS)
+  return a
 
 instance : MonadLift CoreM CommandElabM where
-  monadLift x := private do
-    let ds ← getThe DerivedState
-    let (a, coreS) ← x.run ds.coreCtx ds.coreState
-    set { ds with toState := ds.toState.updateCore coreS, coreState := coreS }
-    return a
+  monadLift := private liftCoreMDirect
+
+instance : MonadStateOf State CommandElabM := inferInstance
 
 protected nonrec def CommandElabM.run (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception (α × State) := do
-  let ds := DerivedState.derive ctx s
-  let (a, ds') ← x.run ctx |>.run ds
-  return (a, ds'.toState)
+  x.run ctx |>.run s
 
 protected def CommandElabM.run' (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception α := do
   (·.1) <$> x.run ctx s
@@ -229,17 +215,17 @@ instance : MonadQuotation CommandElabM where
   withFreshMacroScope := Command.withFreshMacroScope
 
 private def runCore (x : CoreM α) : CommandElabM α := do
-  let s ← getThe DerivedState
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let env := Kernel.resetDiag s.env
-  let coreCtx : Core.Context := { s.coreCtx with initHeartbeats := heartbeats }
-  let x : EIO _ _ := x.run coreCtx { s.coreState with env }
-  let (ea, coreS) ← liftM x
-  modify fun s => s.updateCore { coreS with
-    traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-  }
-  return ea
+  let env := Kernel.resetDiag (← getEnv)
+  liftM (m := CoreM) do
+    withReader ({ · with initHeartbeats := heartbeats }) do
+      modify ({ · with env })
+      let a ← x
+      modify fun s => { s with
+        traceState.traces        := s.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
+      }
+      return a
 
 def liftCoreM (x : CoreM α) : CommandElabM α := do
   MonadExcept.ofExcept (← runCore (observing x))

From 3f8388612c968a0d4af445c54773382bf96e6c17 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 16:38:25 +0200
Subject: [PATCH 7/8] simplify

---
 src/Lean/Elab/Command.lean | 35 +++--------------------------------
 1 file changed, 3 insertions(+), 32 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index ef70ddd28f55..9c45fea4face 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -17,18 +17,10 @@ public section
 
 namespace Lean.Elab.Command
 
-structure State where
-  env            : Environment
-  messages       : MessageLog := {}
+structure State extends Core.State where
   scopes         : List Scope := [{ header := "" }]
   usedQuotCtxts  : NameSet := {}
-  nextMacroScope : Nat := firstFrontendMacroScope + 1
   maxRecDepth    : Nat
-  ngen           : NameGenerator := {}
-  auxDeclNGen    : DeclNameGenerator := .ofPrefix .anonymous
-  infoState      : InfoState := {}
-  traceState     : TraceState := {}
-  snapshotTasks  : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
 structure Context where
@@ -74,17 +66,6 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-private def State.updateCore (s : State) (coreS : Core.State) : State :=
-  { s with
-    env                      := coreS.env
-    nextMacroScope           := coreS.nextMacroScope
-    ngen                     := coreS.ngen
-    auxDeclNGen              := coreS.auxDeclNGen
-    infoState                := coreS.infoState
-    traceState               := coreS.traceState
-    snapshotTasks            := coreS.snapshotTasks
-    messages                 := coreS.messages }
-
 private def liftCoreMDirect (x : CoreM α) : CommandElabM α := do
   let ctx ← read
   let s ← get
@@ -103,18 +84,8 @@ private def liftCoreMDirect (x : CoreM α) : CommandElabM α := do
     options            := scope.opts
     cancelTk?          := ctx.cancelTk?
     suppressElabErrors := ctx.suppressElabErrors }
-  let coreState := {
-    env := s.env
-    ngen := s.ngen
-    auxDeclNGen := s.auxDeclNGen
-    nextMacroScope := s.nextMacroScope
-    infoState := s.infoState
-    traceState := s.traceState
-    snapshotTasks := s.snapshotTasks
-    messages := s.messages
-  }
-  let (a, coreS) ← x.run coreCtx coreState
-  modify (·.updateCore coreS)
+  let (a, coreS) ← x.run coreCtx s.toState
+  modify ({ · with toState := coreS })
   return a
 
 instance : MonadLift CoreM CommandElabM where

From 564445eba9147b5b152e8cd1a2356ec30b861f4d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 18 Oct 2025 16:42:33 +0200
Subject: [PATCH 8/8] fix message log fix

---
 src/Lean/Elab/Command.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 9c45fea4face..a9d922f5a9b0 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -723,10 +723,10 @@ variable (n : Nat)
 -/
 def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
   let scope ← getScope
+  let msgs ← Core.getMessageLog
   liftTermElabM <|
     Term.withAutoBoundImplicit <|
       Term.elabBinders scope.varDecls fun xs => do
-        let msgs ← Core.getMessageLog
         -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature
         -- If we don't use this checkpoint here, then auto-bound implicits in the postponed terms will not be handled correctly.
         Term.synthesizeSyntheticMVarsNoPostponing