fix exclude-meta

leanprover-community · Feb 13, 2024 · 0bf1cdc · 0bf1cdc
1 parent 9618fa9
commit 0bf1cdc
Showing 1 changed file with 7 additions and 6 deletions.
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
@@ -45,12 +45,13 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
       graph := graph.filterMap (fun n i =>
         if p.isPrefixOf n then (i.filter (isPrefixOf p)) else none)
     if args.hasFlag "exclude-meta" then
-      let filterMeta : Name → Bool := fun n => (
-        isPrefixOf `Graph.Lean.Tactic n ∨
-        isPrefixOf `Graph.Lean n ∨
-        isPrefixOf `Graph.Lean.Mathport n ∨
-        isPrefixOf `Graph.Lean.Util n)
-      graph := graph.filterGraph filterMeta (replacement := `«Graph.Lean.Tactics»)
+      -- Mathlib-specific exclusion of tactics
+      let filterMathlibMeta : Name → Bool := fun n => (
+        isPrefixOf `Mathlib.Lean.Tactic n ∨
+        isPrefixOf `Mathlib.Lean n ∨
+        isPrefixOf `Mathlib.Lean.Mathport n ∨
+        isPrefixOf `Mathlib.Lean.Util n)
+      graph := graph.filterGraph filterMathlibMeta (replacement := `«Mathlib.Lean.Tactics»)
     if args.hasFlag "reduce" then
       graph := graph.transitiveReduction
     return asDotGraph graph