From 0bf1cdc5607378ee4ac8fc9511d405bf70023f28 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 13 Feb 2024 10:13:50 +0100 Subject: [PATCH] fix exclude-meta --- ImportGraph/Cli.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index 7249279..1b0bef5 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.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