Merge pull request #25 from leanprover-community/include-lean

feat: add --include-lean option

ImportGraph/Cli.lean

@@ -39,10 +39,16 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
     let mut graph := env.importGraph
     if let Option.some f := from? then
       graph := graph.downstreamOf (NameSet.empty.insert f)
-    if ¬(args.hasFlag "include-deps") then
-      let p := ImportGraph.getModule to
-      graph := graph.filterMap (fun n i =>
-        if p.isPrefixOf n then (i.filter (isPrefixOf p)) else none)
+    let toModule := ImportGraph.getModule to
+    let includeLean := args.hasFlag "include-lean"
+    let includeStd := args.hasFlag "include-std" || includeLean
+    let includeDeps := args.hasFlag "include-deps" || includeStd
+    let filter (n : Name) : Bool :=
+      toModule.isPrefixOf n ||
+      bif isPrefixOf `Std n then includeStd else
+      bif isPrefixOf `Lean n || isPrefixOf `Init n then includeLean else
+      includeDeps
+    graph := graph.filterMap (fun n i => if filter n then (i.filter filter) else none)
     if args.hasFlag "exclude-meta" then
       -- Mathlib-specific exclusion of tactics
       let filterMathlibMeta : Name → Bool := fun n => (

Main.lean

@@ -20,7 +20,9 @@ def graph : Cmd := `[Cli|
     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]`."
-    "include-deps";       "Include used files from other projects (e.g. lake packages)"
+    "include-deps";       "Include used files from other libraries (not including Lean itself and `std`)"
+    "include-std";        "Include used files from the Lean standard library (implies 'include-deps')"
+    "include-lean";       "Include used files from Lean itself (implies 'include-deps' and 'include-std')"
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \