diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean
index f8552d5dc6..e9c2424054 100644
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
@@ -3,34 +3,34 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.Attributes
+import Lake.Util.OrderedTagAttribute
 
 open Lean
 namespace Lake
 
-initialize packageAttr : TagAttribute ←
-  registerTagAttribute `package "mark a definition as a Lake package configuration"
+initialize packageAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package "mark a definition as a Lake package configuration"
 
-initialize packageDepAttr : TagAttribute ←
-  registerTagAttribute `package_dep "mark a definition as a Lake package dependency"
+initialize packageDepAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
-initialize scriptAttr : TagAttribute ←
-  registerTagAttribute `script "mark a definition as a Lake script"
+initialize scriptAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `script "mark a definition as a Lake script"
 
-initialize leanLibAttr : TagAttribute ←
-  registerTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
+initialize leanLibAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
 
-initialize leanExeAttr : TagAttribute ←
-  registerTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
+initialize leanExeAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
 
-initialize externLibAttr : TagAttribute ←
-  registerTagAttribute `extern_lib "mark a definition as a Lake external library target"
+initialize externLibAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
 
-initialize targetAttr : TagAttribute ←
-  registerTagAttribute `target "mark a definition as a custom Lake target"
+initialize targetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `target "mark a definition as a custom Lake target"
 
-initialize defaultTargetAttr : TagAttribute ←
-  registerTagAttribute `default_target "mark a Lake target as the package's default"
+initialize defaultTargetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `default_target "mark a Lake target as the package's default"
     fun name => do
       let valid ← getEnv <&> fun env =>
         leanLibAttr.hasTag env name ||
@@ -40,11 +40,11 @@ initialize defaultTargetAttr : TagAttribute ←
       unless valid do
         throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
-initialize moduleFacetAttr : TagAttribute ←
-  registerTagAttribute `module_facet "mark a definition as a Lake module facet"
+initialize moduleFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
 
-initialize packageFacetAttr : TagAttribute ←
-  registerTagAttribute `package_facet "mark a definition as a Lake package facet"
+initialize packageFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet"
 
-initialize libraryFacetAttr : TagAttribute ←
-  registerTagAttribute `library_facet "mark a definition as a Lake library facet"
+initialize libraryFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet"
diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean
index 223fdbede8..abd65628da 100644
--- a/Lake/Load/Main.lean
+++ b/Lake/Load/Main.lean
@@ -20,8 +20,7 @@ namespace Lake
 
 /-- Load the tagged `Dependency` definitions from a package configuration environment. -/
 def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array Dependency) := do
-  packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
-    return arr.push <| ← evalConstCheck env opts Dependency ``Dependency name
+  (packageDepAttr.ext.getState env).mapM (evalConstCheck env opts Dependency ``Dependency)
 
 def loadDepPackage (parentPkg : Package) (result : MaterializeResult)
 (dep : Dependency) : LogIO Package := do
diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean
index 53ff7a8575..dab1ce1a6f 100644
--- a/Lake/Load/Package.lean
+++ b/Lake/Load/Package.lean
@@ -36,16 +36,16 @@ where
 
 /-- Construct a `NameMap` from the declarations tagged with `attr`. -/
 def mkTagMap
-(env : Environment) (attr : TagAttribute)
+(env : Environment) (attr : OrderedTagAttribute)
 [Monad m]  (f : Name → m α) : m (NameMap α) :=
-  attr.ext.getState env |>.foldM (init := {}) fun map declName =>
+  attr.ext.getState env |>.foldlM (init := {}) fun map declName =>
     return map.insert declName <| ← f declName
 
 /-- Construct a `DNameMap` from the declarations tagged with `attr`. -/
 def mkDTagMap
-(env : Environment) (attr : TagAttribute)
+(env : Environment) (attr : OrderedTagAttribute)
 [Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) :=
-  attr.ext.getState env |>.foldM (init := {}) fun map declName =>
+  attr.ext.getState env |>.foldlM (init := {}) fun map declName =>
     return map.insert declName <| ← f declName
 
 /-- Load a `PackageConfig` from a configuration environment. -/
@@ -89,7 +89,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
       else
         error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`"
     | .error e => error e
-  let defaultTargets := defaultTargetAttr.ext.getState env |>.fold (·.push ·) #[]
+  let defaultTargets := defaultTargetAttr.ext.getState env
 
   -- Fill in the Package
   return {self with
diff --git a/Lake/Util/OrderedTagAttribute.lean b/Lake/Util/OrderedTagAttribute.lean
new file mode 100644
index 0000000000..5c4ef60d30
--- /dev/null
+++ b/Lake/Util/OrderedTagAttribute.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean.Attributes
+
+open Lean
+namespace Lake
+
+structure OrderedTagAttribute where
+  attr : AttributeImpl
+  ext  : PersistentEnvExtension Name Name (Array Name)
+  deriving Inhabited
+
+def registerOrderedTagAttribute (name : Name) (descr : String)
+    (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) : IO OrderedTagAttribute := do
+  let ext ← registerPersistentEnvExtension {
+    name            := ref
+    mkInitial       := pure {}
+    addImportedFn   := fun _ _ => pure {}
+    addEntryFn      := fun s n => s.push n
+    exportEntriesFn := fun es => es
+    statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
+  }
+  let attrImpl : AttributeImpl := {
+    ref   := ref
+    name  := name
+    descr := descr
+    add   := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      let env ← getEnv
+      unless (env.getModuleIdxFor? decl).isNone do
+        throwError "invalid attribute '{name}', declaration is in an imported module"
+      validate decl
+      modifyEnv fun env => ext.addEntry env decl
+  }
+  registerBuiltinAttribute attrImpl
+  return { attr := attrImpl, ext }
+
+def OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (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