feat: replace --reduce with --show-transitive, changing the default b…

…ehaviour (#26)
leanprover-community · Aug 29, 2024 · fe36a37 · fe36a37
1 parent 4a6405e
commit fe36a37
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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]`."