diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean
index 663270340b..e5b38aa33b 100644
--- a/library/init/lean/attributes.lean
+++ b/library/init/lean/attributes.lean
@@ -124,6 +124,9 @@ structure AttributeImpl :=
 (pushScope (env : Environment) : IO Environment := pure env)
 (popScope (env : Environment) : IO Environment := pure env)
 
+instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
+⟨{ name := default _, descr := default _, add := λ env _ _ _, pure env }⟩
+
 def mkAttributeMapRef : IO (IO.Ref (HashMap Name AttributeImpl)) :=
 IO.mkRef {}
 
@@ -246,7 +249,8 @@ ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension {
   addEntryFn      := λ (s : NameSet) n, s.insert n,
   exportEntriesFn := λ es,
     let r : Array Name := es.fold (λ a e, a.push e) Array.empty in
-    r.qsort Name.quickLt
+    r.qsort Name.quickLt,
+  statsFn         := λ s, "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
 },
 let attrImpl : AttributeImpl := {
   name  := name,
@@ -261,9 +265,15 @@ let attrImpl : AttributeImpl := {
 registerAttribute attrImpl,
 pure { attr := attrImpl, ext := ext }
 
-def TagAttribute.hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
+namespace TagAttribute
+
+instance : Inhabited TagAttribute := ⟨{attr := default _, ext := default _}⟩
+
+def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
 match env.getModuleIdxFor decl with
 | some modIdx := (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
 | none        := (attr.ext.getState env).contains decl
 
+end TagAttribute
+
 end Lean
diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean
index 9ed05d1cb1..5190d9a2c9 100644
--- a/library/init/lean/environment.lean
+++ b/library/init/lean/environment.lean
@@ -463,8 +463,9 @@ IO.println ("number of extensions:                  " ++ toString env.extensions
 pExtDescrs.mfor $ λ 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 (λ sum es, sum + es.size) 0)),
-  IO.println ("  " ++ toString (Format.nest 2 (extDescr.statsFn s.state))),
   pure ()
 },
 pure ()
diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean
index 44fe9a8749..2deaf67034 100644
--- a/library/init/lean/format.lean
+++ b/library/init/lean/format.lean
@@ -25,6 +25,10 @@ instance : Inhabited Format     := ⟨nil⟩
 def join (xs : List Format) : Format :=
 xs.foldl (++) ""
 
+def isNil : Format → Bool
+| nil := true
+| _   := false
+
 def flatten : Format → Format
 | nil                     := nil
 | line                    := text " "