fix: builtin attribute initialization

The failure was triggered if a module declared (only) builtin
attributes that do not have any persistent extension associated with
them.

Fixes #726

src/Lean/Attributes.lean

@@ -414,16 +414,20 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
   let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName
   attr.erase declName
 
-builtin_initialize
-  -- See comment at `updateEnvAttributesRef`
-  updateEnvAttributesRef.set fun env => do
-    let map ← attributeMapRef.get
-    let s ← attributeExtension.getState env
-    let s := map.foldl (init := s) fun s attrName attrImpl =>
-      if s.map.contains attrName then
-        s
-      else
-        { s with map := s.map.insert attrName attrImpl }
-    return attributeExtension.setState env s
+/-- `updateEnvAttributes` implementation -/
+@[export lean_update_env_attributes]
+def updateEnvAttributesImpl (env : Environment) : IO Environment := do
+  let map ← attributeMapRef.get
+  let s ← attributeExtension.getState env
+  let s := map.foldl (init := s) fun s attrName attrImpl =>
+    if s.map.contains attrName then
+      s
+    else
+      { s with map := s.map.insert attrName attrImpl }
+  return attributeExtension.setState env s
+
+/-- `getNumBuiltinAttributes` implementation -/
+@[export lean_get_num_attributes] def getNumBuiltiAttributesImpl : IO Nat :=
+  return (← attributeMapRef.get).size
 
 end Lean

src/Lean/Environment.lean

@@ -569,7 +569,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
       env ← extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.push entries }
   return env
 
-/-
+/--
   "Forward declaration" needed for updating the attribute table with user-defined attributes.
   User-defined attributes are declared using the `initialize` command. The `initialize` command is just syntax sugar for the `init` attribute.
   The `init` attribute is initialized after the `attributeExtension` is initialized. We cannot change the order since the `init` attribute is an attribute,
@@ -578,7 +578,9 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   When we a new user-defined attribute declaration is imported, `attributeMapRef` is updated.
   Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
-builtin_initialize updateEnvAttributesRef : IO.Ref (Environment → IO Environment) ← IO.mkRef (fun env => pure env)
+@[extern 2 "lean_update_env_attributes"] constant updateEnvAttributes : Environment → IO Environment
+/-- "Forward declaration" for retrieving the number of builtin attributes. -/
+@[extern 1 "lean_get_num_attributes"] constant getNumBuiltiAttributes : IO Nat
 
 private partial def finalizePersistentExtensions (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do
   loop 0 env
@@ -590,16 +592,17 @@ where
       let extDescr := pExtDescrs[i]
       let s := extDescr.toEnvExtension.getState env
       let prevSize := (← persistentEnvExtensionsRef.get).size
+      let prevAttrSize ← getNumBuiltiAttributes
       let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts }
       let mut env ← extDescr.toEnvExtension.setState env { s with state := newState }
       env ← ensureExtensionsArraySize env
-      if (← persistentEnvExtensionsRef.get).size > prevSize then
+      if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltiAttributes) > prevAttrSize then
         -- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and
         -- a user-defined persistent extension is imported.
         -- Thus, we invoke `setImportedEntries` to update the array `importedEntries` with the entries for the new extensions.
         env ← setImportedEntries env mods prevSize
         -- See comment at `updateEnvAttributesRef`
-        env ← (← updateEnvAttributesRef.get) env
+        env ← updateEnvAttributes env
       loop (i + 1) env
     else
       return env

src/shell/CMakeLists.txt

@@ -203,6 +203,14 @@ add_test(NAME leanpkgtest_user_attr_app
            find . -name '*.olean' -delete
            leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr")
 
+add_test(NAME leanpkgtest_builtin_attr
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/builtin_attr"
+         COMMAND bash -c "
+           set -eu
+           export PATH=${LEAN_BIN}:$PATH
+           find . -name '*.olean' -delete
+           leanmake")
+
 add_test(NAME laketest
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/lake/examples"
          COMMAND bash -c "

tests/leanpkg/builtin_attr/.gitignore

@@ -0,0 +1 @@
+/build

tests/leanpkg/builtin_attr/UserAttr.lean

@@ -0,0 +1 @@
+import UserAttr.Tst

tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean

@@ -0,0 +1,11 @@
+import Lean
+
+open Lean
+
+-- initialize discard <| registerTagAttribute `foo ""
+
+initialize registerBuiltinAttribute {
+    name := `bar,
+    descr := "",
+    add := fun _ _ _ => ()
+  }

tests/leanpkg/builtin_attr/UserAttr/Tst.lean

@@ -0,0 +1,4 @@
+import UserAttr.BlaAttr
+
+@[bar] def f (x : Nat) := x + 2
+@[bar] def g (x : Nat) := x + 1

tests/leanpkg/builtin_attr/leanpkg.toml

@@ -0,0 +1,3 @@
+[package]
+name = "UserAttr"
+version = "0.1"