fix(Tactic/Linter): upstreamableDecl should treat structures like…

… `def`s (#19360)

Reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/upstreamableDecl.20linter.20bug/near/483790949

We want to treat a `structure`/`inductive` declaration in the current file just like a `def` for the `upstreamableDecl` linter: potentially place a warning on the `structure` itself, but otherwise don't place warnings on downstream uses.

There's a small complication where `inductive` declarations are reported to depend on their own constructors. I couldn't find a good way to determine whether any given constant is indeed a constructor declared in some given piece of syntax, so instead we allow depending on constructors just like we allow depending on theorems.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Mathlib/Tactic/Linter/UpstreamableDecl.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Anne Baanen
 -/
 import ImportGraph.Imports
-import Mathlib.Lean.Expr.Basic
 import Mathlib.Tactic.MinImports
 
 /-! # The `upstreamableDecl` linter
@@ -21,8 +20,12 @@ def Lean.Name.isLocal (env : Environment) (decl : Name) : Bool :=
 
 open Mathlib.Command.MinImports
 
-/-- Does the declaration with this name depend on `def`s in the current file? -/
-def Lean.Environment.localDefDependencies (env : Environment) (stx id : Syntax) :
+/-- Does the declaration with this name depend on definitions in the current file?
+
+Here, "definition" means everything that is not a theorem, and so includes `def`,
+`structure`, `inductive`, etc.
+-/
+def Lean.Environment.localDefinitionDependencies (env : Environment) (stx id : Syntax) :
     CommandElabM Bool := do
   let declName : NameSet ← try
     NameSet.ofList <$> resolveGlobalConst id
@@ -37,7 +40,14 @@ def Lean.Environment.localDefDependencies (env : Environment) (stx id : Syntax)
 
   let deps ← liftCoreM <| immediateDeps.transitivelyUsedConstants
   let constInfos := deps.toList.filterMap env.find?
-  let defs := constInfos.filter (·.isDef)
+  -- We allow depending on theorems and constructors.
+  -- We explicitly allow constructors since `inductive` declarations are reported to depend on their
+  -- own constructors, and we want inductives to behave the same as definitions, so place one
+  -- warning on the inductive itself but nothing on its downstream uses.
+  -- (There does not seem to be an easy way to determine, given `Syntax` and `ConstInfo`,
+  -- whether the `ConstInfo` is a constructor declared in this piece of `Syntax`.)
+  let defs := constInfos.filter (fun constInfo => !(constInfo.isTheorem || constInfo.isCtor))
+
   return defs.any fun constInfo => !(declName.contains constInfo.name) && constInfo.name.isLocal env
 
 namespace Mathlib.Linter
@@ -72,7 +82,7 @@ def upstreamableDeclLinter : Linter where run := withSetOptionIn fun stx ↦ do
       let minImports := getIrredundantImports env (← getAllImports stx id)
       match minImports with
       | ⟨(RBNode.node _ .leaf upstream _ .leaf), _⟩ => do
-        if !(← env.localDefDependencies stx id) then
+        if !(← env.localDefinitionDependencies stx id) then
           let p : GoToModuleLinkProps := { modName := upstream }
           let widget : MessageData := .ofWidget
             (← liftCoreM <| Widget.WidgetInstance.ofHash

MathlibTest/MinImports.lean

@@ -165,4 +165,28 @@ def def_with_multiple_dependencies :=
   let _ := Mathlib.Meta.NormNum.evalNatDvd
   false
 
+/-! Structures and inductives should be treated just like definitions. -/
+
+/--
+
+warning: Consider moving this declaration to the module Mathlib.Data.Nat.Notation.
+note: this linter can be disabled with `set_option linter.upstreamableDecl false`
+-/
+#guard_msgs in
+structure ProposeToMoveThisStructure where
+  foo : ℕ
+
+/--
+warning: Consider moving this declaration to the module Mathlib.Data.Nat.Notation.
+note: this linter can be disabled with `set_option linter.upstreamableDecl false`
+-/
+#guard_msgs in
+inductive ProposeToMoveThisInductive where
+| foo : ℕ → ProposeToMoveThisInductive
+| bar : ℕ → ProposeToMoveThisInductive → ProposeToMoveThisInductive
+
+-- This theorem depends on a local inductive, so should not be moved.
+#guard_msgs in
+theorem theorem_with_local_inductive : Nonempty ProposeToMoveThisInductive := ⟨.foo 0⟩
+
 end Linter.UpstreamableDecl