Merge pull request #30 from leanprover-community/eugster/html-visuali…

…sation

feat: add HTML visualisation

ImportGraph/Cli.lean

@@ -8,6 +8,7 @@ import Batteries.Lean.IO.Process
 import ImportGraph.CurrentModule
 import ImportGraph.Imports
 import ImportGraph.Lean.Name
+import ImportGraph.Gexf
 
 open Cli
 
@@ -62,14 +63,27 @@ open Lean Core System
 open IO.FS IO.Process Name in
 /-- Implementation of the import graph command line program. -/
 def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
+  -- file extensions that should be created
+  let extensions : Std.HashSet String := match args.variableArgsAs! String with
+    | #[] => Std.HashSet.empty.insert "dot"
+    | outputs => outputs.foldl (fun acc (o : String) =>
+      match FilePath.extension o with
+       | none => acc.insert "dot"
+       | some "gexf" => acc.insert "gexf"
+       | some "html" => acc.insert "gexf"
+       -- currently all other formats are handled by passing the `.dot` file to
+       -- graphviz
+       | some _ => acc.insert "dot" ) {}
+
   let to ← match args.flag? "to" with
   | some to => pure <| to.as! ModuleName
   | none => getCurrentModule
   let from? := match args.flag? "from" with
   | some fr => some <| fr.as! ModuleName
   | none => none
   searchPathRef.set compile_time_search_path%
-  let dotFile ← try unsafe withImportModules #[{module := to}] {} (trustLevel := 1024) fun env => do
+
+  let outFiles ← try unsafe withImportModules #[{module := to}] {} (trustLevel := 1024) fun env => do
     let p := ImportGraph.getModule to
     let mut graph := env.importGraph
     let unused ←
@@ -130,22 +144,56 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
 
     let markedModule : Option Name := if args.hasFlag "mark-module" then p else none
 
-    return asDotGraph graph (unused := unused) (markedModule := markedModule) (directDeps := directDeps)
+    -- Create all output files that are requested
+    let mut outFiles : Std.HashMap String String := {}
+    if extensions.contains "dot" then
+      let dotFile := asDotGraph graph (unused := unused) (markedModule := markedModule) (directDeps := directDeps)
+      outFiles := outFiles.insert "dot" dotFile
+    if extensions.contains "gexf" then
+      -- 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 gexfFile := Graph.toGexf graph₂ p env
+      outFiles := outFiles.insert "gexf" gexfFile
+    return outFiles
+
   catch err =>
     -- TODO: try to build `to` first, so this doesn't happen
     throw <| IO.userError <| s!"{err}\nIf the error above says `unknown package`, " ++
       s!"try if `lake build {to}` fixes the issue"
     throw err
 
   match args.variableArgsAs! String with
-  | #[] => writeFile "import_graph.dot" dotFile
+  | #[] => writeFile "import_graph.dot" (outFiles["dot"]!)
   | outputs => for o in outputs do
      let fp : FilePath := o
      match fp.extension with
      | none
-     | "dot" => writeFile fp dotFile
+     | "dot" => writeFile fp (outFiles["dot"]!)
+     | "gexf" => IO.FS.writeFile fp (outFiles["gexf"]!)
+     | "html" =>
+        let gexfFile := (outFiles["gexf"]!)
+        -- use `html-template/index.html` and insert any dependencies to make it
+        -- a stand-alone HTML file.
+        -- note: changes in `index.html` might need to be reflected here!
+        let exeDir := (FilePath.parent (← IO.appPath) |>.get!) / ".." / ".." / ".."
+        let mut html ← IO.FS.readFile <| ← IO.FS.realPath ( exeDir / "html-template" / "index.html")
+        for dep in (#[
+            "vendor" / "sigma.min.js",
+            "vendor" / "graphology.min.js",
+            "vendor" / "graphology-library.min.js" ] : Array FilePath) do
+          let depContent ← IO.FS.readFile <| ← IO.FS.realPath (exeDir / "html-template" / dep)
+          html := html.replace s!"<script src=\"{dep}\"></script>" s!"<script>{depContent}</script>"
+        -- inline the graph data
+        -- note: changes in `index.html` might need to be reflected here!
+        let escapedFile := gexfFile.replace "\n" "" |>.replace "\"" "\\\""
+        html := html
+          |>.replace "fetch(\"imports.gexf\").then((res) => res.text()).then(render_gexf)" s!"render_gexf(\"{escapedFile}\")"
+          |>.replace "<h1>Import Graph</h1>" s!"<h1>Import Graph for {to}</h1>"
+        IO.FS.writeFile fp html
      | some ext => try
-        _ ← runCmdWithInput "dot" #["-T" ++ ext, "-o", o] dotFile
+        _ ← runCmdWithInput "dot" #["-T" ++ ext, "-o", o] (outFiles["dot"]!)
       catch ex =>
         IO.eprintln s!"Error occurred while writing out {fp}."
         IO.eprintln s!"Make sure you have `graphviz` installed and the file is writable."

ImportGraph/Gexf.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2024 Jon Eugster. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Eugster
+-/
+
+import Lean
+import Batteries.Lean.NameMap
+import Batteries.Tactic.OpenPrivate
+
+open Lean
+
+namespace ImportGraph
+
+open Elab Meta in
+/-- Filter Lean internal declarations -/
+def isBlackListed (env : Environment) (declName : Name) : Bool :=
+  declName == ``sorryAx
+  || declName matches .str _ "inj"
+  || declName matches .str _ "noConfusionType"
+  || declName.isInternalDetail
+  || isAuxRecursor env declName
+  || isNoConfusion env declName
+  || isRecCore env declName
+  || isMatcherCore env declName
+
+/-- Get number of non-blacklisted declarations per file. -/
+def getNumberOfDeclsPerFile (env: Environment) : NameMap Nat :=
+  env.const2ModIdx.fold (fun acc n (idx : ModuleIdx) =>
+    let mod := env.allImportedModuleNames.get! idx
+    if isBlackListed env n then acc else acc.insert mod ((acc.findD mod 0) + 1)
+    ) {}
+
+/-- Gexf template for a node in th graph. -/
+def Gexf.nodeTemplate (n module : Name) (size : Nat) := s!"<node id=\"{n}\" label=\"{n}\"><attvalues><attvalue for=\"0\" value=\"{size}\" /><attvalue for=\"1\" value=\"{module.isPrefixOf n}\" /></attvalues></node>\n          "
+
+/-- Gexf template for an edge in the graph -/
+def Gexf.edgeTemplate (source target : Name) := s!"<edge source=\"{source}\" target=\"{target}\" id=\"{source}--{target}\" />\n          "
+
+open Gexf in
+/-- Creates a `.gexf` file of the graph, see https://gexf.net/
+
+Metadata can be stored in forms of attributes, currently we record the following:
+* `decl_count` (Nat): number of declarations in the file
+* `in_module` (Bool): whether the file belongs to the main module
+  (used to strip the first part of the name when displaying).
+-/
+def Graph.toGexf (graph : NameMap (Array Name)) (module : Name) (env : Environment) : String :=
+  let sizes : NameMap Nat := getNumberOfDeclsPerFile env
+  let nodes : String := graph.fold (fun acc n _ => acc ++ nodeTemplate n module (sizes.findD n 0)) ""
+  let edges : String := graph.fold (fun acc n i => acc ++ (i.foldl (fun b j => b ++ edgeTemplate j n) "")) ""
+  s!"<?xml version='1.0' encoding='utf-8'?>
+    <gexf xmlns=\"http://www.gexf.net/1.2draft\" xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\" xsi:schemaLocation=\"http://www.gexf.net/1.2draft http://www.gexf.net/1.2draft/gexf.xsd\" version=\"1.2\">
+      <meta>
+        <creator>Lean ImportGraph</creator>
+      </meta>
+      <graph defaultedgetype=\"directed\" mode=\"static\" name=\"\">
+        <attributes mode=\"static\" class=\"node\">
+          <attribute id=\"0\" title=\"decl_count\" type=\"long\" />
+          <attribute id=\"1\" title=\"in_module\" type=\"boolean\" />
+        </attributes>
+        <nodes>
+          {nodes.trim}
+        </nodes>
+        <edges>
+          {edges.trim}
+        </edges>
+      </graph>
+    </gexf>
+    "

Main.lean

@@ -30,7 +30,7 @@ def graph : Cmd := `[Cli|
     ...outputs : String;  "Filename(s) for the output. \
       If none are specified, generates `import_graph.dot`. \
       Automatically chooses the format based on the file extension. \
-      Currently `.dot` is supported, \
+      Currently supported formats are `.dot`, `.gexf`, `.html`, \
       and if you have `graphviz` installed then any supported output format is allowed."
 ]
 

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` as output type:
@@ -32,6 +36,24 @@ To create a Json file, you can use `.xdot_json` as output type:
 lake exe graph my_graph.xdot_json
 ```
 
+### HTML
+
+```
+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/).
@@ -55,20 +77,18 @@ rev = "main"
 
 Then, you might need to call `lake update -R importGraph` in your project.
 
-## Commands
+## Contribution
 
-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.
+Please open PRs/Issues if you have troubles or would like to contribute new features!
 
 ## Credits
 
-This code has been extracted from [mathlib](https://github.com/leanprover-community/mathlib4) and has mainly been written by Kim Morrison and a few other mathlib contributors.
+The main tool has been extracted from [mathlib](https://github.com/leanprover-community/mathlib4),
+originally written by Kim Morrison and other mathlib contributors.
+
+The HTML visualisation has been incorporated from
+[a project by Eric Wieser](https://github.com/eric-wieser/mathlib-import-graph).
 
 ### Maintainers
 
-For issues, questions, or feature requests, please reach out to [Jon Eugster](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster).
+Primarily maintained by [Jon Eugster](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster), Kim Morrison, and the wider leanprover community.

html-template/.gitignore

@@ -0,0 +1 @@
+imports.gexf

html-template/README.md

@@ -0,0 +1,26 @@
+# Visualised import graph
+
+## Instructions
+
+To test this, place a file `imports.gexf` inside this directory. You can create such a file with
+
+```
+lake exe graph html-template/imports.gexf
+```
+
+Then open `index.html` in any browser and you should see the graph.
+
+## Development
+
+Currently `lake exe graph output.html` will use the files here to create a stand-alone
+HTML file. It does so by search-replacing the JS-scripts, the `fetch('imports.gexf')`
+statement, and the `<h1>` header.
+
+Therefore any modifications to these lines need to be reflected in `ImportGraph/Cli.lean`!
+
+# Credits
+
+This tool has been adapted from it's [Lean 3 version](https://github.com/eric-wieser/mathlib-import-graph) written by Eric Wieser, which was published under the [MIT License](./LICENSE_source)
+included here.
+
+Adaptation by Jon Eugster.