feat: add --include-lean option

ImportGraph/Cli.lean

@@ -39,10 +39,12 @@ 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 includeDeps := args.hasFlag "include-deps"
+    let filter (n : Name) : Bool :=
+      toModule.isPrefixOf n || bif (isPrefixOf `Lean 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

@@ -21,6 +21,7 @@ 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"
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \