chore: shake: re-add attribute rev use (#11288)

Global `attribute` commands on non-local declarations are impossible to
track granularly a priori and so should be preserved by `shake` by
default. A new `shake` option could be added to ignore these
dependencies for evaluation.

src/Lean/Elab/Declaration.lean

@@ -330,6 +330,11 @@ def elabMutual : CommandElab := fun stx => do
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName
+    if (← getEnv).isImportedConst declName && attrs.any (·.kind == .global) then
+      -- If an imported declaration is marked with a global attribute, there is no good way to track
+      -- its use generally and so Shake should conservatively preserve imports of the current
+      -- module.
+      recordExtraRevUseOfCurrentModule
 
 @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
   | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do

tests/lean/run/extraModUses.lean

@@ -174,7 +174,7 @@ attribute [grind =] List.append
 
 /--
 info: Entries: [import Init.Grind.Attr, public import Init.Prelude]
-Is rev mod use: false
+Is rev mod use: true
 -/
 #guard_msgs in #eval showExtraModUses