perf: make macro scope numbering less dependent on surrounding context (#10027)

This PR changes macro scope numbering from per-module to per-command, ensuring that unrelated changes to other commands do not affect macro scopes generated by a command, which improves `prefer_native` hit rates on bootstrapping as well as avoids further rebuilds under the module system. In detail, instead of always using the current module name as a macro scope prefix, each command now introduces a new macro scope prefix (called "context") of the shape `<main module>._hygCtx_<uniq>` where `uniq` is a `UInt32` derived from the command but automatically incremented in case of conflicts (which must be local to the current module). In the current implementation, `uniq` is the hash of the declaration name, if any, or else the hash of the full command's syntax. Thus, it is always independent of syntactic changes to other commands (except in case of hash conflicts, which should only happen in practice for syntactically identical commands) and, in the case of declarations, also independent of syntactic changes to any private parts of the declaration.
2025-08-22 15:16:02 +02:00 · 2025-08-22 15:16:02 +02:00 · 51bba5338a
commit 51bba5338a
parent 561a4510b3
21 changed files with 176 additions and 103 deletions
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@ -4934,9 +4934,8 @@ def withRef? [Monad m] [MonadRef m] {α} (ref? : Option Syntax) (x : m α) : m
 class MonadQuotation (m : Type → Type) extends MonadRef m where
  /-- Get the fresh scope of the current macro invocation -/
  getCurrMacroScope : m MacroScope
-  /-- Get the module name of the current file. This is used to ensure that
-  hygienic names don't clash across multiple files. -/
-  getMainModule     : m Name
+  /-- Get the context name used in Note `Macro Scope Representation`. -/
+  getContext        : m Name
  /--
  Execute action in a new macro invocation context. This transformer should be
  used at all places that morally qualify as the beginning of a "macro call",
@ -4952,7 +4951,11 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where
  -/
  withFreshMacroScope {α : Type} : m α → m α

-export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
+export MonadQuotation (getCurrMacroScope withFreshMacroScope)
+
+-- TODO: delete after rebootstrap
+@[inherit_doc MonadQuotation.getContext]
+abbrev MonadQuotation.getMainModule := @MonadQuotation.getContext

 /-- Construct a synthetic `SourceInfo` from the `ref` in the monad state. -/
@[inline]
@ -4961,28 +4964,43 @@ def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo :=

 instance [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
  getCurrMacroScope   := liftM (m := m) getCurrMacroScope
-  getMainModule       := liftM (m := m) getMainModule
+  getContext          := liftM (m := m) MonadQuotation.getContext
  withFreshMacroScope := monadMap (m := m) withFreshMacroScope

 /-!
+# Note [Macro Scope Representation]
+
 We represent a name with macro scopes as
 ```
-<actual name>._@.(<module_name>.<scopes>)*.<module_name>._hyg.<scopes>
+<actual name>._@.(<ctx>.<scopes>)*.<ctx>._hyg.<scopes>
 ```
-Example: suppose the module name is `Init.Data.List.Basic`, and name is `foo.bla`, and macroscopes [2, 5]
+Example: suppose the context name is `Init.Data.List.Basic`, and name is `foo.bla`, and macroscopes [2, 5]
 ```
 foo.bla._@.Init.Data.List.Basic._hyg.2.5
 ```
+The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.

-We may have to combine scopes from different files/modules.
-The main modules being processed is always the right-most one.
-This situation may happen when we execute a macro generated in
-an imported file in the current file.
+The primary purpose of the context name is to differentiate macro scopes from different files as the
+numeric scopes are reset in each file. The current scope is always the right-most one. Scopes from
+multiple files may be collected when we execute a macro generated in an imported file in the current
+file.
 ```
 foo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4
 ```

 The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.
+In practice, we further specify the context name down to be unique per declaration so that the
+numeric scopes are not influenced by the elaboration of preceding declarations. This helps both with
+ensuring declaration names are more stable so that `prefer_native` can find the correct native
+symbol as well as making exported information in general more stable, avoiding rebuilds under the
+module system. Thus the actual encoding of the context name in the current implementation is
+```
+<main module>.<uniq>._hygCtx
+```
+where `<uniq>` is an identifier unique within the current module, set by
+`Command.withInitQuotContext`; see there for details. Thus we can assume the full context name to be
+unique throughout all modules and reset the numeric scopes whenever establishing a fresh context
+name.
 -/

 /-- Does this name have hygienic macro scopes? -/
@ -5030,8 +5048,8 @@ structure MacroScopesView where
  /-- All the name components `(<module_name>.<scopes>)*` from the imports
  concatenated together. -/
  imported   : Name
-  /-- The main module in which this identifier was parsed. -/
-  mainModule : Name
+  /-- The context name, a globally unique prefix. -/
+  ctx        : Name
  /-- The list of macro scopes. -/
  scopes     : List MacroScope

@ -5043,7 +5061,7 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
  match view.scopes with
  | List.nil      => view.name
  | List.cons _ _ =>
-    let base := (Name.mkStr (Name.appendCore (Name.appendCore (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
+    let base := (Name.mkStr (Name.appendCore (Name.appendCore (Name.mkStr view.name "_@") view.imported) view.ctx) "_hyg")
    view.scopes.foldl Name.mkNum base

 private def assembleParts : List Name → Name → Name
@ -5055,7 +5073,7 @@ private def assembleParts : List Name → Name → Name
 private def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView
  | n@(Name.str p str), parts =>
    match beq str "_@" with
-    | true  => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
+    | true  => { name := p, ctx := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
    | false => extractImported scps mainModule p (List.cons n parts)
  | n@(Name.num p _), parts => extractImported scps mainModule p (List.cons n parts)
  | _,                    _     => panic "Error: unreachable @ extractImported"
@ -5063,7 +5081,7 @@ private def extractImported (scps : List MacroScope) (mainModule : Name) : Name
 private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
  | n@(Name.str p str), parts =>
    match beq str "_@" with
-    | true  => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
+    | true  => { name := p, ctx := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
    | false => extractMainModule scps p (List.cons n parts)
  | n@(Name.num _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
  | _,                    _   => panic "Error: unreachable @ extractMainModule"
@ -5080,23 +5098,23 @@ private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
 def extractMacroScopes (n : Name) : MacroScopesView :=
  match n.hasMacroScopes with
  | true  => extractMacroScopesAux n List.nil
-  | false => { name := n, scopes := List.nil, imported := Name.anonymous, mainModule := Name.anonymous }
+  | false => { name := n, scopes := List.nil, imported := Name.anonymous, ctx := Name.anonymous }

-/-- Add a new macro scope onto the name `n`, in the given `mainModule`. -/
-def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
+/-- Add a new macro scope onto the name `n`, in the given `ctx`. -/
+def addMacroScope (ctx : Name) (n : Name) (scp : MacroScope) : Name :=
  match n.hasMacroScopes with
  | true =>
    let view := extractMacroScopes n
-    match beq view.mainModule mainModule with
+    match beq view.ctx ctx with
    | true  => Name.mkNum n scp
    | false =>
      { view with
-        imported   := view.scopes.foldl Name.mkNum (Name.appendCore view.imported view.mainModule)
-        mainModule := mainModule
+        imported   := view.scopes.foldl Name.mkNum (Name.appendCore view.imported view.ctx)
+        ctx := ctx
        scopes     := List.cons scp List.nil
      }.review
  | false =>
-    Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
+    Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") ctx) "_hyg") scp

 /--
 Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
@ -5127,9 +5145,9 @@ Add a new macro scope onto the name `n`, using the monad state to supply the
 main module and current macro scope.
 -/
@[inline] def MonadQuotation.addMacroScope {m : Type → Type} [MonadQuotation m] [Monad m] (n : Name) : m Name :=
-  bind getMainModule     fun mainModule =>
+  bind MonadQuotation.getContext fun ctx =>
  bind getCurrMacroScope fun scp =>
-  pure (Lean.addMacroScope mainModule n scp)
+  pure (Lean.addMacroScope ctx n scp)

 namespace Syntax

@ -5174,8 +5192,8 @@ structure Context where
  /-- An opaque reference to the `Methods` object. This is done to break a
  dependency cycle: the `Methods` involve `MacroM` which has not been defined yet. -/
  methods        : MethodsRef
-  /-- The currently parsing module. -/
-  mainModule     : Name
+  /-- The quotation context name for `MonadQuotation.getContext`. -/
+  quotContext    : Name
  /-- The current macro scope. -/
  currMacroScope : MacroScope
  /-- The current recursion depth. -/
@ -5230,11 +5248,6 @@ instance : MonadRef MacroM where
  getRef     := bind read fun ctx => pure ctx.ref
  withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x

-/-- Add a new macro scope to the name `n`. -/
-def addMacroScope (n : Name) : MacroM Name :=
-  bind read fun ctx =>
-  pure (Lean.addMacroScope ctx.mainModule n ctx.currMacroScope)
-
 /-- Throw an `unsupportedSyntax` exception. -/
 def throwUnsupported {α} : MacroM α :=
  throw Exception.unsupportedSyntax
@ -5268,9 +5281,13 @@ scope is fresh.

 instance : MonadQuotation MacroM where
  getCurrMacroScope ctx := pure ctx.currMacroScope
-  getMainModule     ctx := pure ctx.mainModule
+  getContext        ctx := pure ctx.quotContext
  withFreshMacroScope   := Macro.withFreshMacroScope

+/-- Add a new macro scope to the name `n`. -/
+def addMacroScope (n : Name) : MacroM Name :=
+  MonadQuotation.addMacroScope n
+
 /-- The opaque methods that are available to `MacroM`. -/
 structure Methods where
  /-- Expands macros in the given syntax. A return value of `none` means there
@ -5368,7 +5385,7 @@ instance : MonadQuotation UnexpandM where
  withRef ref x       := withReader (fun _ => ref) x
  -- unexpanders should not need to introduce new names
  getCurrMacroScope   := pure 0
-  getMainModule       := pure `_fakeMod
+  getContext          := pure `_fakeMod
  withFreshMacroScope := id

 end PrettyPrinter
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@ -230,6 +230,7 @@ structure Context where
  openDecls      : List OpenDecl := []
  initHeartbeats : Nat := 0
  maxHeartbeats  : Nat := getMaxHeartbeats options
+  quotContext    : Name := .anonymous
  currMacroScope : MacroScope := firstFrontendMacroScope
  /--
  If `diag := true`, different parts of the system collect diagnostics.
@ -322,7 +323,7 @@ protected def withFreshMacroScope (x : CoreM α) : CoreM α := do

 instance : MonadQuotation CoreM where
  getCurrMacroScope   := return (← read).currMacroScope
-  getMainModule       := return (← getEnv).mainModule
+  getContext          := return (← read).quotContext
  withFreshMacroScope := Core.withFreshMacroScope

 instance : Elab.MonadInfoTree CoreM where
@ -410,8 +411,8 @@ def SavedState.restore (b : SavedState) : CoreM Unit :=
  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }

 private def mkFreshNameImp (n : Name) : CoreM Name := do
-  let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
-  return addMacroScope (← getEnv).mainModule n fresh
+  withFreshMacroScope do
+    MonadQuotation.addMacroScope n

 /--
 Creates a name from `n` that is guaranteed to be unique.
--- a/src/Lean/Data/NameMap/Basic.lean
+++ b/src/Lean/Data/NameMap/Basic.lean
@ -109,13 +109,13 @@ end NameHashSet
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
  v₁.name.isPrefixOf v₂.name &&
  v₁.scopes == v₂.scopes &&
-  v₁.mainModule == v₂.mainModule &&
+  v₁.ctx == v₂.ctx &&
  v₁.imported == v₂.imported

 def MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) : Bool :=
  v₁.name.isSuffixOf v₂.name &&
  v₁.scopes == v₂.scopes &&
-  v₁.mainModule == v₂.mainModule &&
+  v₁.ctx == v₂.ctx &&
  v₁.imported == v₂.imported

 end Lean
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@ -92,6 +92,7 @@ structure State where
  env            : Environment
  messages       : MessageLog := {}
  scopes         : List Scope := [{ header := "" }]
+  usedQuotCtxts  : NameSet := {}
  nextMacroScope : Nat := firstFrontendMacroScope + 1
  maxRecDepth    : Nat
  ngen           : NameGenerator := {}
@ -107,6 +108,7 @@ structure Context where
  currRecDepth   : Nat := 0
  cmdPos         : String.Pos := 0
  macroStack     : MacroStack := []
+  quotContext?   : Option Name := none
  currMacroScope : MacroScope := firstFrontendMacroScope
  ref            : Syntax := Syntax.missing
  /--
@ -217,6 +219,18 @@ instance : MonadDeclNameGenerator CommandElabM where
  getDeclNGen := return (← get).auxDeclNGen
  setDeclNGen ngen := modify fun s => { s with auxDeclNGen := ngen }

+protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
+protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
+
+protected def withFreshMacroScope {α} (x : CommandElabM α) : CommandElabM α := do
+  let fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }))
+  withReader (fun ctx => { ctx with currMacroScope := fresh }) x
+
+instance : MonadQuotation CommandElabM where
+  getCurrMacroScope   := Command.getCurrMacroScope
+  getContext          := do (← read).quotContext?.getDM getMainModule
+  withFreshMacroScope := Command.withFreshMacroScope
+
 private def runCore (x : CoreM α) : CommandElabM α := do
  let s ← get
  let ctx ← read
@ -232,6 +246,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
    currNamespace      := scope.currNamespace
    openDecls          := scope.openDecls
    initHeartbeats     := heartbeats
+    quotContext        := (← MonadQuotation.getMainModule)
    currMacroScope     := ctx.currMacroScope
    options            := scope.opts
    cancelTk?          := ctx.cancelTk?
@ -411,18 +426,6 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
      lintAct infoSt
  logSnapshotTask { stx? := none, task, cancelTk? := cancelTk }

-protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
-protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
-
-protected def withFreshMacroScope {α} (x : CommandElabM α) : CommandElabM α := do
-  let fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }))
-  withReader (fun ctx => { ctx with currMacroScope := fresh }) x
-
-instance : MonadQuotation CommandElabM where
-  getCurrMacroScope   := Command.getCurrMacroScope
-  getMainModule       := Command.getMainModule
-  withFreshMacroScope := Command.withFreshMacroScope
-
 /--
 Registers a command elaborator for the given syntax node kind.

@ -479,7 +482,6 @@ def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : Com
    withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x

 instance : MonadMacroAdapter CommandElabM where
-  getCurrMacroScope := getCurrMacroScope
  getNextMacroScope := return (← get).nextMacroScope
  setNextMacroScope next := modify fun s => { s with nextMacroScope := next }

@ -611,6 +613,43 @@ builtin_initialize
  registerTraceClass `Elab.info
  registerTraceClass `Elab.snapshotTree

+/--
+If `hint?` is `some hint`, establishes a new context for macro scope naming and runs `act` in it,
+otherwise runs `act` directly without changes.
+
+Context names as documented in Note `Macro Scope Representation` help with avoiding rebuilds and
+`prefer_native` lookup misses from macro scopes in declaration names and other exported information.
+This function establishes a new context with a globally unique name by combining the name of the
+current module with `hint` while also checking for previously used `hint`s in the same module.
+Thus `hint` does not need to be unique but ensuring it is usually unique helps with keeping the
+context name stable.
+
+In the current implementation, we call `withInitQuotContext` once in `elabCommandTopLevel` using the
+source input of the command as the hint. This helps with keeping macro scopes stable on changes to
+other parts of the file but not on changes to the command itself. Thus in each *declaration*
+elaborator we call `withInitQuotContext` again with the declaration name(s) as a hint so that
+changes to any other part of the declaration do not change the context name.
+-/
+def withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) : CommandElabM Unit := do
+  let some hint := hint?
+    | act
+  let mut idx := hint.toUInt32.toNat
+  while (← get).usedQuotCtxts.contains ((← getMainModule).num idx |>.str "_hygCtx") do
+    idx := idx + 1
+  let quotCtx := (← getMainModule).num idx |>.str "_hygCtx"
+  let nextMacroScope := (← get).nextMacroScope
+  try
+    modify fun st => { st with
+      usedQuotCtxts  := st.usedQuotCtxts.insert quotCtx
+      nextMacroScope := firstFrontendMacroScope + 1
+    }
+    withReader (fun ctx => { ctx with
+      quotContext?   := some quotCtx
+      currMacroScope := firstFrontendMacroScope
+    }) act
+  finally
+    modify ({ · with nextMacroScope })
+
 /--
 `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
 macro expansion etc.
@ -618,6 +657,9 @@ macro expansion etc.
 def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
  withReader ({ · with suppressElabErrors :=
    stx.hasMissing && !showPartialSyntaxErrors.get (← getOptions) }) do
+  -- initialize quotation context using hash of input string
+  let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false)
+  withInitQuotContext (ss?.map (hash ·.toString.trim)) do
  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
  let initInfoTrees ← getResetInfoTrees
  try
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@ -38,8 +38,8 @@ private def setDeclIdName (declId : Syntax) (nameNew : Name) : Syntax :=
  else
    declId.setArg 0 idStx

-/-- Return `true` if `stx` is a `Command.declaration`, and it is a definition that always has a name. -/
-private def isNamedDef (stx : Syntax) : Bool :=
+/-- Return `true` if `stx` is a `Command.declaration`, and it is a declaration that always has a name. -/
+private def isNamedDecl (stx : Syntax) : Bool :=
  if !stx.isOfKind ``Lean.Parser.Command.declaration then
    false
  else
@ -55,16 +55,16 @@ private def isNamedDef (stx : Syntax) : Bool :=
    k == ``Lean.Parser.Command.structure

 /-- Return `true` if `stx` is an `instance` declaration command -/
-private def isInstanceDef (stx : Syntax) : Bool :=
+private def isInstanceDecl (stx : Syntax) : Bool :=
  stx.isOfKind ``Lean.Parser.Command.declaration &&
  stx[1].getKind == ``Lean.Parser.Command.instance

-/-- Return `some name` if `stx` is a definition named `name` -/
-private def getDefName? (stx : Syntax) : Option Name := do
-  if isNamedDef stx then
+/-- Return `some name` if `stx` is a declaration named `name` -/
+private def getDeclName? (stx : Syntax) : Option Name := do
+  if isNamedDecl stx then
    let (id, _) := expandDeclIdCore stx[1][1]
    some id
-  else if isInstanceDef stx then
+  else if isInstanceDecl stx then
    let optDeclId := stx[1][3]
    if optDeclId.isNone then none
    else
@ -74,13 +74,13 @@ private def getDefName? (stx : Syntax) : Option Name := do
    none

 /--
-Update the name of the given definition.
+Update the name of the given declaration.
 This function assumes `stx` is not a nameless instance.
 -/
-private def setDefName (stx : Syntax) (name : Name) : Syntax :=
-  if isNamedDef stx then
+private def setDeclName (stx : Syntax) (name : Name) : Syntax :=
+  if isNamedDecl stx then
    stx.setArg 1 <| stx[1].setArg 1 <| setDeclIdName stx[1][1] name
-  else if isInstanceDef stx then
+  else if isInstanceDecl stx then
    -- We never set the name of nameless instance declarations
    assert! !stx[1][3].isNone
    stx.setArg 1 <| stx[1].setArg 3 <| stx[1][3].setArg 0 <| setDeclIdName stx[1][3][0] name
@ -92,14 +92,14 @@ private def setDefName (stx : Syntax) (name : Name) : Syntax :=
  Remark: if the id starts with `_root_`, we return `none`.
 -/
 private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax)) := do
-  let some name := getDefName? stx | return none
+  let some name := getDeclName? stx | return none
  if (`_root_).isPrefixOf name then
    ensureValidNamespace (name.replacePrefix `_root_ Name.anonymous)
    return none
  let scpView := extractMacroScopes name
  match scpView.name with
  | .str .anonymous _ => return none
-  | .str pre shortName => return some (pre, setDefName stx { scpView with name := .mkSimple shortName }.review)
+  | .str pre shortName => return some (pre, setDeclName stx { scpView with name := .mkSimple shortName }.review)
  | _ => return none

 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
@ -166,6 +166,9 @@ def elabDeclaration : CommandElab := fun stx => do
    -- only case implementing incrementality currently
    elabMutualDef #[stx]
  else withoutCommandIncrementality true do
+    -- use hash of declaration name, if any, as stable quot context; `elabMutualDef` has its own
+    -- handling
+    withInitQuotContext (getDeclName? stx |>.map hash) do
    let modifiers ← elabModifiers modifiers
    withExporting (isExporting := modifiers.isInferredPublic (← getEnv)) do
      if declKind == ``Lean.Parser.Command.«axiom» then
@ -178,7 +181,7 @@ def elabDeclaration : CommandElab := fun stx => do
        throwError "unexpected declaration"

 /-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
-private def isMutualDef (stx : Syntax) : Bool :=
+private def isMutualDefLike (stx : Syntax) : Bool :=
  stx[1].getArgs.all fun elem =>
    let decl := elem[1]
    isDefLike decl
@ -239,10 +242,10 @@ def expandMutualNamespace : Macro := fun stx => do
  let common := findCommonPrefix nss.toList
  if common.isAnonymous then Macro.throwUnsupported
  let elemsNew ← stx[1].getArgs.mapM fun elem => do
-    let some name := getDefName? elem | unreachable!
+    let some name := getDeclName? elem | unreachable!
    let view := extractMacroScopes name
    let nameNew := { view with name := view.name.replacePrefix common .anonymous }.review
-    return setDefName elem nameNew
+    return setDeclName elem nameNew
  let ns := mkIdentFrom stx common
  let stxNew := stx.setArg 1 (mkNullNode elemsNew)
  `(namespace $ns $(⟨stxNew⟩) end $ns)
@ -282,7 +285,7 @@ def expandMutualPreamble : Macro := fun stx =>
@[builtin_command_elab «mutual», builtin_incremental]
 def elabMutual : CommandElab := fun stx => do
  withExporting (isExporting := (← getScope).isPublic) do
-  if isMutualDef stx then
+  if isMutualDefLike stx then
    -- only case implementing incrementality currently
    elabMutualDef stx[1].getArgs
  else withoutCommandIncrementality true do
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@ -1441,6 +1441,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
    -- no non-fatal diagnostics at this point
    snap.new.resolve <| .ofTyped defsParsedSnap
  let sc ← getScope
+  -- use hash of all names as stable quot context
+  withInitQuotContext (some (hash (views.map (·.declId[0].getId)))) do
  runTermElabM fun vars => do
    Term.elabMutualDef vars sc views
    Term.logGoalsAccomplishedSnapshotTask views defsParsedSnap
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@ -144,7 +144,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
      preresolved
    let val := quote val
    -- `scp` is bound in stxQuot.expand
-    `(Syntax.ident info $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
+    `(Syntax.ident info $(quote rawVal) (addMacroScope quotCtx $val scp) $(quote preresolved))
  -- if antiquotation, insert contents as-is, else recurse
  | stx@(Syntax.node _ k _) => do
    if let some (k, _) := stx.antiquotKind? then
@ -243,7 +243,7 @@ def mkSyntaxQuotation (stx : Syntax) (kind : Name) : TermElabM Syntax := do
     including it literally in a syntax quotation. -/
  `(Bind.bind MonadRef.mkInfoFromRefPos (fun info =>
      Bind.bind getCurrMacroScope (fun scp =>
-        Bind.bind getMainModule (fun mainModule => Pure.pure (@TSyntax.mk $(quote kind) $stx)))))
+        Bind.bind MonadQuotation.getContext (fun quotCtx => Pure.pure (@TSyntax.mk $(quote kind) $stx)))))
  /- NOTE: It may seem like the newly introduced binding `scp` may accidentally
     capture identifiers in an antiquotation introduced by `quoteSyntax`. However,
     note that the syntax quotation above enjoys the same hygiene guarantees as
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@ -1484,7 +1484,6 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
  | elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns

 instance : MonadMacroAdapter TermElabM where
-  getCurrMacroScope := getCurrMacroScope
  getNextMacroScope := return (← getThe Core.State).nextMacroScope
  setNextMacroScope next := modifyThe Core.State fun s => { s with nextMacroScope := next }

--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@ -25,17 +25,17 @@ def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format
  Std.format <|
    if view.scopes.isEmpty then
      view.name
-    else if view.mainModule == mainModule then
+    else if view.ctx == mainModule then
      view.scopes.foldl Name.mkNum (view.name ++ view.imported)
    else
-      view.scopes.foldl Name.mkNum (view.name ++ view.imported ++ view.mainModule)
+      view.scopes.foldl Name.mkNum (view.name ++ view.imported ++ view.ctx)

 /--
 Two names are from the same lexical scope if their scoping information modulo `MacroScopesView.name`
 is equal.
 -/
 def MacroScopesView.equalScope (a b : MacroScopesView) : Bool :=
-  a.scopes == b.scopes && a.mainModule == b.mainModule && a.imported == b.imported
+  a.scopes == b.scopes && a.ctx == b.ctx && a.imported == b.imported

 namespace Elab

@ -161,14 +161,12 @@ def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Ex
      | ex                                => return (e.declName, Except.error ex)
  return none

-class MonadMacroAdapter (m : Type → Type) where
-  getCurrMacroScope                  : m MacroScope
+class MonadMacroAdapter (m : Type → Type) extends MonadQuotation m where
  getNextMacroScope                  : m MacroScope
  setNextMacroScope                  : MacroScope → m Unit

@[always_inline]
-instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
-  getCurrMacroScope := liftM (MonadMacroAdapter.getCurrMacroScope : m _)
+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 _)
 }
@ -190,8 +188,8 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
  }
  match x { methods        := methods
            ref            := ← getRef
-            currMacroScope := ← MonadMacroAdapter.getCurrMacroScope
-            mainModule     := env.mainModule
+            currMacroScope := ← MonadQuotation.getCurrMacroScope
+            quotContext    := ← MonadQuotation.getContext
            currRecDepth   := ← MonadRecDepth.getRecDepth
            maxRecDepth    := ← MonadRecDepth.getMaxRecDepth
          } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@ -2590,6 +2590,10 @@ class MonadEnv (m : Type → Type) where

 export MonadEnv (getEnv modifyEnv)

+/-- Returns the module name of the current file. -/
+def getMainModule [Monad m] [MonadEnv m] : m Name :=
+  return (← getEnv).header.mainModule
+
@[always_inline]
 instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
  getEnv    := liftM (getEnv : m Environment)
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@ -39,7 +39,7 @@ instance : MonadQuotation Unhygienic where
  getRef              := return (← read).ref
  withRef             := fun ref => withReader ({ · with ref := ref })
  getCurrMacroScope   := return (← read).scope
-  getMainModule       := pure `UnhygienicMain
+  getContext          := pure `UnhygienicMain
  withFreshMacroScope := fun x => do
    let fresh ← modifyGet fun n => (n, n + 1)
    withReader ({ · with scope := fresh}) x
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@ -1053,7 +1053,7 @@ def getFVarFromUserName (userName : Name) : MetaM Expr := do
 Lift a `MkBindingM` monadic action `x` to `MetaM`.
 -/
@[inline] def liftMkBindingM (x : MetavarContext.MkBindingM α) : MetaM α := do
-  match x { lctx := (← getLCtx), mainModule := (← getEnv).mainModule } { mctx := (← getMCtx), ngen := (← getNGen), nextMacroScope := (← getThe Core.State).nextMacroScope } with
+  match x { lctx := (← getLCtx), quotContext := (← readThe Core.Context).quotContext } { mctx := (← getMCtx), ngen := (← getNGen), nextMacroScope := (← getThe Core.State).nextMacroScope } with
  | .ok e sNew => do
    setMCtx sNew.mctx
    modifyThe Core.State fun s => { s with ngen := sNew.ngen, nextMacroScope := sNew.nextMacroScope }
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@ -937,7 +937,7 @@ structure State where
  cache          : Std.HashMap ExprStructEq Expr := {}

 structure Context where
-  mainModule         : Name
+  quotContext        : Name
  preserveOrder      : Bool
  /-- When creating binders for abstracted metavariables, we use the following `BinderInfo`. -/
  binderInfoForMVars : BinderInfo := BinderInfo.implicit
@ -953,7 +953,7 @@ instance : MonadMCtx M where

 private def mkFreshBinderName (n : Name := `x) : M Name := do
  let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
-  return addMacroScope (← read).mainModule n fresh
+  return addMacroScope (← read).quotContext n fresh

 def preserveOrder : M Bool :=
  return (← read).preserveOrder
@ -1325,20 +1325,20 @@ def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Exp
 end MkBinding

 structure MkBindingM.Context where
-  mainModule : Name
-  lctx       : LocalContext
+  quotContext : Name
+  lctx        : LocalContext

 abbrev MkBindingM := ReaderT MkBindingM.Context MkBinding.MCore

 def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBindingM Expr := fun ctx =>
-  MkBinding.elimMVarDeps xs e { preserveOrder, mainModule := ctx.mainModule }
+  MkBinding.elimMVarDeps xs e { preserveOrder, quotContext := ctx.quotContext }

 def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun ctx =>
-  MkBinding.revert xs mvarId { preserveOrder, mainModule := ctx.mainModule }
+  MkBinding.revert xs mvarId { preserveOrder, quotContext := ctx.quotContext }

 def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr := fun ctx =>
  let mvarIdsToAbstract := xs.foldl (init := {}) fun s x => if x.isMVar then s.insert x.mvarId! else s
-  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce generalizeNondepLet { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
+  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce generalizeNondepLet { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, quotContext := ctx.quotContext }

@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (generalizeNondepLet := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
  mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce generalizeNondepLet binderInfoForMVars
@ -1347,10 +1347,10 @@ def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool :=
  mkBinding (isLambda := false) xs e usedOnly usedLetOnly false generalizeNondepLet binderInfoForMVars

@[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
-  MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }
+  MkBinding.abstractRange xs n e { preserveOrder := false, quotContext := ctx.quotContext }

@[inline] def collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) (generalizeNondepLet := true) : MkBindingM (Array Expr) := fun ctx =>
-  MkBinding.collectForwardDeps ctx.lctx toRevert generalizeNondepLet { preserveOrder, mainModule := ctx.mainModule }
+  MkBinding.collectForwardDeps ctx.lctx toRevert generalizeNondepLet { preserveOrder, quotContext := ctx.quotContext }

 /--
  `isWellFormed lctx e` returns true iff
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@ -219,7 +219,7 @@ def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
 -- so give a trivial implementation.
 instance : MonadQuotation ParenthesizerM := {
  getCurrMacroScope   := pure default
-  getMainModule       := pure default
+  getContext          := pure default
  withFreshMacroScope := fun x => x
 }

--- a/tests/lean/1275.lean.expected.out
+++ b/tests/lean/1275.lean.expected.out
@ -1,7 +1,7 @@
 fun x => do
  let info ← MonadRef.mkInfoFromRefPos
  let scp ← getCurrMacroScope
-  let mainModule ← getMainModule
+  let quotCtx ← MonadQuotation.getContext
  pure
      {
        raw :=
@ -12,7 +12,7 @@ true
 fun x => do
  let info ← MonadRef.mkInfoFromRefPos
  let scp ← getCurrMacroScope
-  let mainModule ← getMainModule
+  let quotCtx ← MonadQuotation.getContext
  pure
      {
        raw :=
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@ -64,7 +64,7 @@ Note: You can use `set_option quotPrecheck false` to disable this check.
 fun e => do
  let info ← MonadRef.mkInfoFromRefPos
  let scp ← getCurrMacroScope
-  let mainModule ← getMainModule
+  let quotCtx ← MonadQuotation.getContext
  pure
      {
        raw :=
--- a/tests/lean/macroscopes.lean
+++ b/tests/lean/macroscopes.lean
@ -27,12 +27,12 @@ let x := addMacroScope `foo x 4;
 IO.println $ x;
 let x := addMacroScope `foo x 5;
 let v := extractMacroScopes x;
-check (v.mainModule == `foo);
+check (v.ctx == `foo);
 IO.println $ x;
 let x := addMacroScope `bla.bla x 6;
 IO.println $ x;
 let v := extractMacroScopes x;
-check (v.mainModule == `bla.bla);
+check (v.ctx == `bla.bla);
 let x := addMacroScope `bla.bla x 7;
 IO.println $ x;
 let v := extractMacroScopes x;
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@ -13,12 +13,12 @@
        do
        let info ← Lean.MonadRef.mkInfoFromRefPos
        let scp ← Lean.getCurrMacroScope
-        let mainModule ← Lean.getMainModule
+        let quotCtx ← Lean.MonadQuotation.getContext
        pure
            {
                raw :=
                  Lean.Syntax.node2 info `Lean.Parser.Term.app
-                    (Lean.Syntax.ident info "Nat.add".toSubstring' (Lean.addMacroScope mainModule `Nat.add scp)
+                    (Lean.Syntax.ident info "Nat.add".toSubstring' (Lean.addMacroScope quotCtx `Nat.add scp)
                      [Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add])
                    (Lean.Syntax.node2 info `null lhs.raw rhs.raw) }.raw
      else
@ -40,7 +40,7 @@
            Lean.withRef f.raw do
              let info ← Lean.MonadRef.mkInfoFromRefPos
              let _ ← Lean.getCurrMacroScope
-              let _ ← Lean.getMainModule
+              let _ ← Lean.MonadQuotation.getContext
              pure { raw := Lean.Syntax.node3 info `«term_+++_» lhs.raw (Lean.Syntax.atom info "+++") rhs.raw }.raw
          else
            have __discr := __discr.getArg 1;
--- a/tests/lean/run/methodsRetInhabited.lean
+++ b/tests/lean/run/methodsRetInhabited.lean
@ -2,7 +2,7 @@ open Lean

 def exec (x : MacroM α) : Option α :=
  match x {
-      mainModule := `Expander
+      quotContext := `Expander
      currMacroScope := 0
      ref := default
      methods := default } { macroScope := 0 } with
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@ -19,7 +19,7 @@ inst✝ inst : α
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.74 : Inhabited α
+inst.3 : Inhabited α
 inst inst : α
 ⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder
--- a/tests/pkg/rebuild/test.sh
+++ b/tests/pkg/rebuild/test.sh
@ -16,6 +16,13 @@ set_option compiler.small 0
 public def hello := "world"

 public def testSpec (xs : List Nat) : List Nat := xs.map (fun x => x + 1)
+
+-- Public macro scopes such as from unnamed parameters and deriving handlers should not cause
+-- rebuilds on changes above.
+public def macroScopes : Nat -> Nat := id
+
+public inductive Foo
+deriving Repr
 EOF

 lake build