perf(Tactic/StacksAttribute): avoid initialization cost (leanprover-community#34679)

This PR improves the performace by removing the initialization cost of the `stacks` attribute. Previously, a `HashSet` of stacks tags was being created upon initialization of any file.

See [#mathlib4 > Performance cost of environment extensions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Performance.20cost.20of.20environment.20extensions/with/571319366)

Author: JovanGerb

Mathlib/Tactic/StacksAttribute.lean

@@ -44,12 +44,12 @@ structure Tag where
   comment : String
   deriving BEq, Hashable
 
-/-- Defines the `tagExt` extension for adding a `HashSet` of `Tag`s
-to the environment. -/
-initialize tagExt : SimplePersistentEnvExtension Tag (Std.HashSet Tag) ←
+/-- Defines the `tagExt` extension for storing all `Tag`s in the environment.
+`addImportedFn` is a constant function to avoid a performance overhead during initialization. -/
+initialize tagExt : SimplePersistentEnvExtension Tag (Array (Array Tag)) ←
   registerSimplePersistentEnvExtension {
-    addImportedFn := fun as => as.foldl Std.HashSet.insertMany {}
-    addEntryFn := .insert
+    addImportedFn tags := tags
+    addEntryFn tags _ := tags
   }
 
 /--
@@ -171,7 +171,8 @@ end Mathlib.StacksTag
 `getSortedStackProjectTags env` returns the array of `Tags`, sorted by alphabetical order of tag.
 -/
 private def Lean.Environment.getSortedStackProjectTags (env : Environment) : Array Tag :=
-  tagExt.getState env |>.toArray.qsort (·.tag < ·.tag)
+  let tags := PersistentEnvExtension.getState tagExt env
+  tags.2.flatten.appendList tags.1 |>.qsort (·.tag < ·.tag)
 
 /--
 `getSortedStackProjectDeclNames env tag` returns the array of declaration names of results