From 72802f11c14bb72fd06a6e93bc2e3ef8e21424e0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Oct 2024 21:56:37 +1100 Subject: [PATCH 01/15] faster? --- ImportGraph/Imports.lean | 6 ++---- ImportGraph/RequiredModules.lean | 26 ++++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean index 8025b60..d061ebd 100644 --- a/ImportGraph/Imports.lean +++ b/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 let env ← getEnv let transitiveImports := env.importGraph.transitiveClosure + let transitivelyRequired ← env.transitivelyRequiredModules' amongst 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)) /-- diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 7ca2fd5..89c4922 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -115,6 +115,32 @@ 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) : + CoreM (NameMap NameSet) := do + let mut c2m : NameMap NameSet := {} + let mut result : NameMap NameSet := {} + for m in modules do + let mut r : NameSet := {} + for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do + c2m ← process c2m n + r := r.union ((c2m.find? n).getD {}) + result := result.insert m r + return result +where process (constantsToModules : NameMap NameSet) (const : Name) : CoreM (NameMap NameSet) := do + if constantsToModules.contains const then + return constantsToModules + let mut c2m := constantsToModules + let ci ← getConstInfo const + let mut r : NameSet := {} + for n in ci.getUsedConstantsAsSet do + c2m ← process c2m n + r := r.union ((c2m.find? n).getD {}) + return c2m.insert const r + /-- Return the names of the modules in which constants used in the current file were defined. From 8738783bbd9ab73df0cf4e12549bbbe3b7e4adef Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 00:26:41 +1100 Subject: [PATCH 02/15] stackoverflow --- ImportGraph/RequiredModules.lean | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 89c4922..0443a42 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -126,20 +126,25 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module for m in modules do let mut r : NameSet := {} for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do - c2m ← process c2m n + let mut stack : Array (ConstantInfo × Option NameSet) := #[⟨← getConstInfo n, none⟩] + while !stack.isEmpty do + let (ci, used?) := stack.back + match used? with + | none => + stack := stack.pop + if !c2m.contains ci.name then + let used := ci.getUsedConstantsAsSet + stack := stack.pop.push ⟨ci, some used⟩ + for u in used do + if !c2m.contains u then + stack := stack.push ⟨← getConstInfo u, none⟩ + | some used => + let transitivelyUsed : NameSet := used.fold (init := used) (fun s u => s.union ((c2m.find? u).getD {})) + c2m := c2m.insert ci.name transitivelyUsed + stack := stack.pop r := r.union ((c2m.find? n).getD {}) result := result.insert m r return result -where process (constantsToModules : NameMap NameSet) (const : Name) : CoreM (NameMap NameSet) := do - if constantsToModules.contains const then - return constantsToModules - let mut c2m := constantsToModules - let ci ← getConstInfo const - let mut r : NameSet := {} - for n in ci.getUsedConstantsAsSet do - c2m ← process c2m n - r := r.union ((c2m.find? n).getD {}) - return c2m.insert const r /-- Return the names of the modules in which constants used in the current file were defined. From 0c61e26bf68ab56ec37578ec82f7abb519ee6da9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 00:40:26 +1100 Subject: [PATCH 03/15] . --- ImportGraph/RequiredModules.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 0443a42..294d745 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -126,22 +126,25 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module for m in modules do let mut r : NameSet := {} for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do + -- 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 : Array (ConstantInfo × Option NameSet) := #[⟨← getConstInfo n, none⟩] while !stack.isEmpty do let (ci, used?) := stack.back + stack := stack.pop match used? with | none => - stack := stack.pop if !c2m.contains ci.name then let used := ci.getUsedConstantsAsSet - stack := stack.pop.push ⟨ci, some used⟩ + stack := stack.push ⟨ci, some used⟩ for u in used do if !c2m.contains u then stack := stack.push ⟨← getConstInfo u, none⟩ | some used => let transitivelyUsed : NameSet := used.fold (init := used) (fun s u => s.union ((c2m.find? u).getD {})) c2m := c2m.insert ci.name transitivelyUsed - stack := stack.pop r := r.union ((c2m.find? n).getD {}) result := result.insert m r return result From e61efb3adb638795204358a92e5454c863359b12 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 11:52:35 +1100 Subject: [PATCH 04/15] use BitVec --- ImportGraph/RequiredModules.lean | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 294d745..2eb5dfd 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -121,10 +121,11 @@ Should be equivalent to calling `transitivelyRequiredModules` on each module, bu -/ partial def Environment.transitivelyRequiredModules' (env : Environment) (modules : List Name) : CoreM (NameMap NameSet) := do - let mut c2m : NameMap NameSet := {} + let N := env.header.moduleNames.size + let mut c2m : NameMap (BitVec N) := {} let mut result : NameMap NameSet := {} for m in modules do - let mut r : NameSet := {} + let mut r : BitVec N := 0 for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do -- 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: @@ -143,11 +144,16 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module if !c2m.contains u then stack := stack.push ⟨← getConstInfo u, none⟩ | some used => - let transitivelyUsed : NameSet := used.fold (init := used) (fun s u => s.union ((c2m.find? u).getD {})) + let transitivelyUsed : BitVec N := used.fold (init := toBitVec used) (fun s u => s ||| ((c2m.find? u).getD 0)) c2m := c2m.insert ci.name transitivelyUsed - r := r.union ((c2m.find? n).getD {}) - result := result.insert m r + 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. From b6a8d266e1beddd354e4f02185a80a15ac6763a8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 11:53:08 +1100 Subject: [PATCH 05/15] verbose --- ImportGraph/RequiredModules.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 2eb5dfd..41a21c0 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -119,12 +119,14 @@ def Environment.transitivelyRequiredModules (env : Environment) (module : Name) 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) : +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 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 -- This is messy: Mathlib is big enough that writing a recursive function causes a stack overflow. From d1c7eb7034012a9a7e6d793cc6a0c9e74b83f27b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 11:56:22 +1100 Subject: [PATCH 06/15] verbose --- ImportGraph/Imports.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean index d061ebd..8184999 100644 --- a/ImportGraph/Imports.lean +++ b/ImportGraph/Imports.lean @@ -177,10 +177,10 @@ 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`. -/ -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 + let transitivelyRequired ← env.transitivelyRequiredModules' amongst verbose amongst.mapM fun n => do return (n, let unused := (transitiveImports.find? n).getD {} \ (transitivelyRequired.find? n |>.getD {}) amongst.filter (fun m => unused.contains m)) From 481c60bee93f4a3ce60371a5b2a590de11ba645c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 12:37:27 +1100 Subject: [PATCH 07/15] fix --- ImportGraph/RequiredModules.lean | 37 +++++++++++++++--------- ImportGraph/UnusedTransitiveImports.lean | 23 +++++++++++++++ ImportGraphTest/Imports.lean | 9 ++++++ lakefile.toml | 7 +++++ 4 files changed, 62 insertions(+), 14 deletions(-) create mode 100644 ImportGraph/UnusedTransitiveImports.lean diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 41a21c0..5e90a90 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -123,31 +123,40 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module 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 : Array (ConstantInfo × Option NameSet) := #[⟨← getConstInfo n, none⟩] + let mut stack : List (Name × Option NameSet) := [⟨n, none⟩] + pushed := pushed.insert n while !stack.isEmpty do - let (ci, used?) := stack.back - stack := stack.pop - match used? with - | none => - if !c2m.contains ci.name then - let used := ci.getUsedConstantsAsSet - stack := stack.push ⟨ci, some used⟩ - for u in used do - if !c2m.contains u then - stack := stack.push ⟨← getConstInfo u, none⟩ - | some used => - let transitivelyUsed : BitVec N := used.fold (init := toBitVec used) (fun s u => s ||| ((c2m.find? u).getD 0)) - c2m := c2m.insert ci.name transitivelyUsed + 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 diff --git a/ImportGraph/UnusedTransitiveImports.lean b/ImportGraph/UnusedTransitiveImports.lean new file mode 100644 index 0000000..4743757 --- /dev/null +++ b/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 := "", 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 diff --git a/ImportGraphTest/Imports.lean b/ImportGraphTest/Imports.lean index c2e1047..0abc260 100644 --- a/ImportGraphTest/Imports.lean +++ b/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: diff --git a/lakefile.toml b/lakefile.toml index 5d47ad9..f613939 100644 --- a/lakefile.toml +++ b/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" + From 793740f63564dfc84ff6beca7e7c83c4d2bafbf5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 14:37:59 +1100 Subject: [PATCH 08/15] readme --- README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/README.md b/README.md index 397a134..a931d52 100644 --- a/README.md +++ b/README.md @@ -54,6 +54,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/), From 6e19e75626a0071c7d1499c2200a03d6fc20f074 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 15:25:16 +1100 Subject: [PATCH 09/15] feat: allow multiple --to and --from arguments --- ImportGraph/Cli.lean | 50 ++++++++++++++++++++++---------------------- Main.lean | 18 ++++++++-------- 2 files changed, 34 insertions(+), 34 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index f181ece..be87575 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -18,8 +18,8 @@ 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. -/ @@ -27,27 +27,27 @@ def asDotGraph (graph : NameMap (Array Name)) (unused : NameSet := {}) (header := "import_graph") - (markedModule : Option Name := none) + (markedPackage : Option Name := none) (directDeps : NameSet := {}) : String := Id.run do let mut lines := #[s!"digraph \"{header}\" " ++ "{"] for (n, is) in graph do - if markedModule.isSome ∧ directDeps.contains n then + 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];" else if unused.contains n then lines := lines.push s!" \"{n}\" [style=filled, fillcolor=\"#e0e0e0\"];" - else if isInModule markedModule n then + else if isInModule markedPackage n then -- mark node lines := lines.push s!" \"{n}\" [style=filled, fillcolor=\"#96ec5b\"];" else lines := lines.push s!" \"{n}\";" -- 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 +76,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 := "", 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 +142,26 @@ 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) 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 diff --git a/Main.lean b/Main.lean index 80b5ee6..0ef8c05 100644 --- a/Main.lean +++ b/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 module." + "from" : Array 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-package"; "Visually highlight the current package (used in combination with some `--include-XXX`)." ARGS: ...outputs : String; "Filename(s) for the output. \ From fe586e6d9a26cd53b9f29b54f7f1a3eaaa2dc9cf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 15:32:28 +1100 Subject: [PATCH 10/15] node shapes to indicate --to and --from --- ImportGraph/Cli.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index be87575..89ef5da 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -28,22 +28,24 @@ def asDotGraph (unused : NameSet := {}) (header := "import_graph") (markedPackage : Option Name := none) - (directDeps : NameSet := {}) : + (directDeps : NameSet := {}) + (from_ to : NameSet := {}): String := Id.run do let mut lines := #[s!"digraph \"{header}\" " ++ "{"] for (n, is) in graph do + 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\"];" + 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 markedPackage n then @@ -148,6 +150,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let mut outFiles : Std.HashMap String String := {} if extensions.contains "dot" then 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 From fa418ca2a7073e6ec19ee6733a42652a8e8baa1c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 15:33:29 +1100 Subject: [PATCH 11/15] README --- ImportGraph.lean | 1 + README.md | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/ImportGraph.lean b/ImportGraph.lean index 183f1ac..a58f13b 100644 --- a/ImportGraph.lean +++ b/ImportGraph.lean @@ -3,3 +3,4 @@ import ImportGraph.Imports import ImportGraph.CurrentModule import ImportGraph.Lean.Name import ImportGraph.RequiredModules +import ImportGraph.UnusedTransitiveImports diff --git a/README.md b/README.md index a931d52..56051c1 100644 --- a/README.md +++ b/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`! From 5c04dea31052f5addc14ca94564b08ab73e52127 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Oct 2024 11:06:13 +1100 Subject: [PATCH 12/15] Apply suggestions from code review Co-authored-by: Jon Eugster --- Main.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Main.lean b/Main.lean index 0ef8c05..f9f0e28 100644 --- a/Main.lean +++ b/Main.lean @@ -17,8 +17,8 @@ def graph : Cmd := `[Cli| FLAGS: "show-transitive"; "Show transitively redundant edges." - "to" : Array ModuleName; "Only show the upstream imports of the specified module." - "from" : Array ModuleName; "Only show the downstream dependencies of the specified module." + "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`)" From e2597e77847c396f6f6b651d95cf122dfda3c679 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Oct 2024 11:08:18 +1100 Subject: [PATCH 13/15] suggestion from review --- Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index f9f0e28..b192ed9 100644 --- a/Main.lean +++ b/Main.lean @@ -24,7 +24,7 @@ def graph : Cmd := `[Cli| "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 current package (used in combination with some `--include-XXX`)." + "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. \ From d2600ef13ecb316774f17de5a8ce29bf27a17610 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Oct 2024 11:09:41 +1100 Subject: [PATCH 14/15] update test --- ImportGraphTest/expected.dot | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ImportGraphTest/expected.dot b/ImportGraphTest/expected.dot index d69678a..51c4e88 100644 --- a/ImportGraphTest/expected.dot +++ b/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"; } \ No newline at end of file From 7db540b8ad13ffb7ddd3a48aaf713e46397a4fc7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 1 Nov 2024 14:20:57 +1100 Subject: [PATCH 15/15] chore: bump toolchain to v4.13.0 --- lake-manifest.json | 4 ++-- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6631554..47cb204 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,11 +15,11 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4", + "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.toml"}], "name": "importGraph", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index b1b73fe..e0676e0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0-rc1 \ No newline at end of file +leanprover/lean4:v4.13.0 \ No newline at end of file