Merge remote-tracking branch 'origin/main' into nightly-testing

ImportGraph/Imports.lean

@@ -172,6 +172,21 @@ def filterGraph (graph : NameMap (Array Name)) (filter : Name → Bool)
 
 end Lean.NameMap
 
+/--
+Returns a `List (Name × List Name)` with a key for each module `n` in `amongst`,
+whose corresponding value is the list of modules `m` in `amongst` which are transitively imported by `n`,
+but no declaration in `n` makes use of a declaration in `m`.
+
+The current implementation is too slow to run on the entirety of Mathlib,
+although it should be fine for any sequential chain of imports in Mathlib.
+-/
+def unusedTransitiveImports (amongst : List Name) : CoreM (List (Name × List Name)) := do
+  let env ← getEnv
+  let transitiveImports := env.importGraph.transitiveClosure
+  amongst.mapM fun n => do return (n,
+    let unused := (transitiveImports.find? n).getD {} \ (← env.transitivelyRequiredModules n)
+    amongst.filter (fun m => unused.contains m))
+
 /--
 Return the redundant imports (i.e. those transitively implied by another import)
 of a specified module (or the current module if `none` is specified).

ImportGraph/RequiredModules.lean

@@ -5,6 +5,29 @@ Authors: Kim Morrison
 -/
 import Lean
 
+
+namespace Lean.NameSet
+
+instance : Singleton Name NameSet where
+  singleton := fun n => (∅ : NameSet).insert n
+
+instance : Union NameSet where
+  union := fun s t => s.fold (fun t n => t.insert n) t
+
+instance : Inter NameSet where
+  inter := fun s t => s.fold (fun r n => if t.contains n then r.insert n else r) {}
+
+instance : SDiff NameSet where
+  sdiff := fun s t => t.fold (fun s n => s.erase n) s
+
+def ofList (l : List Name) : NameSet :=
+  l.foldl (fun s n => s.insert n) {}
+
+def ofArray (a : Array Name) : NameSet :=
+  a.foldl (fun s n => s.insert n) {}
+
+end Lean.NameSet
+
 namespace Lean
 
 /-- Return the name of the module in which a declaration was defined. -/
@@ -36,12 +59,12 @@ def Name.requiredModules (n : Name) : CoreM NameSet := do
   return requiredModules
 
 /--
-Return the names of the constants used in the specified declaration,
+Return the names of the constants used in the specified declarations,
 and the constants they use transitively.
 -/
-def Name.transitivelyUsedConstants (n : Name) : CoreM NameSet := do
+def NameSet.transitivelyUsedConstants (s : NameSet) : CoreM NameSet := do
   let mut usedConstants : NameSet := {}
-  let mut toProcess : NameSet := NameSet.empty.insert n
+  let mut toProcess : NameSet := s
   while !toProcess.isEmpty do
     let current := toProcess.min.get!
     toProcess := toProcess.erase current
@@ -51,33 +74,46 @@ def Name.transitivelyUsedConstants (n : Name) : CoreM NameSet := do
         toProcess := toProcess.insert m
   return usedConstants
 
+/--
+Return the names of the constants used in the specified declaration,
+and the constants they use transitively.
+-/
+def Name.transitivelyUsedConstants (n : Name) : CoreM NameSet :=
+  NameSet.transitivelyUsedConstants {n}
+
 /--
 Return the names of the modules in which constants used transitively
-in the specified declaration were defined.
+in the specified declarations were defined.
 
 Note that this will *not* account for tactics and syntax used in the declaration,
 so the results may not suffice as imports.
 -/
-def Name.transitivelyRequiredModules (n : Name) (env : Environment) : CoreM NameSet := do
+def NameSet.transitivelyRequiredModules (s : NameSet) (env : Environment) : CoreM NameSet := do
   let mut requiredModules : NameSet := {}
-  for m in (← n.transitivelyUsedConstants) do
+  for m in (← s.transitivelyUsedConstants) do
     if let some module := env.getModuleFor? m then
       requiredModules := requiredModules.insert module
   return requiredModules
 
+/--
+Return the names of the modules in which constants used transitively
+in the specified declaration were defined.
+
+Note that this will *not* account for tactics and syntax used in the declaration,
+so the results may not suffice as imports.
+-/
+def Name.transitivelyRequiredModules (n : Name) (env : Environment) : CoreM NameSet :=
+  NameSet.transitivelyRequiredModules {n} env
+
 /--
 Finds all constants defined in the specified module,
 and identifies all modules containing constants which are transitively required by those constants.
 -/
 def Environment.transitivelyRequiredModules (env : Environment) (module : Name) : CoreM NameSet := do
-  let mut requiredModules : NameSet := {}
-  for (_, ci) in env.constants.map₁.toList do
-    if !ci.name.isInternal then
-    if let some m := env.getModuleFor? ci.name then
-      if m = module then
-        for r in (← ci.name.transitivelyRequiredModules env) do
-          requiredModules := requiredModules.insert r
-  return requiredModules
+  let constants := env.constants.map₁.values.map (·.name)
+    |>.filter (! ·.isInternal)
+    |>.filter (env.getModuleFor? · = some module)
+  (NameSet.ofList constants).transitivelyRequiredModules env
 
 /--
 Return the names of the modules in which constants used in the current file were defined.

ImportGraphTest/Imports.lean

@@ -24,6 +24,36 @@ ImportGraph.RequiredModules
 
 open Elab Command
 
+
+/--
+Reports unused transitive imports amongst the specified modules.
+-/
+elab "#unused_transitive_imports" names:ident* : command => do
+  let imports := (names.map Syntax.getId).toList
+  let unused ← Elab.Command.liftCoreM (unusedTransitiveImports imports)
+  for (n, u) in unused do
+    if !u.isEmpty then
+    logInfo <| s!"Transitively unused imports of {n}:\n{"\n".intercalate (u.map (fun i => s!"  {i}"))}"
+
+-- This test case can be removed after nightly-2024-10-24, because these imports have been cleaned up.
+/--
+info: Transitively unused imports of Init.Control.StateRef:
+  Init.System.IO
+---
+info: Transitively unused imports of Init.System.IO:
+  Init.Control.Reader
+-/
+#guard_msgs in
+#unused_transitive_imports Init.Control.StateRef Init.System.IO Init.Control.Reader Init.Control.Basic
+
+-- This is a spurious unused transitive import, because it relies on notation from `Init.Core`.
+/--
+info: Transitively unused imports of Init.Control.Basic:
+  Init.Core
+-/
+#guard_msgs in
+#unused_transitive_imports Init.Control.Basic Init.Core
+
 elab "#transitivelyRequiredModules_test" : command => do
   let env ← getEnv
   let unused ← liftCoreM <| env.transitivelyRequiredModules `ImportGraph.RequiredModules