diff --git a/src/Init/Lean/Attributes.lean b/src/Init/Lean/Attributes.lean
index 06d185c688..bcef1adf22 100644
--- a/src/Init/Lean/Attributes.lean
+++ b/src/Init/Lean/Attributes.lean
@@ -153,6 +153,7 @@ structure TagAttribute :=
 def registerTagAttribute (name : Name) (descr : String) (validate : Environment → Name → Except String Unit := fun _ _ => Except.ok ()) : IO TagAttribute := do
 ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
   name            := name,
+  initial         := {},
   addImportedFn   := fun _ _ => pure {},
   addEntryFn      := fun (s : NameSet) n => s.insert n,
   exportEntriesFn := fun es =>
@@ -201,6 +202,7 @@ def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr
        (afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env) : IO (ParametricAttribute α) := do
 ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
   name            := name,
+  initial         := {},
   addImportedFn   := fun _ _ => pure {},
   addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
   exportEntriesFn := fun m =>
@@ -259,6 +261,7 @@ structure EnumAttributes (α : Type) :=
 def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO (EnumAttributes α) := do
 ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
   name            := extName,
+  initial         := {},
   addImportedFn   := fun _ _ => pure {},
   addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
   exportEntriesFn := fun m =>
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index 8a1f601b10..db1fff827b 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -51,6 +51,7 @@ The current implementation just uses the bultin elaborators.
 def mkElabAttribute {σ} [Inhabited σ] (attrName : Name) (kind : String) (builtinTable : IO.Ref σ) : IO (ElabAttribute σ) := do
 ext : PersistentEnvExtension ElabAttributeEntry ElabAttributeEntry σ ← registerPersistentEnvExtension {
   name            := attrName,
+  initial         := arbitrary _,
   addImportedFn   := fun env es => do
     table ← builtinTable.get;
     -- TODO: populate table with `es`
diff --git a/src/Init/Lean/Environment.lean b/src/Init/Lean/Environment.lean
index 33fa1a6ee9..efb3756a19 100644
--- a/src/Init/Lean/Environment.lean
+++ b/src/Init/Lean/Environment.lean
@@ -276,6 +276,7 @@ private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtens
 
 structure PersistentEnvExtensionDescr (α β σ : Type) :=
 (name            : Name)
+(initial         : σ)
 (addImportedFn   : Environment → Array (Array α) → IO σ)
 (addEntryFn      : σ → β → σ)
 (exportEntriesFn : σ → Array α)
@@ -285,11 +286,9 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ]
 pExts ← persistentEnvExtensionsRef.get;
 when (pExts.any (fun ext => ext.name == descr.name)) $ throw (IO.userError ("invalid environment extension, '" ++ toString descr.name ++ "' has already been used"));
 ext ← registerEnvExtension $ do {
-  env ← mkEmptyEnvironment;
-  state ← descr.addImportedFn env #[];
   let s : PersistentEnvExtensionState α σ := {
     importedEntries := #[],
-    state           := state
+    state           := descr.initial
   };
   pure s
 };
@@ -322,9 +321,10 @@ structure SimplePersistentEnvExtensionDescr (α σ : Type) :=
 
 def registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : SimplePersistentEnvExtensionDescr α σ) : IO (SimplePersistentEnvExtension α σ) :=
 registerPersistentEnvExtension {
-  name := descr.name,
-  addImportedFn := fun _ as => pure ([], descr.addImportedFn as),
-  addEntryFn := fun s e => match s with
+  name            := descr.name,
+  initial         := ([], descr.addImportedFn #[]),
+  addImportedFn   := fun _ as => pure ([], descr.addImportedFn as),
+  addEntryFn      := fun s e => match s with
     | (entries, s) => (e::entries, descr.addEntryFn s e),
   exportEntriesFn := fun s => descr.toArrayFn s.1.reverse,
   statsFn := fun s => format "number of local entries: " ++ format s.1.length
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index c20809360f..ca24b084b3 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1334,6 +1334,7 @@ set_option compiler.extract_closed false
 def mkTokenTableAttribute : IO TokenTableAttribute := do
 ext : PersistentEnvExtension TokenConfig TokenConfig TokenTable ← registerPersistentEnvExtension {
   name            := `_tokens_,
+  initial         := {},
   addImportedFn   := fun _ es => mkImportedTokenTable es,
   addEntryFn      := fun (s : TokenTable) _ => s,         -- TODO
   exportEntriesFn := fun _ => #[],                        -- TODO
@@ -1626,6 +1627,7 @@ attrTable ← parserAttributeTableRef.get;
 when (attrTable.contains kindSym) $ throw (IO.userError ("parser attribute '" ++ kind ++ "' has already been defined"));
 ext : PersistentEnvExtension Name ParserAttributeEntry ParserAttributeExtensionState ← registerPersistentEnvExtension {
   name            := attrName,
+  initial         := { ParserAttributeExtensionState . },
   addImportedFn   := addImportedParsers builtinTables,
   addEntryFn      := addParserAttributeEntry,
   exportEntriesFn := fun s => s.newEntries.reverse.toArray,