feat: automatic extension names

src/Lean/Attributes.lean

@@ -138,7 +138,7 @@ structure TagAttribute where
 def registerTagAttribute (name : Name) (descr : String)
     (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) : IO TagAttribute := do
   let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
-    name            := name
+    name            := ref
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameSet) n => s.insert n
@@ -191,7 +191,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
 
 def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
-    name            := impl.name
+    name            := impl.ref
     mkInitial       := pure {}
     addImportedFn   := fun s => impl.afterImport s *> pure {}
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
@@ -245,12 +245,12 @@ structure EnumAttributes (α : Type) where
   ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
   deriving Inhabited
 
-def registerEnumAttributes [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α))
+def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
     (validate : Name → α → AttrM Unit := fun _ _ => pure ())
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
     (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
-    name            := extName
+    name            := ref
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
@@ -366,7 +366,6 @@ private def addAttrEntry (s : AttributeExtensionState) (e : AttributeExtensionOL
 
 builtin_initialize attributeExtension : AttributeExtension ←
   registerPersistentEnvExtension {
-    name            := `attrExt
     mkInitial       := AttributeExtension.mkInitial
     addImportedFn   := AttributeExtension.addImported
     addEntryFn      := addAttrEntry

src/Lean/AuxRecursor.lean

@@ -19,7 +19,7 @@ def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSu
 def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
 def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
 
-builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension `auxRec
+builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
 @[export lean_mark_aux_recursor]
 def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
@@ -47,7 +47,7 @@ def isRecOnRecursor (env : Environment) (declName : Name) : Bool :=
 def isBRecOnRecursor (env : Environment) (declName : Name) : Bool :=
   isAuxRecursorWithSuffix env declName brecOnSuffix
 
-builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension `noConf
+builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
 @[export lean_mark_no_confusion]
 def markNoConfusion (env : Environment) (n : Name) : Environment :=

src/Lean/Class.lean

@@ -54,7 +54,6 @@ Type class environment extension
 -- TODO: add support for scoped instances
 builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ←
   registerSimplePersistentEnvExtension {
-    name          := `classExt
     addEntryFn    := ClassState.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch
   }

src/Lean/Compiler/CSimpAttr.lean

@@ -26,7 +26,6 @@ def State.switch : State → State
 
 builtin_initialize ext : SimpleScopedEnvExtension Entry State ←
   registerSimpleScopedEnvExtension {
-    name           := `csimp
     initial        := {}
     addEntry       := fun { map, thmNames } { fromDeclName, toDeclName, thmName } => { map := map.insert fromDeclName toDeclName, thmNames := thmNames.insert thmName }
     finalizeImport := fun s => s.switch

src/Lean/Compiler/IR/CompilerM.lean

@@ -81,7 +81,6 @@ private def mkEntryArray (decls : List Decl) : Array Decl :=
 
 builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
   registerSimplePersistentEnvExtension {
-    name       := `IRDecls,
     addImportedFn := fun as =>
        let m : DeclMap := mkStateFromImportedEntries (fun s (d : Decl) => s.insert d.name d) {} as
        m.switch,

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -126,7 +126,6 @@ abbrev FunctionSummaries := SMap FunId Value
 
 builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries ←
   registerSimplePersistentEnvExtension {
-    name       := `unreachBranchesFunSummary,
     addImportedFn := fun as =>
       let cache : FunctionSummaries := mkStateFromImportedEntries (fun s (p : FunId × Value) => s.insert p.1 p.2) {} as
       cache.switch,

src/Lean/Compiler/InlineAttrs.lean

@@ -32,7 +32,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
   return true
 
 builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ←
-  registerEnumAttributes `inlineAttrs
+  registerEnumAttributes
     [(`inline, "mark definition to always be inlined", InlineAttributeKind.inline),
      (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", InlineAttributeKind.inlineIfReduce),
      (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline),

src/Lean/Compiler/LCNF/Passes.lean

@@ -69,7 +69,6 @@ def runImportedDecls (importedDeclNames : Array (Array Name)) : CoreM PassManage
 
 builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassManager) (List Name × PassManager) ←
   registerPersistentEnvExtension {
-    name := `cpass
     mkInitial := return ([], builtinPassManager)
     addImportedFn := fun ns => return ([], ← ImportM.runCoreM <| runImportedDecls ns)
     addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew)

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -22,7 +22,7 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
 
 abbrev DeclExt := PersistentEnvExtension Decl Decl DeclExtState
 
-def mkDeclExt (name : Name) : IO DeclExt := do
+def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
   registerPersistentEnvExtension {
     name            := name
     mkInitial       := return {}
@@ -33,8 +33,8 @@ def mkDeclExt (name : Name) : IO DeclExt := do
       sortDecls decls
   }
 
-builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt `compBaseDecls
-builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt `compMonoDecls
+builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
+builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
 
 def getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) : Option Decl :=
   match env.getModuleIdxFor? declName with

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -384,7 +384,6 @@ structure FolderEntry extends FolderOleanEntry where
 
 builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderOleanEntry × SMap Name Folder) ←
   registerPersistentEnvExtension {
-    name := `cfolder
     mkInitial := return ([], builtinFolders)
     addImportedFn := fun entriesArray => do
       let ctx ← read

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -74,7 +74,6 @@ Remark: we only store information for declarations that will be specialized.
 -/
 builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecState ←
   registerSimplePersistentEnvExtension {
-    name          := `specInfoExt
     addEntryFn    := SpecState.addEntry
     addImportedFn := fun es => mkStateFromImportedEntries SpecState.addEntry {} es |>.switch
   }

src/Lean/Compiler/NoncomputableAttr.lean

@@ -7,7 +7,7 @@ import Lean.Environment
 
 namespace Lean
 
-builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension `noncomputable
+builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
 /-- Mark in the environment extension that the given declaration has been declared by the user as `noncomputable`. -/
 def addNoncomputable (env : Environment) (declName : Name) : Environment :=

src/Lean/Compiler/Specialize.lean

@@ -106,7 +106,6 @@ end SpecState
 
 builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecState ←
   registerSimplePersistentEnvExtension {
-    name          := `specExt,
     addEntryFn    := SpecState.addEntry,
     addImportedFn := fun es => (mkStateFromImportedEntries SpecState.addEntry {} es).switch
   }

src/Lean/DeclarationRange.lean

@@ -36,7 +36,7 @@ instance : ToExpr DeclarationRanges where
   toTypeExpr := mkConst ``DeclarationRanges
 
 builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
-builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension `declranges
+builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension
 
 def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
   builtinDeclRanges.modify (·.insert declName declRanges)

src/Lean/DocString.lean

@@ -9,7 +9,7 @@ import Lean.MonadEnv
 namespace Lean
 
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension `docstring
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
 private def findLeadingSpacesSize (s : String) : Nat :=
   let it := s.iter
@@ -72,7 +72,6 @@ structure ModuleDoc where
   declarationRange : DeclarationRange
 
 private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  name          := `moduleDocExt
   addImportedFn := fun _ => {}
   addEntryFn    := fun s e => s.push e
   toArrayFn     := fun es => es.toArray

src/Lean/Elab/Command.lean

@@ -213,13 +213,13 @@ instance : MonadQuotation CommandElabM where
   getMainModule       := Command.getMainModule
   withFreshMacroScope := Command.withFreshMacroScope
 
-unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) :=
-  mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
+unsafe def mkCommandElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute CommandElab) :=
+  mkElabAttribute CommandElab `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" ref
 
 @[implementedBy mkCommandElabAttributeUnsafe]
-opaque mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab)
+opaque mkCommandElabAttribute (ref : Name) : IO (KeyedDeclsAttribute CommandElab)
 
-builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute
+builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute decl_name%
 
 private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do
   let ctx ← read

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -77,7 +77,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     }
   return thmNames
 
-builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension `structEqInfo
+builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -206,7 +206,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     }
   return thmNames
 
-builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension `wfEqInfo
+builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : CoreM Unit := do
   let declNames := preDefs.map (·.declName)

src/Lean/Elab/Tactic/Basic.lean

@@ -97,7 +97,7 @@ protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Cor
 protected def getMainModule     : TacticM Name       := do pure (← getEnv).mainModule
 
 unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
-  mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
+  mkElabAttribute Tactic `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" `Lean.Elab.Tactic.tacticElabAttribute
 
 @[builtinInit mkTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute Tactic
 

src/Lean/Elab/Term.lean

@@ -350,13 +350,13 @@ private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : Te
 def withoutSavingRecAppSyntax (x : TermElabM α) : TermElabM α :=
   withReader (fun ctx => { ctx with saveRecAppSyntax := false }) x
 
-unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) :=
-  mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term"
+unsafe def mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute TermElab) :=
+  mkElabAttribute TermElab `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref
 
 @[implementedBy mkTermElabAttributeUnsafe]
-opaque mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab)
+opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab)
 
-builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute
+builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute decl_name%
 
 /--
   Auxiliary datatatype for presenting a Lean lvalue modifier.

src/Lean/Elab/Util.lean

@@ -91,8 +91,8 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options)
 @[implementedBy evalSyntaxConstantUnsafe]
 opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
 
-unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String)
-    : IO (KeyedDeclsAttribute γ) :=
+unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String)
+    (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) :=
   KeyedDeclsAttribute.init {
     builtinName   := attrBuiltinName
     name          := attrName
@@ -118,13 +118,13 @@ unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (
           declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
   } attrDeclName
 
-unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
-  mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro"
+unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) :=
+  mkElabAttribute Macro `builtinMacro `macro Name.anonymous `Lean.Macro "macro" ref
 
 @[implementedBy mkMacroAttributeUnsafe]
-opaque mkMacroAttribute : IO (KeyedDeclsAttribute Macro)
+opaque mkMacroAttribute (ref : Name) : IO (KeyedDeclsAttribute Macro)
 
-builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
+builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute decl_name%
 
 /--
 Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful.

src/Lean/Environment.lean

@@ -440,7 +440,7 @@ end PersistentEnvExtension
 builtin_initialize persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)) ← IO.mkRef #[]
 
 structure PersistentEnvExtensionDescr (α β σ : Type) where
-  name            : Name
+  name            : Name := by exact decl_name%
   mkInitial       : IO σ
   addImportedFn   : Array (Array α) → ImportM σ
   addEntryFn      : σ → β → σ
@@ -478,7 +478,7 @@ def SimplePersistentEnvExtension (α σ : Type) := PersistentEnvExtension α α
   as.foldl (fun r es => es.foldl (fun r e => addEntryFn r e) r) initState
 
 structure SimplePersistentEnvExtensionDescr (α σ : Type) where
-  name          : Name
+  name          : Name := by exact decl_name%
   addEntryFn    : σ → α → σ
   addImportedFn : Array (Array α) → σ
   toArrayFn     : List α → Array α := fun es => es.toArray
@@ -522,7 +522,7 @@ end SimplePersistentEnvExtension
     Declarations must only be tagged in the module where they were declared. -/
 def TagDeclarationExtension := SimplePersistentEnvExtension Name NameSet
 
-def mkTagDeclarationExtension (name : Name) : IO TagDeclarationExtension :=
+def mkTagDeclarationExtension (name : Name := by exact decl_name%) : IO TagDeclarationExtension :=
   registerSimplePersistentEnvExtension {
     name          := name,
     addImportedFn := fun _ => {},
@@ -551,7 +551,7 @@ end TagDeclarationExtension
 
 def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
 
-def mkMapDeclarationExtension [Inhabited α] (name : Name) : IO (MapDeclarationExtension α) :=
+def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
     name          := name,
     addImportedFn := fun _ => {},
@@ -612,13 +612,9 @@ unsafe def Environment.freeRegions (env : Environment) : IO Unit :=
 
 def mkModuleData (env : Environment) : IO ModuleData := do
   let pExts ← persistentEnvExtensionsRef.get
-  let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
-    (fun i result =>
-      let state  := (pExts.get! i).getState env
-      let exportEntriesFn := (pExts.get! i).exportEntriesFn
-      let extName    := (pExts.get! i).name
-      result.push (extName, exportEntriesFn state))
-    #[]
+  let entries := pExts.map fun pExt =>
+    let state := pExt.getState env
+    (pExt.name, pExt.exportEntriesFn state)
   pure {
     imports         := env.header.imports
     constants       := env.constants.foldStage2 (fun cs _ c => cs.push c) #[]
@@ -764,7 +760,6 @@ Environment extension for tracking all `namespace` declared by users.
 -/
 builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet ←
   registerSimplePersistentEnvExtension {
-    name            := `namespaces
     addImportedFn   := fun as => mkStateFromImportedEntries NameSSet.insert NameSSet.empty as |>.switch
     addEntryFn      := fun s n => s.insert n
   }

src/Lean/KeyedDeclsAttribute.lean

@@ -100,10 +100,10 @@ def ExtensionState.erase (s : ExtensionState γ) (attrName : Name) (declName : N
     throwError "'{declName}' does not have [{attrName}] attribute"
   return { s with erased := s.erased.insert declName, declNames := s.declNames.erase declName }
 
-protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do
+protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) := do
   let tableRef ← IO.mkRef ({} : Table γ)
   let ext : Extension γ ← registerScopedEnvExtension {
-    name         := df.name
+    name         := attrDeclName
     mkInitial    := return mkStateOfTable (← tableRef.get)
     ofOLeanEntry := fun _ entry => do
       let ctx ← read

src/Lean/Linter/MissingDocs.lean

@@ -49,7 +49,6 @@ builtin_initialize builtinHandlersRef : IO.Ref (NameMap Handler) ← IO.mkRef {}
 builtin_initialize missingDocsExt :
   PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler) ←
   registerPersistentEnvExtension {
-    name            := "missing docs extension"
     mkInitial       := return ([], ← builtinHandlersRef.get)
     addImportedFn   := fun as => do
       ([], ·) <$> as.foldlM (init := ← builtinHandlersRef.get) fun s as =>

src/Lean/Linter/UnusedVariables.lean

@@ -104,7 +104,6 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
 
 builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ←
   registerSimplePersistentEnvExtension {
-    name          := `unusedVariablesIgnoreFns
     addEntryFn    := fun _ _ => ()
     addImportedFn := fun _ => ()
   }

src/Lean/Meta/GlobalInstances.lean

@@ -10,7 +10,6 @@ namespace Lean.Meta
 
 builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit)  ←
   registerSimpleScopedEnvExtension {
-    name     := `ginstanceExt
     initial  := {}
     addEntry := fun s n => s.insert n ()
   }

src/Lean/Meta/Instances.lean

@@ -45,7 +45,6 @@ def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) :
 
 builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ←
   registerSimpleScopedEnvExtension {
-    name     := `instanceExt
     initial  := {}
     addEntry := addInstanceEntry
   }
@@ -106,7 +105,6 @@ def addDefaultInstanceEntry (d : DefaultInstances) (e : DefaultInstanceEntry) :
 
 builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances ←
   registerSimplePersistentEnvExtension {
-    name          := `defaultInstanceExt
     addEntryFn    := addDefaultInstanceEntry
     addImportedFn := fun es => (mkStateFromImportedEntries addDefaultInstanceEntry {} es)
   }

src/Lean/Meta/Match/MatcherInfo.lean

@@ -79,7 +79,6 @@ def State.switch (s : State) : State :=  { s with map := s.map.switch }
 
 builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
   registerSimplePersistentEnvExtension {
-    name          := `matcher
     addEntryFn    := State.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch
   }

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -107,7 +107,6 @@ def addCustomEliminatorEntry (es : CustomEliminators) (e : CustomEliminator) : C
 
 builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminator CustomEliminators ←
   registerSimpleScopedEnvExtension {
-    name           := `elimExt
     initial        := {}
     addEntry       := addCustomEliminatorEntry
     finalizeImport := fun { map := map } => { map := map.switch }

src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean

@@ -44,7 +44,6 @@ where
 
 builtin_initialize congrExtension : SimpleScopedEnvExtension SimpCongrTheorem SimpCongrTheorems ←
   registerSimpleScopedEnvExtension {
-    name           := `congrExt
     initial        := {}
     addEntry       := addSimpCongrTheoremEntry
     finalizeImport := fun s => { s with lemmas := s.lemmas.switch }

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -356,9 +356,9 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
       modifyEnv fun env => ext.modifyState env fun _ => s
   }
 
-def mkSimpExt (extName : Name) : IO SimpExtension :=
+def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension :=
   registerSimpleScopedEnvExtension {
-    name     := extName
+    name     := name
     initial  := {}
     addEntry := fun d e =>
       match e with
@@ -372,9 +372,8 @@ abbrev SimpExtensionMap := HashMap Name SimpExtension
 builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {}
 
 def registerSimpAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%)
-    (extName : Name := attrName.appendAfter "Ext") : IO SimpExtension := do
-  let ext ← mkSimpExt extName
+    (ref : Name := by exact decl_name%) : IO SimpExtension := do
+  let ext ← mkSimpExt ref
   mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
   simpExtensionMapRef.modify fun map => map.insert attrName ext
   return ext

src/Lean/Meta/UnificationHint.lean

@@ -27,7 +27,6 @@ def UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) :
 
 builtin_initialize unificationHintExtension : SimpleScopedEnvExtension UnificationHintEntry UnificationHints ←
   registerSimpleScopedEnvExtension {
-    name     := `unifHints
     addEntry := UnificationHints.add
     initial  := {}
   }

src/Lean/Modifiers.lean

@@ -7,7 +7,7 @@ import Lean.Environment
 
 namespace Lean
 
-builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension `protected
+builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
 @[export lean_add_protected]
 def addProtected (env : Environment) (n : Name) : Environment :=

src/Lean/Parser/Extension.lean

@@ -339,7 +339,6 @@ private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → Impo
 
 builtin_initialize parserExtension : ParserExtension ←
   registerScopedEnvExtension {
-    name            := `parserExt
     mkInitial       := ParserExtension.mkInitial
     addEntry        := ParserExtension.addEntryImpl
     toOLeanEntry    := ParserExtension.Entry.toOLeanEntry

src/Lean/ParserCompiler/Attribute.lean

@@ -17,14 +17,15 @@ structure CombinatorAttribute where
   deriving Inhabited
 -- TODO(Sebastian): We'll probably want priority support here at some point
 
-def registerCombinatorAttribute (name : Name) (descr : String)
+def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by exact decl_name%)
     : IO CombinatorAttribute := do
   let ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) ← registerSimplePersistentEnvExtension {
-    name            := name,
+    name            := ref,
     addImportedFn   := mkStateFromImportedEntries (fun s p => s.insert p.1 p.2) {},
     addEntryFn      := fun (s : NameMap Name) (p : Name × Name) => s.insert p.1 p.2,
   }
   let attrImpl : AttributeImpl := {
+    ref   := ref,
     name  := name,
     descr := descr,
     add   := fun decl stx _ => do

src/Lean/ProjFns.lean

@@ -29,7 +29,7 @@ def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass
 def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
   info.fromClass
 
-builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension `projinfo
+builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
 
 @[export lean_add_projection_info]
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=

src/Lean/ReducibilityAttrs.lean

@@ -18,7 +18,7 @@ inductive ReducibilityStatus where
 Environment extension for storing the reducibility attribute for definitions.
 -/
 builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
-  registerEnumAttributes `reducibility
+  registerEnumAttributes
     [(`reducible, "reducible", ReducibilityStatus.reducible),
      (`semireducible, "semireducible", ReducibilityStatus.semireducible),
      (`irreducible, "irreducible", ReducibilityStatus.irreducible)]

src/Lean/ResolveName.lean

@@ -24,7 +24,6 @@ def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
 
 builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ←
   registerSimplePersistentEnvExtension {
-    name          := `aliasesExt,
     addEntryFn    := addAliasEntry,
     addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es |>.switch
   }

src/Lean/ScopedEnvExtension.lean

@@ -30,7 +30,7 @@ structure StateStack (α : Type) (β : Type) (σ : Type) where
   deriving Inhabited
 
 structure Descr (α : Type) (β : Type) (σ : Type) where
-  name           : Name
+  name           : Name := by exact decl_name%
   mkInitial      : IO σ
   ofOLeanEntry   : σ → α → ImportM β
   toOLeanEntry   : β → α
@@ -197,7 +197,7 @@ def activateScoped [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (name
 abbrev SimpleScopedEnvExtension (α : Type) (σ : Type) := ScopedEnvExtension α α σ
 
 structure SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) where
-  name           : Name
+  name           : Name := by exact decl_name%
   addEntry       : σ → α → σ
   initial        : σ
   finalizeImport : σ → σ := id

src/Lean/Server/Completion.lean

@@ -20,7 +20,7 @@ open Elab
 open Meta
 open FuzzyMatching
 
-builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension `blackListCompletion
+builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
 @[export lean_completion_add_to_black_list]
 def addToBlackList (env : Environment) (declName : Name) : Environment :=

src/Lean/Server/Rpc/RequestHandling.lean

@@ -21,7 +21,7 @@ they *can* easily create custom handlers and use them in the same file. -/
 builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ←
   IO.mkRef {}
 builtin_initialize userRpcProcedures : MapDeclarationExtension Name ←
-  mkMapDeclarationExtension `userRpcProcedures
+  mkMapDeclarationExtension
 
 private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (procName : Name) :
     Except String RpcProcedure :=

src/Lean/Structure.lean

@@ -44,7 +44,6 @@ private structure StructureState where
   deriving Inhabited
 
 builtin_initialize structureExt : SimplePersistentEnvExtension StructureInfo StructureState ← registerSimplePersistentEnvExtension {
-  name          := `structExt
   addImportedFn := fun _ => {}
   addEntryFn    := fun s e => { s with map := s.map.insert e.structName e }
   toArrayFn     := fun es => es.toArray.qsort StructureInfo.lt

src/Lean/Widget/UserWidget.lean

@@ -54,10 +54,9 @@ private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension
     (RBMap UInt64 Name compare)
 
 -- Mapping widgetSourceId to hash of sourcetext
-builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry
+builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension
 builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ←
   registerSimplePersistentEnvExtension {
-    name          := `widgetSourceRegistry
     addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
     addEntryFn    := fun s n => s.insert n.1 n.2
     toArrayFn     := fun es => es.toArray

stage0/src/stdlib_flags.h

@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     opts = opts.update({"pp", "rawOnError"}, true);

tests/pkg/user_ext/UserExt/BlaExt.lean

@@ -4,7 +4,6 @@ open Lean
 
 initialize blaExtension : SimplePersistentEnvExtension Name NameSet ←
   registerSimplePersistentEnvExtension {
-    name          := `blaExt
     addEntryFn    := NameSet.insert
     addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
   }

tests/pkg/user_ext/UserExt/FooExt.lean

@@ -4,7 +4,6 @@ open Lean
 
 initialize fooExtension : SimplePersistentEnvExtension Name NameSet ←
   registerSimplePersistentEnvExtension {
-    name          := `fooExt
     addEntryFn    := NameSet.insert
     addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
   }