fix: some ExtraModUses (#10620)

This PR records extra mod uses that previously caused wrong unnecessary
import reports from shake.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/Lean/Elab/Command.lean

@@ -599,7 +599,6 @@ macro expansion etc.
 def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
   withReader ({ · with suppressElabErrors :=
     stx.hasMissing && !showPartialSyntaxErrors.get (← getOptions) }) do
-  recordUsedSyntaxKinds stx
   -- initialize quotation context using hash of input string
   let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false)
   withInitQuotContext (ss?.map (hash ·.toString.trim)) do
@@ -612,6 +611,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       -- `end` command of the `in` macro would be skipped and the option would be leaked to the outside!
       elabCommand stx
     finally
+      -- This call could be placed at a prior point in this function except that it
+      -- would then record uses of `#guard_msgs` before that elaborator is run, which
+      -- would increase noise in related tests. Thus all other things being equal, we
+      -- place it here.
+      recordUsedSyntaxKinds stx
       -- Make sure `snap?` is definitely resolved; we do not use it for reporting as `#guard_msgs` may
       -- be the caller of this function and add new messages and info trees
       if let some snap := (← read).snap? then

src/Lean/Elab/ErrorExplanation.lean

@@ -101,11 +101,12 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do
 open Command in
 @[builtin_command_elab registerErrorExplanationStx] def elabRegisterErrorExplanation : CommandElab
 | `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do
-  unless (← getEnv).contains ``Lean.ErrorExplanation do
+  unless (← getEnv).contains ``ErrorExplanation.Metadata do
     throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file"
+  recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true)
   let tp := mkConst ``ErrorExplanation.Metadata
   let metadata ← runTermElabM <| fun _ => unsafe do
-    let e ← elabTerm t tp
+    let e ← elabTermEnsuringType t tp
     if e.hasSyntheticSorry then throwAbortTerm
     evalExpr ErrorExplanation.Metadata tp e
   let name := id.getId

src/Lean/Elab/Quotation.lean

@@ -134,6 +134,8 @@ private partial def quoteSyntax : Syntax → TermElabM Term
     -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
     -- See the paper for details.
     let consts ← resolveGlobalName val
+    -- Record all constants to make sure they can still be resolved after shaking imports
+    consts.forM fun (n, _) => recordExtraModUseFromDecl (isMeta := false) n
     -- extension of the paper algorithm: also store unique section variable names as top-level scopes
     -- so they can be captured and used inside the section, but not outside
     let sectionVars := resolveSectionVariable (← read).sectionVars val

src/Lean/Elab/Syntax.lean

@@ -94,6 +94,7 @@ def elabParserName? (stx : Syntax.Ident) (checkMeta := true) : TermElabM (Option
   | [n@(.parser parser _)] =>
     if checkMeta && getIRPhases (← getEnv) parser == .runtime then
       throwError m!"Declaration `{.ofConstName parser}` must be marked or imported as `meta` to be used as parser"
+    recordExtraModUseFromDecl (isMeta := true) parser
     addTermInfo' stx (Lean.mkConst parser)
     return n
   | [n@(.alias _)] =>

src/Lean/Elab/Util.lean

@@ -122,8 +122,10 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa
     evalKey       := fun _ stx => do
       let kind ← syntaxNodeKindOfAttrParam parserNamespace stx
       /- Recall that a `SyntaxNodeKind` is often the name of the parser, but this is not always true, and we must check it. -/
-      if (← getEnv).contains kind && (← getInfoState).enabled then
-        addConstInfo stx[1] kind none
+      if (← getEnv).contains kind then
+        recordExtraModUseFromDecl (isMeta := false) kind
+        if (← getInfoState).enabled then
+          addConstInfo stx[1] kind none
       return kind
     onAdded       := fun builtin declName kind => do
       if builtin then

src/Lean/KeyedDeclsAttribute.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.ScopedEnvExtension
 import Lean.Compiler.InitAttr
 import Lean.Compiler.IR.CompilerM
+import Lean.ExtraModUses
 
 public section
 
@@ -43,8 +44,10 @@ structure Def (γ : Type) where
   evalKey (builtin : Bool) (stx : Syntax) : AttrM Key := private_decl% (do
     let stx ← Attribute.Builtin.getIdent stx
     let kind := stx.getId
-    if (← getEnv).contains kind && (← Elab.getInfoState).enabled then
-      Elab.addConstInfo stx kind none
+    if (← getEnv).contains kind then
+      recordExtraModUseFromDecl (isMeta := false) kind
+      if (← Elab.getInfoState).enabled then
+        Elab.addConstInfo stx kind none
     pure kind)
   onAdded (builtin : Bool) (declName : Name) (key : Key) : AttrM Unit := pure ()
   deriving Inhabited

src/Lean/Linter/MissingDocs.lean

@@ -95,6 +95,7 @@ builtin_initialize
       let decl ← getConstInfo declName
       let fnNameStx ← Attribute.Builtin.getIdent stx
       let key ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
+      recordExtraModUseFromDecl (isMeta := false) key
       unless decl.levelParams.isEmpty && (decl.type == .const ``Handler [] || decl.type == .const ``SimpleHandler []) do
         throwError m!"Unexpected type for missing docs handler: Expected `{.ofConstName ``Handler}` or \
           `{.ofConstName ``SimpleHandler}`, but `{declName}` has type{indentExpr decl.type}"

src/Lean/Meta/Coe.lean

@@ -33,6 +33,15 @@ coercions.
 def isCoeDecl (env : Environment) (declName : Name) : Bool :=
   coeDeclAttr.hasTag env declName
 
+/-- Recurse through projection functions (e.g. `(f a b c).fst.snd` => `f`) -/
+private partial def recProjTarget (e : Expr) (nm : Name := e.getAppFn.constName!) : MetaM Name := do
+  let some info ← getProjectionFnInfo? nm | return nm
+  let target := e.getArgD info.numParams (.sort .zero)
+  if target.getAppFn.isConst then
+    recProjTarget target
+  else
+    return nm
+
 /-- Expand coercions occurring in `e` -/
 partial def expandCoe (e : Expr) : MetaM Expr :=
   withReducibleAndInstances do
@@ -41,11 +50,13 @@ partial def expandCoe (e : Expr) : MetaM Expr :=
       if f.isConst then
         let declName := f.constName!
         if isCoeDecl (← getEnv) declName then
-          for arg in e.getAppArgs do
-            -- The following should record at least the top-level instance as a dependency, which
-            -- appears to be good enough for now.
-            if let .const n .. := arg then
-              recordExtraModUseFromDecl (isMeta := false) n
+          /-
+          Unfolding an instance projection corresponds to unfolding the target of the projection
+          (and then reducing the projection). Thus we can recursively visit projections before
+          recording the declaration. We shouldn't need to record any other arguments because they
+          should still appear after unfolding (unless there are unused variables in the instances).
+          -/
+          recordExtraModUseFromDecl (isMeta := false) (← recProjTarget e)
           if let some e ← unfoldDefinition? e then
             return .visit e.headBeta
       return .continue

src/Lean/Parser/Tactic/Doc.lean

@@ -12,6 +12,7 @@ import Lean.DocString.Extension
 import Lean.Elab.InfoTree.Main
 meta import Lean.Parser.Attr
 import Lean.Parser.Extension
+import Lean.ExtraModUses
 
 public section
 
@@ -80,6 +81,7 @@ builtin_initialize
         | throwError "Invalid `[{name}]` attribute syntax"
 
       let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
+      recordExtraModUseFromDecl (isMeta := false) tgtName
 
       if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "`{tgtName}` is not a tactic"
       -- If the target is a known syntax kind, ensure that it's a tactic

src/Lean/ParserCompiler/Attribute.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Attributes
 public import Lean.Compiler.InitAttr
 public import Lean.ToExpr
+import Lean.ExtraModUses
 
 public section
 
@@ -35,6 +36,7 @@ def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by
     add   := fun decl stx _ => do
       let env ← getEnv
       let parserDeclName ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      recordExtraModUseFromDecl (isMeta := false) parserDeclName
       setEnv <| ext.addEntry env (parserDeclName, decl)
   }
   registerBuiltinAttribute attrImpl

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -13,6 +13,7 @@ public import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 import Lean.Elab.InfoTree.Main
 meta import Init.Data.String.Basic
 meta import Init.Data.ToString.Name
+import Lean.ExtraModUses
 
 public section
 
@@ -120,6 +121,7 @@ unsafe builtin_initialize delabAttribute : KeyedDeclsAttribute Delab ←
       if (← Elab.getInfoState).enabled && kind.getRoot == `app then
         let c := kind.replacePrefix `app .anonymous
         if (← getEnv).contains c then
+          recordExtraModUseFromDecl (isMeta := false) c
           Elab.addConstInfo stx c none
       pure kind
   }
@@ -470,7 +472,9 @@ unsafe builtin_initialize appUnexpanderAttribute : KeyedDeclsAttribute Unexpande
     descr := "Register an unexpander for applications of a given constant.",
     valueTypeName := `Lean.PrettyPrinter.Unexpander
     evalKey := fun _ stx => do
-      Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      let id ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      recordExtraModUseFromDecl (isMeta := false) id
+      return id
   }
 
 end Delaborator

src/Lean/PrettyPrinter/Formatter.lean

@@ -13,6 +13,7 @@ public import Lean.KeyedDeclsAttribute
 public import Lean.ParserCompiler.Attribute
 public import Lean.PrettyPrinter.Basic
 public import Lean.PrettyPrinter.Delaborator.Options
+import Lean.ExtraModUses
 
 public section
 
@@ -84,8 +85,10 @@ unsafe builtin_initialize formatterAttribute : KeyedDeclsAttribute Formatter ←
       -- synthesize a formatter for it immediately, so we just check for a declaration in this case
       unless (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id do
         throwError "Invalid `[formatter]` argument: Unknown syntax kind `{id}`"
-      if (← getEnv).contains id && (← Elab.getInfoState).enabled then
-        Elab.addConstInfo stx id none
+      if (← getEnv).contains id then
+        recordExtraModUseFromDecl (isMeta := false) id
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx id none
       pure id
   }
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -11,6 +11,7 @@ public import Lean.Parser.StrInterpolation
 public import Lean.ParserCompiler.Attribute
 public import Lean.PrettyPrinter.Basic
 public import Lean.PrettyPrinter.Delaborator.Options
+import Lean.ExtraModUses
 
 public section
 
@@ -139,8 +140,10 @@ unsafe builtin_initialize parenthesizerAttribute : KeyedDeclsAttribute Parenthes
       -- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
       unless (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id do
         throwError "Invalid `[parenthesizer]` argument: Unknown syntax kind `{id}`"
-      if (← getEnv).contains id && (← Elab.getInfoState).enabled then
-        Elab.addConstInfo stx id none
+      if (← getEnv).contains id then
+        recordExtraModUseFromDecl (isMeta := false) id
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx id none
       pure id
   }
 
@@ -168,8 +171,10 @@ unsafe builtin_initialize categoryParenthesizerAttribute : KeyedDeclsAttribute C
       let id := stx.getId
       let some cat := (Parser.parserExtension.getState env).categories.find? id
         | throwError "Invalid `[category_parenthesizer]` argument: Unknown parser category `{toString id}`"
-      if (← Elab.getInfoState).enabled && (← getEnv).contains cat.declName then
-        Elab.addConstInfo stx cat.declName none
+      if (← getEnv).contains cat.declName then
+        recordExtraModUseFromDecl (isMeta := false) cat.declName
+        if (← Elab.getInfoState).enabled then
+          Elab.addConstInfo stx cat.declName none
       pure id
   }
 

src/Lean/Server/CodeActions/Attr.lean

@@ -127,6 +127,7 @@ builtin_initialize
       let `(attr| command_code_action $args*) := stx | return
       let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
+      args.forM (recordExtraModUseFromDecl (isMeta := false))
       modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
   }
 

tests/lean/run/extraModUses.lean

@@ -0,0 +1,330 @@
+module
+
+prelude
+public import Init.Prelude
+import all Lean.ExtraModUses
+public meta import Lean.Elab.Tactic.Basic
+
+/-!
+# Test for module dependencies described by ExtraModUses
+-/
+
+meta def resetExtraModUses : Lean.CoreM Unit := do
+  Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.extraModUses · ⟨[], ∅⟩)
+  Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.isExtraRevModUseExt · ⟨[], ()⟩)
+
+meta def Lean.ExtraModUse.toImport (e : ExtraModUse) : Import :=
+  { e with }
+
+meta def showExtraModUses : Lean.CoreM Unit := do
+  Lean.logInfo m!"Entries: {toString <| (Lean.extraModUses.getEntries (← Lean.getEnv)).map (·.toImport)}\n\
+    Is rev mod use: {!(Lean.isExtraRevModUseExt.getEntries (← Lean.getEnv)).isEmpty}"
+
+/-!
+Test that the `resetExtraModUses` + `showExtraModUses` pair is working.
+-/
+
+#eval resetExtraModUses
+
+/--
+info: Entries: []
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Notation being used in a command is recorded (here `«term_+_»` from Init.Notation)
+-/
+
+#eval resetExtraModUses
+
+example := 3 + 3
+
+/--
+info: Entries: [import Init.Notation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Declarations referenced using double-quoted names are recorded.
+-/
+
+#eval resetExtraModUses
+
+def test1 := ``List.sum
+
+/--
+info: Entries: [import Init.Data.List.Basic]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Running `attribute` with declarations from an imported module causes a rev use.
+-/
+
+#eval resetExtraModUses
+
+attribute [builtin_doc] Int.natCast_add
+
+/--
+info: Entries: []
+Is rev mod use: true
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+`recommended_spelling` records a dependency.
+-/
+
+#eval resetExtraModUses
+
+recommended_spelling "id" for "id" in [id]
+
+/--
+info: Entries: [import Init.Prelude]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+`syntax` records a dependency for the syntax category
+(here Lean.Parser.Category.Term from Init.Notation).
+-/
+
+#eval resetExtraModUses
+
+syntax "hi" : term
+
+/--
+info: Entries: [import Init.Notation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Term macro expansions are tracked (here `«term_+_»` from Init.Notation)
+-/
+
+macro "macro1" : term => `(3 + 3)
+
+#eval resetExtraModUses
+
+def test2 := macro1
+
+/--
+info: Entries: [import Init.Notation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Tactic macro expansions are tracked (here `Lean.Parser.Tactic.tacticTrivial` from Init.Tactics)
+-/
+
+macro "macro2" : tactic => `(tactic| trivial)
+
+#eval resetExtraModUses
+
+public meta def test3 : True := by macro2
+
+/--
+info: Entries: [import Init.Tactics]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Tactic configuration structures are recorded.
+-/
+
+#eval resetExtraModUses
+
+public def test4 : True := by simp +contextual
+
+/--
+info: Entries: [import Init.Tactics, meta import Init.MetaTypes]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+`omega` introduces a dependency on `Init.Omega`.
+-/
+
+#eval resetExtraModUses
+
+public def test5 : Eq 1 1 := by omega
+
+/--
+info: Entries: [import Init.Tactics, import Init.Omega]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+References from `@[deprecated]` are tracked (here `Nat.add` from Init.Prelude)
+-/
+
+#eval resetExtraModUses
+
+@[deprecated Nat.add "we decided to shorten the name" (since := "1010-10-10")]
+def NaturalNumber.additionOperator := Nat.add
+
+/--
+info: Entries: [import Init.Notation, import Init.Prelude]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+References from `@[grind]` are tracked (here `List.append` from Init.Prelude)
+-/
+
+#eval resetExtraModUses
+
+attribute [grind =] List.append
+
+/--
+info: Entries: [import Init.Grind.Attr, import Init.Prelude]
+Is rev mod use: true
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Coercion instances are recorded as dependencies.
+-/
+
+#eval resetExtraModUses
+
+public def test6 : Option Bool := false
+
+/--
+info: Entries: [import Init.Data.Option.Coe, import Init.Coe]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Simp theorems (especially defeq ones) are tracked (here `Nat.pow_succ` from Init.Data.Nat.Basic)
+-/
+
+#eval resetExtraModUses
+
+def test7 : 2 ^ 8 = 256 := by simp [Nat.pow_succ]
+
+/--
+info: Entries: [import Init.Tactics, import Init.Data.Nat.Basic, import Init.Notation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+`register_error_explanation` creates a dependency on `Lean.ErrorExplanation`.
+-/
+
+#eval resetExtraModUses
+
+/-- This error never occurs. If you still get it, something went wrong, sorry -/
+register_error_explanation lean.never {
+  summary := "Not an error"
+  sinceVersion := "never"
+}
+
+/--
+info: Entries: [meta import Lean.ErrorExplanation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+The syntax node kind in `syntax` declarations get recorded as a `meta` dependency.
+-/
+
+#eval resetExtraModUses
+
+syntax "test_me " Lean.Parser.Term.ident : term
+
+/--
+info: Entries: [meta import Lean.Parser.Term, import Init.Notation]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+The syntax node kind in quotations get recorded as a `meta` dependency.
+-/
+
+#eval resetExtraModUses
+
+def test8 : Lean.MacroM Lean.Syntax := `(Lean.Parser.Command.declaration| def a := 5)
+
+/--
+info: Entries: [import Init.Notation, import Init.Coe, meta import Lean.Parser.Command]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Resolved constants from syntax quotations get added (here `List.sum` from Init.Data.List.Basic).
+-/
+
+#eval resetExtraModUses
+
+def test9 : Lean.MacroM Lean.Syntax := `(List.sum)
+
+/--
+info: Entries: [import Init.Notation, import Init.Coe, import Init.Data.List.Basic]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Elaboration attributes add dependency on the syntax node kind
+(here `Lean.Parser.Tactic.done` from Init.Tactics).
+-/
+
+public meta def myElab : Lean.Elab.Tactic.Tactic := fun _ => pure ()
+
+#eval resetExtraModUses
+
+attribute [tactic Lean.Parser.Tactic.done] myElab
+
+/--
+info: Entries: [import Init.Tactics]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+Similarly with formatters...
+-/
+
+public meta def myFormatter : Lean.PrettyPrinter.Formatter := fun _ => pure ()
+
+#eval resetExtraModUses
+
+attribute [formatter Lean.Parser.Tactic.done] myFormatter
+
+/--
+info: Entries: [import Init.Tactics]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses
+
+/-!
+... and parenthesizers
+-/
+
+public meta def myParenthesizer : Lean.PrettyPrinter.Parenthesizer := fun _ => pure ()
+
+#eval resetExtraModUses
+
+attribute [parenthesizer Lean.Parser.Tactic.done] myParenthesizer
+
+/--
+info: Entries: [import Init.Tactics]
+Is rev mod use: false
+-/
+#guard_msgs in #eval showExtraModUses