diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 605bc7c..86d844c 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -51,7 +51,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do isPrefixOf `Mathlib.Mathport n ∨ isPrefixOf `Mathlib.Util n) graph := graph.filterGraph filterMathlibMeta (replacement := `«Mathlib.Tactics») - if args.hasFlag "reduce" then + if !args.hasFlag "show-transitive" then graph := graph.transitiveReduction return asDotGraph graph catch err => diff --git a/Main.lean b/Main.lean index 0de6f03..d1e579e 100644 --- a/Main.lean +++ b/Main.lean @@ -16,7 +16,7 @@ def graph : Cmd := `[Cli| If you are working in a downstream project, use `lake exe graph --to MyProject`." FLAGS: - reduce; "Remove transitively redundant edges." + "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]`."