merge main

ImportGraph.lean

@@ -3,3 +3,4 @@ import ImportGraph.Imports
 import ImportGraph.CurrentModule
 import ImportGraph.Lean.Name
 import ImportGraph.RequiredModules
+import ImportGraph.UnusedTransitiveImports

ImportGraph/Cli.lean

@@ -18,36 +18,38 @@ open ImportGraph
 /--
 Write an import graph, represented as a `NameMap (Array Name)` to the ".dot" graph format.
 * Nodes in the `unused` set will be shaded light gray.
-* If `markedModule` is provided:
-  * Nodes which start with the `markedModule` will be highlighted in green and drawn closer together.
+* If `markedPackage` is provided:
+  * Nodes which start with the `markedPackage` will be highlighted in green and drawn closer together.
   * Edges from `directDeps` into the module are highlighted in green
   * Nodes in `directDeps` are marked with a green border and green text.
 -/
 def asDotGraph
     (graph : NameMap (Array Name))
     (unused : NameSet := {})
     (header := "import_graph")
-    (markedModule : Option Name := none)
-    (directDeps : NameSet := {}) :
+    (markedPackage : Option Name := none)
+    (directDeps : NameSet := {})
+    (from_ to : NameSet := {}):
     String := Id.run do
 
   let mut lines := #[s!"digraph \"{header}\" " ++ "{"]
   for (n, is) in graph do
-    if markedModule.isSome ∧ directDeps.contains n then
+    let shape := if from_.contains n then "invhouse" else if to.contains n then "house" else "ellipse"
+    if markedPackage.isSome ∧ directDeps.contains n then
       -- note: `fillcolor` defaults to `color` if not specified
       let fill := if unused.contains n then "#e0e0e0" else "white"
-      lines := lines.push s!"  \"{n}\" [style=filled, fontcolor=\"#4b762d\", color=\"#71b144\", fillcolor=\"{fill}\", penwidth=2];"
+      lines := lines.push s!"  \"{n}\" [style=filled, fontcolor=\"#4b762d\", color=\"#71b144\", fillcolor=\"{fill}\", penwidth=2, shape={shape}];"
     else if unused.contains n then
-      lines := lines.push s!"  \"{n}\" [style=filled, fillcolor=\"#e0e0e0\"];"
-    else if isInModule markedModule n then
+      lines := lines.push s!"  \"{n}\" [style=filled, fillcolor=\"#e0e0e0\", shape={shape}];"
+    else if isInModule markedPackage n then
       -- mark node
-      lines := lines.push s!"  \"{n}\" [style=filled, fillcolor=\"#96ec5b\"];"
+      lines := lines.push s!"  \"{n}\" [style=filled, fillcolor=\"#96ec5b\", shape={shape}];"
     else
-      lines := lines.push s!"  \"{n}\";"
+      lines := lines.push s!"  \"{n}\" [shape={shape}];"
     -- Then add edges
     for i in is do
-      if isInModule markedModule n then
-        if isInModule markedModule i then
+      if isInModule markedPackage n then
+        if isInModule markedPackage i then
           -- draw the main project close together
           lines := lines.push s!"  \"{i}\" -> \"{n}\" [weight=100];"
         else
@@ -76,37 +78,37 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
        | some _ => acc.insert "dot" ) {}
 
   let to ← match args.flag? "to" with
-  | some to => pure <| to.as! ModuleName
-  | none => getCurrentModule
-  let from? := match args.flag? "from" with
-  | some fr => some <| fr.as! ModuleName
+  | some to => pure <| to.as! (Array ModuleName)
+  | none => pure #[← getCurrentModule]
+  let from? : Option (Array Name) := match args.flag? "from" with
+  | some fr => some <| fr.as! (Array ModuleName)
   | none => none
   initSearchPath (← findSysroot)
 
-  let outFiles ← try unsafe withImportModules #[{module := to}] {} (trustLevel := 1024) fun env => do
-    let p := ImportGraph.getModule to
+  let outFiles ← try unsafe withImportModules (to.map ({module := ·})) {} (trustLevel := 1024) fun env => do
+    let toModule := ImportGraph.getModule to[0]!
     let mut graph := env.importGraph
     let unused ←
       match args.flag? "to"  with
       | some _ =>
         let ctx := { options := {}, fileName := "<input>", fileMap := default }
         let state := { env }
-        let used ← Prod.fst <$> (CoreM.toIO (env.transitivelyRequiredModules to) ctx state)
+        let used ← Prod.fst <$> (CoreM.toIO (env.transitivelyRequiredModules' to.toList) ctx state)
+        let used := used.fold (init := NameSet.empty) (fun s _ t => s ∪ t)
         pure <| graph.fold (fun acc n _ => if used.contains n then acc else acc.insert n) NameSet.empty
       | none => pure NameSet.empty
     if let Option.some f := from? then
-      graph := graph.downstreamOf (NameSet.empty.insert f)
-    let toModule := ImportGraph.getModule to
+      graph := graph.downstreamOf (NameSet.ofArray f)
     let includeLean := args.hasFlag "include-lean"
     let includeStd := args.hasFlag "include-std" || includeLean
     let includeDeps := args.hasFlag "include-deps" || includeStd
     -- Note: `includeDirect` does not imply `includeDeps`!
-    -- e.g. if the module contains `import Lean`, the node `Lean` will be included with
+    -- e.g. if the package contains `import Lean`, the node `Lean` will be included with
     -- `--include-direct`, but not included with `--include-deps`.
     let includeDirect := args.hasFlag "include-direct"
 
-    -- `directDeps` contains files which are not in the module
-    -- but directly imported by a file in the module
+    -- `directDeps` contains files which are not in the package
+    -- but directly imported by a file in the package
     let directDeps : NameSet := graph.fold (init := .empty) (fun acc n deps =>
       if toModule.isPrefixOf n then
         deps.filter (!toModule.isPrefixOf ·) |>.foldl (init := acc) NameSet.insert
@@ -142,26 +144,27 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
     if !args.hasFlag "show-transitive" then
       graph := graph.transitiveReduction
 
-    let markedModule : Option Name := if args.hasFlag "mark-module" then p else none
+    let markedPackage : Option Name := if args.hasFlag "mark-package" then toModule else none
 
     -- Create all output files that are requested
     let mut outFiles : Std.HashMap String String := {}
     if extensions.contains "dot" then
-      let dotFile := asDotGraph graph (unused := unused) (markedModule := markedModule) (directDeps := directDeps)
+      let dotFile := asDotGraph graph (unused := unused) (markedPackage := markedPackage) (directDeps := directDeps)
+        (to := NameSet.ofArray to) (from_ := NameSet.ofArray (from?.getD #[]))
       outFiles := outFiles.insert "dot" dotFile
     if extensions.contains "gexf" then
       -- filter out the top node as it makes the graph less pretty
       let graph₂ := match args.flag? "to" with
-        | none => graph.filter (fun n _ => n != to)
+        | none => graph.filter (fun n _ => !to.contains n)
         | some _ => graph
-      let gexfFile := Graph.toGexf graph₂ p env
+      let gexfFile := Graph.toGexf graph₂ toModule env
       outFiles := outFiles.insert "gexf" gexfFile
     return outFiles
 
   catch err =>
     -- TODO: try to build `to` first, so this doesn't happen
-    throw <| IO.userError <| s!"{err}\nIf the error above says `unknown package`, " ++
-      s!"try if `lake build {to}` fixes the issue"
+    throw <| IO.userError <| s!"{err}\nIf the error above says `object file ... does not exist`, " ++
+      s!"try if `lake build {" ".intercalate (to.toList.map Name.toString)}` fixes the issue"
     throw err
 
   match args.variableArgsAs! String with

ImportGraph/Imports.lean

@@ -176,15 +176,13 @@ 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
+def unusedTransitiveImports (amongst : List Name) (verbose : Bool := false) : CoreM (List (Name × List Name)) := do
   let env ← getEnv
   let transitiveImports := env.importGraph.transitiveClosure
+  let transitivelyRequired ← env.transitivelyRequiredModules' amongst verbose
   amongst.mapM fun n => do return (n,
-    let unused := (transitiveImports.find? n).getD {} \ (← env.transitivelyRequiredModules n)
+    let unused := (transitiveImports.find? n).getD {} \ (transitivelyRequired.find? n |>.getD {})
     amongst.filter (fun m => unused.contains m))
 
 /--

ImportGraph/RequiredModules.lean

@@ -115,6 +115,57 @@ def Environment.transitivelyRequiredModules (env : Environment) (module : Name)
     |>.filter (env.getModuleFor? · = some module)
   (NameSet.ofList constants).transitivelyRequiredModules env
 
+/--
+Computes all the modules transitively required by the specified modules.
+Should be equivalent to calling `transitivelyRequiredModules` on each module, but shares more of the work.
+-/
+partial def Environment.transitivelyRequiredModules' (env : Environment) (modules : List Name) (verbose : Bool := false) :
+    CoreM (NameMap NameSet) := do
+  let N := env.header.moduleNames.size
+  let mut c2m : NameMap (BitVec N) := {}
+  let mut pushed : NameSet := {}
+  let mut result : NameMap NameSet := {}
+  for m in modules do
+    if verbose then
+      IO.println s!"Processing module {m}"
+    let mut r : BitVec N := 0
+    for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do
+      if ! n.isInternal then
+      -- This is messy: Mathlib is big enough that writing a recursive function causes a stack overflow.
+      -- So we use an explicit stack instead. We visit each constant twice:
+      -- once to record the constants transitively used by it,
+      -- and again to record the modules which defined those constants.
+      let mut stack : List (Name × Option NameSet) := [⟨n, none⟩]
+      pushed := pushed.insert n
+      while !stack.isEmpty do
+        match stack with
+        | [] => panic! "Stack is empty"
+        | (c, used?) :: tail =>
+          stack := tail
+          match used? with
+          | none =>
+            if !c2m.contains c then
+              let used := (← getConstInfo c).getUsedConstantsAsSet
+              stack := ⟨c, some used⟩ :: stack
+              for u in used do
+                if !pushed.contains u then
+                  stack := ⟨u, none⟩ :: stack
+                  pushed := pushed.insert u
+          | some used =>
+            let usedModules : NameSet :=
+              used.fold (init := {}) (fun s u => if let some m := env.getModuleFor? u then s.insert m else s)
+            let transitivelyUsed : BitVec N :=
+              used.fold (init := toBitVec usedModules) (fun s u => s ||| ((c2m.find? u).getD 0))
+            c2m := c2m.insert c transitivelyUsed
+      r := r ||| ((c2m.find? n).getD 0)
+    result := result.insert m (toNameSet r)
+  return result
+where
+  toBitVec {N : Nat} (s : NameSet) : BitVec N :=
+    s.fold (init := 0) (fun b n => b ||| BitVec.twoPow _ ((env.header.moduleNames.getIdx? n).getD 0))
+  toNameSet {N : Nat} (b : BitVec N) : NameSet :=
+    env.header.moduleNames.zipWithIndex.foldl (init := {}) (fun s (n, i) => if b.getLsbD i then s.insert n else s)
+
 /--
 Return the names of the modules in which constants used in the current file were defined.
 

ImportGraph/UnusedTransitiveImports.lean

@@ -0,0 +1,23 @@
+import ImportGraph.Imports
+
+open Lean
+
+def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do
+  searchPathRef.set compile_time_search_path%
+  unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024)
+    fun env => Prod.fst <$> Core.CoreM.toIO
+        (ctx := { fileName := "<CoreM>", fileMap := default }) (s := { env := env }) do f
+
+/--
+`lake exe unused_transitive_imports m1 m2 ...`
+
+For each specified module `m`, prints those `n` from the argument list which are imported, but transitively unused by `m`.
+-/
+def main (args : List String) : IO UInt32 := do
+  let (flags, args) := args.partition (fun s => s.startsWith "-")
+  let mut modules := args.map (fun s => s.toName)
+  Core.withImportModules modules.toArray do
+    let r ← unusedTransitiveImports modules (verbose := flags.contains "-v" || flags.contains "--verbose")
+    for (n, u) in r do
+      IO.println s!"{n}: {u}"
+    return 0

ImportGraphTest/Imports.lean

@@ -1,5 +1,6 @@
 import ImportGraph.Imports
 import ImportGraph.RequiredModules
+import ImportGraphTest.Used
 
 open Lean
 
@@ -36,6 +37,7 @@ elab "#unused_transitive_imports" names:ident* : command => do
     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.
+-- It should be replaced with another test case!
 /--
 info: Transitively unused imports of Init.Control.StateRef:
   Init.System.IO
@@ -46,6 +48,13 @@ info: Transitively unused imports of Init.System.IO:
 #guard_msgs in
 #unused_transitive_imports Init.Control.StateRef Init.System.IO Init.Control.Reader Init.Control.Basic
 
+/--
+info: Transitively unused imports of ImportGraphTest.Used:
+  ImportGraphTest.Unused
+-/
+#guard_msgs in
+#unused_transitive_imports ImportGraphTest.Used ImportGraphTest.Unused Init.Control.Reader
+
 -- This is a spurious unused transitive import, because it relies on notation from `Init.Core`.
 /--
 info: Transitively unused imports of Init.Control.Basic:

ImportGraphTest/expected.dot

@@ -1,5 +1,5 @@
 digraph "import_graph" {
-  "ImportGraphTest.Unused" [style=filled, fillcolor="#e0e0e0"];
-  "ImportGraphTest.Used" [style=filled, fillcolor="#e0e0e0"];
+  "ImportGraphTest.Unused" [style=filled, fillcolor="#e0e0e0", shape=ellipse];
+  "ImportGraphTest.Used" [style=filled, fillcolor="#e0e0e0", shape=house];
   "ImportGraphTest.Unused" -> "ImportGraphTest.Used";
 }

Main.lean

@@ -16,15 +16,15 @@ def graph : Cmd := `[Cli|
    If you are working in a downstream project, use `lake exe graph --to MyProject`."
 
   FLAGS:
-    "show-transitive";    "Show transitively redundant edges."
-    to : ModuleName;      "Only show the upstream imports of the specified module."
-    "from" : ModuleName;  "Only show the downstream dependencies of the specified module."
-    "exclude-meta";       "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`."
-    "include-direct";     "Include directly imported files from other libraries"
-    "include-deps";       "Include used files from other libraries (not including Lean itself and `std`)"
-    "include-std";        "Include used files from the Lean standard library (implies `--include-deps`)"
-    "include-lean";       "Include used files from Lean itself (implies `--include-deps` and `--include-std`)"
-    "mark-module";        "Visually highlight the current module (used in combination with some `--include-XXX`)."
+    "show-transitive";         "Show transitively redundant edges."
+    "to" : Array ModuleName;   "Only show the upstream imports of the specified modules."
+    "from" : Array ModuleName; "Only show the downstream dependencies of the specified modules."
+    "exclude-meta";            "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`."
+    "include-direct";          "Include directly imported files from other libraries"
+    "include-deps";            "Include used files from other libraries (not including Lean itself and `std`)"
+    "include-std";             "Include used files from the Lean standard library (implies `--include-deps`)"
+    "include-lean";            "Include used files from Lean itself (implies `--include-deps` and `--include-std`)"
+    "mark-package";            "Visually highlight the package containing the first `--to` target (used in combination with some `--include-XXX`)."
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \

README.md

@@ -24,6 +24,11 @@ lake exe graph --to MyModule my_graph.pdf
 ```
 where `MyModule` follows the same module naming you would use to `import` it in lean. See `lake exe graph --help` for more options.
 
+You can specify multiple sources and targets e.g. as
+```bash
+lake exe graph --from MyModule1,MyModule2 --to MyModule3,MyModule4 my_graph.pdf
+```
+
 ### Troubleshoot
 
 * make sure to `lake build` your project (or the specified `--to` module) before using `lake exe graph`!
@@ -54,6 +59,12 @@ There are a few commands implemented, which help you analysing the imports of a
   (Must be run at the end of the file. Tactics and macros may result in incorrect output.)
 * `#find_home decl`: suggests files higher up the import hierarchy to which `decl` could be moved.
 
+## Other executables
+
+`lake exe unused_transitive_imports m1 m2 ...`
+
+For each specified module `m`, prints those `n` from the argument list which are imported, but transitively unused by `m`.
+
 ## Installation
 
 The installation works exactly like for any [Lake package](https://reservoir.lean-lang.org/),

lakefile.toml

@@ -28,5 +28,12 @@ root = "Main"
 # Remove this line if you do not need such functionality.
 supportInterpreter = true
 
+# `lake exe unused_transitive_imports` prints unused transitive imports from amongst a given list of modules.
+[[lean_exe]]
+name = "unused_transitive_imports"
+root = "ImportGraph.UnusedTransitiveImports"
+supportInterpreter = true
+
 [[lean_lib]]
 name = "ImportGraphTest"
+