diff --git a/library/Init/Lean/Attributes.lean b/library/Init/Lean/Attributes.lean
index cad6b9dbae..4ab40fa898 100644
--- a/library/Init/Lean/Attributes.lean
+++ b/library/Init/Lean/Attributes.lean
@@ -148,30 +148,29 @@ structure TagAttribute :=
 (ext  : PersistentEnvExtension Name NameSet)
 
 def registerTagAttribute (name : Name) (descr : String) (validate : Environment → Name → Except String Unit := fun _ _ => Except.ok ()) : IO TagAttribute :=
-do
-ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension {
-  name            := name,
-  addImportedFn   := fun _ => pure {},
-  addEntryFn      := fun (s : NameSet) n => s.insert n,
-  exportEntriesFn := fun es =>
-    let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
-    r.qsort Name.quickLt,
-  statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
-};
-let attrImpl : AttributeImpl := {
-  name  := name,
-  descr := descr,
-  add   := fun env decl args persistent => do
-    unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
-    unless (env.getModuleIdxFor decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match validate env decl with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | _                => pure $ ext.addEntry env decl
-};
-registerAttribute attrImpl;
-pure { attr := attrImpl, ext := ext }
+do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension {
+     name            := name,
+     addImportedFn   := fun _ => pure {},
+     addEntryFn      := fun (s : NameSet) n => s.insert n,
+     exportEntriesFn := fun es =>
+       let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
+       r.qsort Name.quickLt,
+     statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
+   };
+   let attrImpl : AttributeImpl := {
+     name  := name,
+     descr := descr,
+     add   := fun env decl args persistent => do
+       unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
+       unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+       unless (env.getModuleIdxFor decl).isNone $
+         throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
+       match validate env decl with
+       | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
+       | _                => pure $ ext.addEntry env decl
+   };
+   registerAttribute attrImpl;
+   pure { attr := attrImpl, ext := ext }
 
 namespace TagAttribute
 
@@ -197,33 +196,32 @@ structure ParametricAttribute (α : Type) :=
 def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
        (getParam : Environment → Name → Syntax → Except String α)
        (afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env) : IO (ParametricAttribute α) :=
-do
-ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
-  name            := name,
-  addImportedFn   := fun _ => pure {},
-  addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
-  exportEntriesFn := fun m =>
-    let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
-    r.qsort (fun a b => Name.quickLt a.1 b.1),
-  statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
-};
-let attrImpl : AttributeImpl := {
-  name  := name,
-  descr := descr,
-  add   := fun env decl args persistent => do
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
-    unless (env.getModuleIdxFor decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match getParam env decl args with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | Except.ok val    => do
-      let env := ext.addEntry env (decl, val);
-      match afterSet env decl val with
-      | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-      | Except.ok env    => pure env
-};
-registerAttribute attrImpl;
-pure { attr := attrImpl, ext := ext }
+do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
+     name            := name,
+     addImportedFn   := fun _ => pure {},
+     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
+     exportEntriesFn := fun m =>
+       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
+       r.qsort (fun a b => Name.quickLt a.1 b.1),
+     statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
+   };
+   let attrImpl : AttributeImpl := {
+     name  := name,
+     descr := descr,
+     add   := fun env decl args persistent => do
+       unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+       unless (env.getModuleIdxFor decl).isNone $
+         throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
+       match getParam env decl args with
+       | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
+       | Except.ok val    => do
+         let env := ext.addEntry env (decl, val);
+         match afterSet env decl val with
+         | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
+         | Except.ok env    => pure env
+   };
+   registerAttribute attrImpl;
+   pure { attr := attrImpl, ext := ext }
 
 namespace ParametricAttribute
 
@@ -256,29 +254,28 @@ structure EnumAttributes (α : Type) :=
 (ext   : PersistentEnvExtension (Name × α) (NameMap α))
 
 def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) : IO (EnumAttributes α) :=
-do
-ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
-  name            := extName,
-  addImportedFn   := fun _ => pure {},
-  addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
-  exportEntriesFn := fun m =>
-    let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
-    r.qsort (fun a b => Name.quickLt a.1 b.1),
-  statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
-};
-let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
-  name  := name,
-  descr := descr,
-  add   := fun env decl args persistent => do
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
-    unless (env.getModuleIdxFor decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match validate env decl val with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | _                => pure $ ext.addEntry env (decl, val)
-};
-attrs.mfor registerAttribute;
-pure { ext := ext, attrs := attrs }
+do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
+     name            := extName,
+     addImportedFn   := fun _ => pure {},
+     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
+     exportEntriesFn := fun m =>
+       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
+       r.qsort (fun a b => Name.quickLt a.1 b.1),
+     statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
+   };
+   let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
+     name  := name,
+     descr := descr,
+     add   := fun env decl args persistent => do
+       unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+       unless (env.getModuleIdxFor decl).isNone $
+         throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
+       match validate env decl val with
+       | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
+       | _                => pure $ ext.addEntry env (decl, val)
+   };
+   attrs.mfor registerAttribute;
+   pure { ext := ext, attrs := attrs }
 
 namespace EnumAttributes
 
diff --git a/library/Init/Lean/Environment.lean b/library/Init/Lean/Environment.lean
index fd397226c8..c61d3cc4a2 100644
--- a/library/Init/Lean/Environment.lean
+++ b/library/Init/Lean/Environment.lean
@@ -31,7 +31,7 @@ structure EnvironmentHeader :=
 (trustLevel   : UInt32     := 0)
 (quotInit     : Bool       := false)
 (mainModule   : Name       := default _)
-(imports      : Array Name := Array.empty)
+(imports      : Array Name := #[])
 
 /- TODO: mark opaque. -/
 structure Environment :=
@@ -43,7 +43,7 @@ structure Environment :=
 namespace Environment
 
 instance : Inhabited Environment :=
-⟨{ const2ModIdx := {}, constants := {}, extensions := Array.empty }⟩
+⟨{ const2ModIdx := {}, constants := {}, extensions := #[] }⟩
 
 def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
 { constants := env.constants.insert cinfo.name cinfo, .. env }
@@ -153,7 +153,7 @@ constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f
 end EnvExtension
 
 private def mkEnvExtensionsRef : IO (IO.Ref (Array (EnvExtension EnvExtensionState))) :=
-IO.mkRef Array.empty
+IO.mkRef #[]
 
 @[init mkEnvExtensionsRef]
 private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := default _
@@ -162,18 +162,17 @@ instance EnvExtension.Inhabited (σ : Type) [Inhabited σ] : Inhabited (EnvExten
 ⟨{ idx := 0, stateInh := default _, mkInitial := default _ }⟩
 
 unsafe def registerEnvExtensionUnsafe {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) :=
-do
-initializing ← IO.initializing;
-unless initializing $ throw (IO.userError ("failed to register environment, extensions can only be registered during initialization"));
-exts ← envExtensionsRef.get;
-let idx := exts.size;
-let ext : EnvExtension σ := {
-   idx        := idx,
-   mkInitial  := mkInitial,
-   stateInh   := default _
-};
-envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
-pure ext
+do initializing ← IO.initializing;
+   unless initializing $ throw (IO.userError ("failed to register environment, extensions can only be registered during initialization"));
+   exts ← envExtensionsRef.get;
+   let idx := exts.size;
+   let ext : EnvExtension σ := {
+      idx        := idx,
+      mkInitial  := mkInitial,
+      stateInh   := default _
+   };
+   envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
+   pure ext
 
 /- Environment extensions can only be registered during initialization.
    Reasons:
@@ -187,14 +186,13 @@ do exts ← envExtensionsRef.get; exts.mmap $ fun ext => ext.mkInitial
 
 @[export lean_mk_empty_environment]
 def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment :=
-do
-initializing ← IO.initializing;
-when initializing $ throw (IO.userError "environment objects cannot be created during initialization");
-exts ← mkInitialExtensionStates;
-pure { const2ModIdx := {},
-       constants    := {},
-       header       := { trustLevel := trustLevel },
-       extensions   := exts }
+do initializing ← IO.initializing;
+   when initializing $ throw (IO.userError "environment objects cannot be created during initialization");
+   exts ← mkInitialExtensionStates;
+   pure { const2ModIdx := {},
+          constants    := {},
+          header       := { trustLevel := trustLevel },
+          extensions   := exts }
 
 structure PersistentEnvExtensionState (α : Type) (σ : Type) :=
 (importedEntries : Array (Array α))  -- entries per imported module
@@ -219,14 +217,14 @@ def EnvExtensionEntry := NonScalar
 instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := inferInstanceAs (Inhabited NonScalar)
 
 instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
-⟨{importedEntries := Array.empty, state := default _ }⟩
+⟨{importedEntries := #[], state := default _ }⟩
 
 instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α σ) :=
 ⟨{ toEnvExtension := { idx := 0, stateInh := default _, mkInitial := default _ },
    name := default _,
    addImportedFn := fun _ => default _,
    addEntryFn := fun s _ => s,
-   exportEntriesFn := fun _ => Array.empty,
+   exportEntriesFn := fun _ => #[],
    statsFn := fun _ => Format.nil }⟩
 
 namespace PersistentEnvExtension
@@ -251,7 +249,7 @@ ext.toEnvExtension.modifyState env $ fun ps => { state := f (ps.state), .. ps }
 end PersistentEnvExtension
 
 private def mkPersistentEnvExtensionsRef : IO (IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState))) :=
-IO.mkRef Array.empty
+IO.mkRef #[]
 
 @[init mkPersistentEnvExtensionsRef]
 private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
@@ -264,26 +262,25 @@ structure PersistentEnvExtensionDescr (α σ : Type) :=
 (statsFn         : σ → Format := fun _ => Format.nil)
 
 unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) :=
-do
-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
-  state ← descr.addImportedFn Array.empty;
-  let s : PersistentEnvExtensionState α σ := {
-    importedEntries := Array.empty,
-    state           := state
-  };
-  pure s);
-let pExt : PersistentEnvExtension α σ := {
-  toEnvExtension  := ext,
-  name            := descr.name,
-  addImportedFn   := descr.addImportedFn,
-  addEntryFn      := descr.addEntryFn,
-  exportEntriesFn := descr.exportEntriesFn,
-  statsFn         := descr.statsFn
-};
-persistentEnvExtensionsRef.modify (fun pExts => pExts.push (unsafeCast pExt));
-pure pExt
+do 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
+     state ← descr.addImportedFn #[];
+     let s : PersistentEnvExtensionState α σ := {
+       importedEntries := #[],
+       state           := state
+     };
+     pure s);
+   let pExt : PersistentEnvExtension α σ := {
+     toEnvExtension  := ext,
+     name            := descr.name,
+     addImportedFn   := descr.addImportedFn,
+     addEntryFn      := descr.addEntryFn,
+     exportEntriesFn := descr.exportEntriesFn,
+     statsFn         := descr.statsFn
+   };
+   persistentEnvExtensionsRef.modify (fun pExts => pExts.push (unsafeCast pExt));
+   pure pExt
 
 @[implementedBy registerPersistentEnvExtensionUnsafe]
 constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
@@ -403,22 +400,21 @@ constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := defaul
 constant readModuleData (fname : @& String) : IO ModuleData := default _
 
 def mkModuleData (env : Environment) : IO ModuleData :=
-do
-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))
-  Array.empty;
-bytes ← serializeModifications (modListExtension.getState env);
-pure {
-imports    := env.header.imports,
-constants  := env.constants.foldStage2 (fun cs _ c => cs.push c) Array.empty,
-entries    := entries,
-serialized := bytes
-}
+do 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))
+     #[];
+   bytes ← serializeModifications (modListExtension.getState env);
+   pure {
+     imports    := env.header.imports,
+     constants  := env.constants.foldStage2 (fun cs _ c => cs.push c) #[],
+     entries    := entries,
+     serialized := bytes
+   }
 
 @[export lean_write_module]
 def writeModule (env : Environment) (fname : String) : IO Unit :=
@@ -443,54 +439,51 @@ private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Ar
     let curr := mod.entries.get! i;
     if curr.1 == extId then curr.2 else getEntriesFor (i+1)
   else
-    Array.empty
+    #[]
 
 private def setImportedEntries (env : Environment) (mods : Array ModuleData) : IO Environment :=
-do
-pExtDescrs ← persistentEnvExtensionsRef.get;
-pure $ mods.iterate env $ fun _ mod env =>
-  pExtDescrs.iterate env $ fun _ extDescr env =>
-    let entries := getEntriesFor mod extDescr.name 0;
-    extDescr.toEnvExtension.modifyState env $ fun s =>
-      { importedEntries := s.importedEntries.push entries,
-        .. s }
+do pExtDescrs ← persistentEnvExtensionsRef.get;
+   pure $ mods.iterate env $ fun _ mod env =>
+     pExtDescrs.iterate env $ fun _ extDescr env =>
+       let entries := getEntriesFor mod extDescr.name 0;
+       extDescr.toEnvExtension.modifyState env $ fun s =>
+         { importedEntries := s.importedEntries.push entries,
+           .. s }
 
 private def finalizePersistentExtensions (env : Environment) : IO Environment :=
-do
-pExtDescrs ← persistentEnvExtensionsRef.get;
-pExtDescrs.miterate env $ fun _ extDescr env => do
-  let s := extDescr.toEnvExtension.getState env;
-  newState ← extDescr.addImportedFn s.importedEntries;
-  pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
+do pExtDescrs ← persistentEnvExtensionsRef.get;
+   pExtDescrs.miterate env $ fun _ extDescr env => do
+     let s := extDescr.toEnvExtension.getState env;
+     newState ← extDescr.addImportedFn s.importedEntries;
+     pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
 
 @[export lean_import_modules]
 def importModules (modNames : List Name) (trustLevel : UInt32 := 0) : IO Environment :=
-do
-(_, mods) ← importModulesAux modNames ({}, Array.empty);
-let const2ModIdx := mods.iterate {} $ fun (modIdx) (mod : ModuleData) (m : HashMap Name ModuleIdx) =>
-  mod.constants.iterate m $ fun _ cinfo m =>
-    m.insert cinfo.name modIdx.val;
-constants ← mods.miterate SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
-  mod.constants.miterate cs $ fun _ cinfo cs => do {
-    when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'"));
-    pure $ cs.insert cinfo.name cinfo
-  };
-let constants   := constants.switch;
-exts ← mkInitialExtensionStates;
-let env : Environment := {
-  const2ModIdx := const2ModIdx,
-  constants    := constants,
-  extensions   := exts,
-  header       := {
-    quotInit     := !modNames.isEmpty, -- We assume `core.lean` initializes quotient module
-    trustLevel   := trustLevel,
-    imports      := modNames.toArray
-  }
-};
-env ← setImportedEntries env mods;
-env ← finalizePersistentExtensions env;
-env ← mods.miterate env $ fun _ mod env => performModifications env mod.serialized;
-pure env
+do (_, mods) ← importModulesAux modNames ({}, #[]);
+   let const2ModIdx := mods.iterate {} $ fun (modIdx) (mod : ModuleData) (m : HashMap Name ModuleIdx) =>
+     mod.constants.iterate m $ fun _ cinfo m =>
+       m.insert cinfo.name modIdx.val;
+   constants ← mods.miterate SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
+     mod.constants.miterate cs $ fun _ cinfo cs => do {
+       when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'"));
+       pure $ cs.insert cinfo.name cinfo
+     };
+   let constants   := constants.switch;
+   exts ← mkInitialExtensionStates;
+   let env : Environment := {
+     const2ModIdx := const2ModIdx,
+     constants    := constants,
+     extensions   := exts,
+     header       := {
+       quotInit     := !modNames.isEmpty, -- We assume `core.lean` initializes quotient module
+       trustLevel   := trustLevel,
+       imports      := modNames.toArray
+     }
+   };
+   env ← setImportedEntries env mods;
+   env ← finalizePersistentExtensions env;
+   env ← mods.miterate env $ fun _ mod env => performModifications env mod.serialized;
+   pure env
 
 def regNamespacesExtension : IO (SimplePersistentEnvExtension Name NameSet) :=
 registerSimplePersistentEnvExtension {
@@ -529,26 +522,25 @@ env.addAux cinfo
 
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit :=
-do
-pExtDescrs ← persistentEnvExtensionsRef.get;
-let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
-IO.println ("direct imports:                        " ++ toString env.header.imports);
-IO.println ("number of imported modules:            " ++ toString numModules);
-IO.println ("number of consts:                      " ++ toString env.constants.size);
-IO.println ("number of imported consts:             " ++ toString env.constants.stageSizes.1);
-IO.println ("number of local consts:                " ++ toString env.constants.stageSizes.2);
-IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
-IO.println ("trust level:                           " ++ toString env.header.trustLevel);
-IO.println ("number of extensions:                  " ++ toString env.extensions.size);
-pExtDescrs.mfor $ fun extDescr => do {
-  IO.println ("extension '" ++ toString extDescr.name ++ "'");
-  let s := extDescr.toEnvExtension.getState env;
-  let fmt := extDescr.statsFn s.state;
-  unless fmt.isNil (IO.println ("  " ++ toString (Format.nest 2 (extDescr.statsFn s.state))));
-  IO.println ("  number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0));
-  pure ()
-};
-pure ()
+do pExtDescrs ← persistentEnvExtensionsRef.get;
+   let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
+   IO.println ("direct imports:                        " ++ toString env.header.imports);
+   IO.println ("number of imported modules:            " ++ toString numModules);
+   IO.println ("number of consts:                      " ++ toString env.constants.size);
+   IO.println ("number of imported consts:             " ++ toString env.constants.stageSizes.1);
+   IO.println ("number of local consts:                " ++ toString env.constants.stageSizes.2);
+   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
+   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
+   IO.println ("number of extensions:                  " ++ toString env.extensions.size);
+   pExtDescrs.mfor $ fun extDescr => do {
+     IO.println ("extension '" ++ toString extDescr.name ++ "'");
+     let s := extDescr.toEnvExtension.getState env;
+     let fmt := extDescr.statsFn s.state;
+     unless fmt.isNil (IO.println ("  " ++ toString (Format.nest 2 (extDescr.statsFn s.state))));
+     IO.println ("  number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0));
+     pure ()
+   };
+   pure ()
 
 end Environment
 end Lean
diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean
index f20aca7acc..56a5bc222b 100644
--- a/library/Init/Lean/Path.lean
+++ b/library/Init/Lean/Path.lean
@@ -89,10 +89,9 @@ def addRel (baseDir : String) : Nat → String
 | n+1 => addRel n ++ pathSep ++ ".."
 
 def findLeanFile (modName : Name) (ext : String) : IO String :=
-do
-let fname := modNameToFileName modName;
-some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
-realPathNormalized fname
+do let fname := modNameToFileName modName;
+   some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
+   realPathNormalized fname
 
 def findOLean (modName : Name) : IO String :=
 findLeanFile modName "olean"
@@ -110,22 +109,21 @@ do fname ← realPathNormalized fname;
 
 @[export lean_module_name_of_file]
 def moduleNameOfFileName (fname : String) : IO Name :=
-do
-path  ← findAtSearchPath fname;
-fname ← realPathNormalized fname;
-let fnameSuffix := fname.drop path.length;
-let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
-if path ++ pathSep ++ fnameSuffix != fname then
-  throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, path is not a prefix of the given file"))
-else do
-  some extPos ← pure (fnameSuffix.revPosOf '.')
-    | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing"));
-  let modNameStr := fnameSuffix.extract 0 extPos;
-  let extStr     := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize;
-  let parts      := modNameStr.split pathSep;
-  let modName    := parts.foldl Name.mkString Name.anonymous;
-  fname' ← findLeanFile modName extStr;
-  unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'"));
-  pure modName
+do path  ← findAtSearchPath fname;
+   fname ← realPathNormalized fname;
+   let fnameSuffix := fname.drop path.length;
+   let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
+   if path ++ pathSep ++ fnameSuffix != fname then
+     throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, path is not a prefix of the given file"))
+   else do
+     some extPos ← pure (fnameSuffix.revPosOf '.')
+       | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing"));
+     let modNameStr := fnameSuffix.extract 0 extPos;
+     let extStr     := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize;
+     let parts      := modNameStr.split pathSep;
+     let modName    := parts.foldl Name.mkString Name.anonymous;
+     fname' ← findLeanFile modName extStr;
+     unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'"));
+     pure modName
 
 end Lean
diff --git a/library/Init/Lean/Syntax.lean b/library/Init/Lean/Syntax.lean
index b12c1b389b..79223d4002 100644
--- a/library/Init/Lean/Syntax.lean
+++ b/library/Init/Lean/Syntax.lean
@@ -146,7 +146,7 @@ def isOfKind {α} : Syntax α → SyntaxNodeKind → Bool
 
 def asNode {α} : Syntax α → SyntaxNode α
 | Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩
-| _                     => ⟨Syntax.node nullKind Array.empty, IsNode.mk nullKind Array.empty⟩
+| _                     => ⟨Syntax.node nullKind #[], IsNode.mk nullKind #[]⟩
 
 def getNumArgs {α} (stx : Syntax α) : Nat :=
 stx.asNode.getNumArgs
@@ -354,7 +354,7 @@ Syntax.node nullKind args.toArray
 def mkOptionalNode {α} (arg : Option (Syntax α)) : Syntax α :=
 match arg with
 | some arg => Syntax.node nullKind #[arg]
-| none     => Syntax.node nullKind Array.empty
+| none     => Syntax.node nullKind #[]
 
 /- Helper functions for creating string and numeric literals -/