From 8128754f13e2955b1098c15822c72d581c51a057 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 30 Aug 2024 18:36:32 +0200 Subject: [PATCH 1/9] feat: add directly imported deps to --mark-module --- ImportGraph/Cli.lean | 25 ++++++++++++++++++++----- Main.lean | 2 +- 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index abc5963..6fcf231 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -18,17 +18,23 @@ 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. * Nodes which start with the `markedModule` and edges into them will be 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) : + (markedModule : Option Name := none) + (directDeps : NameSet := {}) : String := Id.run do let mut lines := #[s!"digraph \"{header}\" " ++ "{"] for (n, is) in graph do - if unused.contains n then + if 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 -- mark node @@ -77,9 +83,18 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let toModule := ImportGraph.getModule to let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean - let includeDeps := args.hasFlag "include-deps" || args.hasFlag "mark-module" || includeStd + let includeDeps := args.hasFlag "include-deps" || includeStd + + -- `directDeps` are excempt from being filtered out. + let directDeps := if args.hasFlag "mark-module" then + graph.fold (fun acc n deps => if toModule.isPrefixOf n then + -- append all dependencies of `n` which are not in the module + deps.filter (!toModule.isPrefixOf ·) |>.foldl NameSet.insert acc + else acc) NameSet.empty + else NameSet.empty + let filter (n : Name) : Bool := - toModule.isPrefixOf n || + toModule.isPrefixOf n || directDeps.contains n || bif isPrefixOf `Std n then includeStd else bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else includeDeps @@ -97,7 +112,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let markedModule : Option Name := if args.hasFlag "mark-module" then p else none - return asDotGraph graph (unused := unused) (markedModule := markedModule) + return asDotGraph graph (unused := unused) (markedModule := markedModule) (directDeps := directDeps) 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`, " ++ diff --git a/Main.lean b/Main.lean index 7e65269..c84f5d6 100644 --- a/Main.lean +++ b/Main.lean @@ -21,7 +21,7 @@ def graph : Cmd := `[Cli| "from" : ModuleName; "Only show the downstream dependencies of the specified module." "exclude-meta"; "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`." "include-deps"; "Include used files from other libraries (not including Lean itself and `std`)" - "mark-module"; "Visually highlight the current module. (implies `--include-deps`)" + "mark-module"; "Include directly imported files from other libraries and visually highlight the current module" "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`)" From 581e55d0170982b973b3c9d5d4ad22152d6e5c5c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 08:34:54 +0200 Subject: [PATCH 2/9] Update ImportGraph/Cli.lean Co-authored-by: Kim Morrison --- ImportGraph/Cli.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 6fcf231..c1cac5b 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -85,7 +85,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd - -- `directDeps` are excempt from being filtered out. + -- `directDeps` are exempt from being filtered out. let directDeps := if args.hasFlag "mark-module" then graph.fold (fun acc n deps => if toModule.isPrefixOf n then -- append all dependencies of `n` which are not in the module From 9eccd341f0dd07265437ad2f4a656159370c5197 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 11:13:26 +0200 Subject: [PATCH 3/9] split into --include-direct-deps and --mark-module --- ImportGraph/Cli.lean | 16 ++++++++++------ Main.lean | 19 ++++++++++--------- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index c1cac5b..ed051f5 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -30,7 +30,7 @@ def asDotGraph let mut lines := #[s!"digraph \"{header}\" " ++ "{"] for (n, is) in graph do - if directDeps.contains n then + if markedModule.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];" @@ -84,21 +84,25 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd + let includeDirectDeps := args.hasFlag "include-direct-deps" || args.hasFlag "mark-module" - -- `directDeps` are exempt from being filtered out. - let directDeps := if args.hasFlag "mark-module" then + -- If the flag is set, `directDeps` contains files which are not in the module + -- but directly imported by a file in the module + let directDeps := if includeDirectDeps then graph.fold (fun acc n deps => if toModule.isPrefixOf n then - -- append all dependencies of `n` which are not in the module deps.filter (!toModule.isPrefixOf ·) |>.foldl NameSet.insert acc else acc) NameSet.empty else NameSet.empty let filter (n : Name) : Bool := - toModule.isPrefixOf n || directDeps.contains n || + toModule.isPrefixOf n || bif isPrefixOf `Std n then includeStd else bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else includeDeps - graph := graph.filterMap (fun n i => if filter n then (i.filter filter) else none) + graph := graph.filterMap (fun n i => if filter n then + (i.filter (fun m => directDeps.contains m || filter m)) else + -- include direct dep but without any further deps + if directDeps.contains n then some #[] else none) if args.hasFlag "exclude-meta" then -- Mathlib-specific exclusion of tactics let filterMathlibMeta : Name → Bool := fun n => ( diff --git a/Main.lean b/Main.lean index c84f5d6..b314193 100644 --- a/Main.lean +++ b/Main.lean @@ -10,20 +10,21 @@ open Cli /-- Setting up command line options and help text for `lake exe graph`. -/ def graph : Cmd := `[Cli| - graph VIA importGraphCLI; ["0.0.2"] + graph VIA importGraphCLI; ["0.0.3"] "Generate representations of a Lean import graph. \ By default generates the import graph up to `Mathlib`. \ 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-deps"; "Include used files from other libraries (not including Lean itself and `std`)" - "mark-module"; "Include directly imported files from other libraries and visually highlight the current module" - "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`)" + "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-deps"; "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 (implies `--include-direct-deps`)" ARGS: ...outputs : String; "Filename(s) for the output. \ From b87256b0e1950b2da3ceef0817c0f79874c3e561 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 11:35:09 +0200 Subject: [PATCH 4/9] update logic --- ImportGraph/Cli.lean | 15 +++++++-------- Main.lean | 2 +- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index ed051f5..6a47129 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -84,25 +84,24 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd - let includeDirectDeps := args.hasFlag "include-direct-deps" || args.hasFlag "mark-module" + let includeDirectDeps := args.hasFlag "include-direct-deps" -- If the flag is set, `directDeps` contains files which are not in the module -- but directly imported by a file in the module - let directDeps := if includeDirectDeps then - graph.fold (fun acc n deps => if toModule.isPrefixOf n then - deps.filter (!toModule.isPrefixOf ·) |>.foldl NameSet.insert acc - else acc) NameSet.empty - else NameSet.empty + let directDeps := graph.fold (fun acc n deps => if toModule.isPrefixOf n then + deps.filter (!toModule.isPrefixOf ·) |>.foldl NameSet.insert acc + else acc) NameSet.empty let filter (n : Name) : Bool := toModule.isPrefixOf n || bif isPrefixOf `Std n then includeStd else bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else includeDeps + let filterDirect (n : Name) : Bool := includeDirectDeps ∧ directDeps.contains n graph := graph.filterMap (fun n i => if filter n then - (i.filter (fun m => directDeps.contains m || filter m)) else + (i.filter (fun m => filterDirect m || filter m)) else -- include direct dep but without any further deps - if directDeps.contains n then some #[] else none) + if filterDirect n then some #[] else none) if args.hasFlag "exclude-meta" then -- Mathlib-specific exclusion of tactics let filterMathlibMeta : Name → Bool := fun n => ( diff --git a/Main.lean b/Main.lean index b314193..78fccc2 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-module"; "Visually highlight the current module (implies `--include-direct-deps`)" + "mark-module"; "Visually highlight the current module (used in combination with some `--include-XXX`)." ARGS: ...outputs : String; "Filename(s) for the output. \ From f57a9186f63460e2b4063692dcdfe262d320d841 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 11:39:49 +0200 Subject: [PATCH 5/9] add comment --- ImportGraph/Cli.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 6a47129..802822d 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -84,6 +84,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd + -- `includeDirectDeps` does not imply `includeDeps`, e.g. `import Lean`. let includeDirectDeps := args.hasFlag "include-direct-deps" -- If the flag is set, `directDeps` contains files which are not in the module From e1b5b6df203c32d3bb6bd6b6926f5b9fb8f660e8 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 11:44:16 +0200 Subject: [PATCH 6/9] rename option --- ImportGraph/Cli.lean | 6 +++--- Main.lean | 18 +++++++++--------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 802822d..a17b7d6 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -84,8 +84,8 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd - -- `includeDirectDeps` does not imply `includeDeps`, e.g. `import Lean`. - let includeDirectDeps := args.hasFlag "include-direct-deps" + -- `includeDirect` does not imply `includeDeps`, e.g. `import Lean`. + let includeDirect := args.hasFlag "include-direct" -- If the flag is set, `directDeps` contains files which are not in the module -- but directly imported by a file in the module @@ -98,7 +98,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do bif isPrefixOf `Std n then includeStd else bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else includeDeps - let filterDirect (n : Name) : Bool := includeDirectDeps ∧ directDeps.contains n + let filterDirect (n : Name) : Bool := includeDirect ∧ directDeps.contains n graph := graph.filterMap (fun n i => if filter n then (i.filter (fun m => filterDirect m || filter m)) else -- include direct dep but without any further deps diff --git a/Main.lean b/Main.lean index 78fccc2..2104d4f 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-deps"; "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 : 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`)." ARGS: ...outputs : String; "Filename(s) for the output. \ From d153077400299a53b494a569b46182f92df1fbcd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 14:56:08 +0200 Subject: [PATCH 7/9] style --- ImportGraph/Cli.lean | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index a17b7d6..40921a2 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -87,22 +87,32 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do -- `includeDirect` does not imply `includeDeps`, e.g. `import Lean`. let includeDirect := args.hasFlag "include-direct" - -- If the flag is set, `directDeps` contains files which are not in the module + -- `directDeps` contains files which are not in the module -- but directly imported by a file in the module - let directDeps := graph.fold (fun acc n deps => if toModule.isPrefixOf n then - deps.filter (!toModule.isPrefixOf ·) |>.foldl NameSet.insert acc - else acc) NameSet.empty + 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 + else + acc) let filter (n : Name) : Bool := toModule.isPrefixOf n || bif isPrefixOf `Std n then includeStd else bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else includeDeps - let filterDirect (n : Name) : Bool := includeDirect ∧ directDeps.contains n - graph := graph.filterMap (fun n i => if filter n then - (i.filter (fun m => filterDirect m || filter m)) else - -- include direct dep but without any further deps - if filterDirect n then some #[] else none) + let filterDirect (n : Name) : Bool := + includeDirect ∧ directDeps.contains n + + graph := graph.filterMap (fun n i => + if filter n then + -- include node regularly + (i.filter (fun m => filterDirect m || filter m)) + else if filterDirect n then + -- include node as direct dependency; drop any further deps. + some #[] + else + -- not included + none) if args.hasFlag "exclude-meta" then -- Mathlib-specific exclusion of tactics let filterMathlibMeta : Name → Bool := fun n => ( From 14a84664583048445c098122c871cc4ef261db42 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 14:58:10 +0200 Subject: [PATCH 8/9] style --- ImportGraph/Cli.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 40921a2..bbbbf86 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -17,8 +17,10 @@ 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. -* Nodes which start with the `markedModule` and edges into them will be highlighted in green. -* Nodes in `directDeps` are marked with a green border and green text. +* If `markedModule` is provided: + * Nodes which start with the `markedModule` 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)) From 16fcfe0fb83114810b1067579d4f8d69a2ddb1f6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 15:01:21 +0200 Subject: [PATCH 9/9] style --- ImportGraph/Cli.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index bbbbf86..b4ab70d 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -86,7 +86,9 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do let includeLean := args.hasFlag "include-lean" let includeStd := args.hasFlag "include-std" || includeLean let includeDeps := args.hasFlag "include-deps" || includeStd - -- `includeDirect` does not imply `includeDeps`, e.g. `import Lean`. + -- Note: `includeDirect` does not imply `includeDeps`! + -- e.g. if the module 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