tweaks

ImportGraph/Cli.lean

@@ -117,7 +117,11 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
       let dotFile := asDotGraph graph (unused := unused) (markedModule := markedModule)
       outFiles := outFiles.insert "dot" dotFile
     if extensions.contains "gexf" then
-      let (out, _) ← CoreM.toIO (Graph.toGexf graph p) ctx state
+      -- filter out the top node as it makes the graph less pretty
+      let graph₂ := match args.flag? "to" with
+        | none => graph.filter (fun n _ => n != to)
+        | some _ => graph
+      let (out, _) ← CoreM.toIO (Graph.toGexf graph₂ p) ctx state
       outFiles := outFiles.insert "gexf" out
     return outFiles
 

README.md

@@ -24,6 +24,10 @@ lake exe graph --to MyModule my_graph.pdf
 ```
 where `MyModule` follows the same module naming you would use to `import` it in lean. See `lake exe graph --help` for more options.
 
+### Troubleshoot
+
+* make sure to `lake build` your project (or the specified `--to` module) before using `lake exe graph`!
+
 ### Json
 
 To create a Json file, you can use `.xdot_json` or `.json` as output type:
@@ -40,6 +44,16 @@ lake exe graph my_graph.html
 
 creates a stand-alone HTML file visualising the import structure.
 
+## Commands
+
+There are a few commands implemented, which help you analysing the imports of a file. These are accessible by adding `import ImportGraph.Imports` to your lean file.
+
+* `#redundant_imports`: lists any transitively redundant imports in the current module.
+* `#min_imports`: attempts to construct a minimal set of imports for the declarations
+  in the current file.
+  (Must be run at the end of the file. Tactics and macros may result in incorrect output.)
+* `#find_home decl`: suggests files higher up the import hierarchy to which `decl` could be moved.
+
 ## Installation
 
 The installation works exactly like for any [Lake package](https://reservoir.lean-lang.org/).
@@ -63,16 +77,6 @@ rev = "main"
 
 Then, you might need to call `lake update -R importGraph` in your project.
 
-## Commands
-
-There are a few commands implemented, which help you analysing the imports of a file. These are accessible by adding `import ImportGraph.Imports` to your lean file.
-
-* `#redundant_imports`: lists any transitively redundant imports in the current module.
-* `#min_imports`: attempts to construct a minimal set of imports for the declarations
-  in the current file.
-  (Must be run at the end of the file. Tactics and macros may result in incorrect output.)
-* `#find_home decl`: suggests files higher up the import hierarchy to which `decl` could be moved.
-
 ## Contribution
 
 Please open PRs/Issues if you have troubles or would like to contribute new features!