From f01a124f187793cdf09788b0cc102eba156b1c60 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Oct 2021 13:52:07 -0700 Subject: [PATCH] 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 | 26 +++++++++++-------- src/Lean/Environment.lean | 11 +++++--- src/shell/CMakeLists.txt | 8 ++++++ tests/leanpkg/builtin_attr/.gitignore | 1 + tests/leanpkg/builtin_attr/UserAttr.lean | 1 + .../builtin_attr/UserAttr/BlaAttr.lean | 11 ++++++++ tests/leanpkg/builtin_attr/UserAttr/Tst.lean | 4 +++ tests/leanpkg/builtin_attr/leanpkg.toml | 3 +++ 8 files changed, 50 insertions(+), 15 deletions(-) create mode 100644 tests/leanpkg/builtin_attr/.gitignore create mode 100644 tests/leanpkg/builtin_attr/UserAttr.lean create mode 100644 tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean create mode 100644 tests/leanpkg/builtin_attr/UserAttr/Tst.lean create mode 100644 tests/leanpkg/builtin_attr/leanpkg.toml diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 3cc1405c2a..d0f3cc911b 100644 --- a/src/Lean/Attributes.lean +++ b/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 diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e87f555bbb..e4e4864ffb 100644 --- a/src/Lean/Environment.lean +++ b/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 diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index b6ad916c5c..ff87361740 100644 --- a/src/shell/CMakeLists.txt +++ b/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 " diff --git a/tests/leanpkg/builtin_attr/.gitignore b/tests/leanpkg/builtin_attr/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/tests/leanpkg/builtin_attr/.gitignore @@ -0,0 +1 @@ +/build diff --git a/tests/leanpkg/builtin_attr/UserAttr.lean b/tests/leanpkg/builtin_attr/UserAttr.lean new file mode 100644 index 0000000000..28b59b3472 --- /dev/null +++ b/tests/leanpkg/builtin_attr/UserAttr.lean @@ -0,0 +1 @@ +import UserAttr.Tst diff --git a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean b/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean new file mode 100644 index 0000000000..6fb03c4e86 --- /dev/null +++ b/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 _ _ _ => () + } diff --git a/tests/leanpkg/builtin_attr/UserAttr/Tst.lean b/tests/leanpkg/builtin_attr/UserAttr/Tst.lean new file mode 100644 index 0000000000..76870872c4 --- /dev/null +++ b/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 diff --git a/tests/leanpkg/builtin_attr/leanpkg.toml b/tests/leanpkg/builtin_attr/leanpkg.toml new file mode 100644 index 0000000000..155f689776 --- /dev/null +++ b/tests/leanpkg/builtin_attr/leanpkg.toml @@ -0,0 +1,3 @@ +[package] +name = "UserAttr" +version = "0.1"