From 64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 13 Feb 2024 10:27:11 +0100
Subject: [PATCH] fix: correct mathlib names in "exclude-meta" (#1)

---
 ImportGraph/Cli.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
index 7249279..1865a82 100644
--- 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.Tactic n ∨
+        isPrefixOf `Mathlib.Lean n ∨
+        isPrefixOf `Mathlib.Mathport n ∨
+        isPrefixOf `Mathlib.Util n)
+      graph := graph.filterGraph filterMathlibMeta (replacement := `«Mathlib.Tactics»)
     if args.hasFlag "reduce" then
       graph := graph.transitiveReduction
     return asDotGraph graph