diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 4b190da087..fd521ce4c3 100644
--- 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
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 950a891850..ea610e5be4 100644
--- 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.
diff --git a/src/Lean/Data/NameMap/Basic.lean b/src/Lean/Data/NameMap/Basic.lean
index 3b0e196702..4aa4e2934a 100644
--- 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
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 1b99ab4aa8..250a270d0e 100644
--- 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
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 5146ba3c17..1fd3020cc3 100644
--- 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
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 1f8a13a20d..4428397f04 100644
--- 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
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index b13fe1db06..6a3d93bc39 100644
--- 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
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 59e8a0f776..3f850c68f1 100644
--- 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 }
 
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 1058bbe212..7eb5a0e7c4 100644
--- 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
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 7f3742843c..5ab432bc0b 100644
--- 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)
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 3d5d614d15..90fb52a360 100644
--- 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
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index cbe286ba31..280d4fca7b 100644
--- 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 }
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index bed7474f0d..d79cae6eda 100644
--- 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
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 1ff97aafa1..c63df3f917 100644
--- 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
 }
 
diff --git a/tests/lean/1275.lean.expected.out b/tests/lean/1275.lean.expected.out
index acbb2b89d9..47c51ee2a6 100644
--- 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 :=
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 2443f5b965..61906fc89f 100644
--- 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 :=
diff --git a/tests/lean/macroscopes.lean b/tests/lean/macroscopes.lean
index 1e0cb6a19e..1d03f4d59e 100644
--- 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;
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index 63694dba90..6e3e4b220b 100644
--- 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;
diff --git a/tests/lean/run/methodsRetInhabited.lean b/tests/lean/run/methodsRetInhabited.lean
index ac44b373f5..b7d3419a52 100644
--- 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
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index 3b4c56184d..3a108451f2 100644
--- 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
diff --git a/tests/pkg/rebuild/test.sh b/tests/pkg/rebuild/test.sh
index becede2639..06017a7b2a 100755
--- 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