handle Init and Std

ImportGraph/Cli.lean

@@ -41,9 +41,13 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
       graph := graph.downstreamOf (NameSet.empty.insert f)
     let toModule := ImportGraph.getModule to
     let includeLean := args.hasFlag "include-lean"
+    let includeStd := args.hasFlag "include-std"
     let includeDeps := args.hasFlag "include-deps"
     let filter (n : Name) : Bool :=
-      toModule.isPrefixOf n || bif (isPrefixOf `Lean n) then includeLean else includeDeps
+      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

Main.lean

@@ -21,7 +21,8 @@ def graph : Cmd := `[Cli|
     "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-lean";       "Include used files from Lean"
+    "include-std";        "Include used files from the Lean standard library"
+    "include-lean";       "Include used files from Lean itself (`Lean.*` and `Init.*`)"
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \