feat: incorporate Eric's 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
 
@@ -60,21 +61,34 @@ 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 : Array String := match args.variableArgsAs! String with
+    | #[] => #["dot"]
+    | outputs => outputs.foldl (fun acc (o : String) =>
+      match FilePath.extension o with
+       | none => if acc.contains "dot" then acc else acc.push "dot"
+       | some "gexf" => if acc.contains "gexf" then acc else acc.push "gexf"
+       | some "html" => if acc.contains "gexf" then acc else acc.push "gexf"
+       -- currently all other formats are handled by passing the `.dot` file to
+       -- graphviz
+       | some _ => if acc.contains "dot" then acc else acc.push "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 ctx := { options := {}, fileName := "<input>", fileMap := default }
+    let state := { env }
     let mut graph := env.importGraph
     let unused ←
       match args.flag? "to"  with
       | some _ =>
-        let ctx := { options := {}, fileName := "<input>", fileMap := default }
-        let state := { env }
         let used ← Prod.fst <$> (CoreM.toIO (env.transitivelyRequiredModules to) ctx state)
         pure <| graph.fold (fun acc n _ => if used.contains n then acc else acc.insert n) NameSet.empty
       | none => pure NameSet.empty
@@ -112,22 +126,49 @@ 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 : 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
+      let (out, _) ← CoreM.toIO (Graph.toGexf graph p) ctx state
+      outFiles := outFiles.insert "gexf" out
+    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.find! "dot")
   | outputs => for o in outputs do
      let fp : FilePath := o
      match fp.extension with
      | none
-     | "dot" => writeFile fp dotFile
+     | "dot" => writeFile fp (outFiles.find! "dot")
+     | "gexf" => IO.FS.writeFile fp (outFiles.find! "gexf")
+     | "html" =>
+        -- use `html-template/index.html` and insert any dependencies to make it
+        -- a stand-alone HTML file.
+        let gexFile := (outFiles.find! "gexf")
+        let mut html ← IO.FS.readFile "html-template/index.html"
+        for dep in #[
+            "vendor/sigma.min.js",
+            "vendor/graphology.min.js",
+            "vendor/graphology-library.min.js" ] do
+          let depContent ← IO.FS.readFile ("html-template" / dep)
+          html := html.replace s!"<script src=\"{dep}\"></script>"
+            s!"<script>{depContent}</script>"
+        html := html.replace "fetch(\"imports.gexf\").then((res) => res.text()).then(render_gexf)"
+          s!"render_gexf(\"{gexFile.replace "\n" ""|>.replace "\"" "\\\""}\")"
+          |>.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.find! "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,77 @@
+/-
+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 {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
+  if declName == ``sorryAx then return true
+  if declName matches .str _ "inj" then return true
+  if declName matches .str _ "noConfusionType" then return true
+  let env ← getEnv
+  pure <| declName.isInternalDetail
+   || isAuxRecursor env declName
+   || isNoConfusion env declName
+  <||> isRec declName <||> isMatcher declName
+
+/-- Get all declarations in the specified file. -/
+def getNumberOfDeclsInFile (module : Name) : CoreM (NameSet) := do
+  let env ← getEnv
+  match env.moduleIdxForModule? module with
+    | none => return {}
+    | some modIdx =>
+      let decls := env.const2ModIdx
+      let declsIn ← decls.foldM (fun acc n idx => do
+        if idx == modIdx && (! (← isBlackListed n)) then return acc.insert n else return acc) ({} : NameSet)
+      return declsIn
+
+/-- 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) : CoreM String := do
+  let sizes : NameMap Nat ← graph.foldM (fun acc n _ => do
+    pure <| acc.insert n (← getNumberOfDeclsInFile n).size ) {}
+    -- graph.fold (fun acc _ i => i.foldl (fun acc₂ j => acc₂.insert j ((acc₂.findD j 0) + 1)) acc) {}
+
+  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) "")) ""
+  return 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

@@ -29,7 +29,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

@@ -26,12 +26,20 @@ where `MyModule` follows the same module naming you would use to `import` it in
 
 ### Json
 
-To create a Json file, you can use `.xdot_json` as output type:
+To create a Json file, you can use `.xdot_json` or `.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.
+
 ## Installation
 
 The installation works exactly like for any [Lake package](https://reservoir.lean-lang.org/).
@@ -65,10 +73,18 @@ There are a few commands implemented, which help you analysing the imports of a
   (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!
+
 ## 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/LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2021 Eric Wieser
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

html-template/README.md

@@ -0,0 +1,25 @@
+# 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.
+
+Adaptation by Jon Eugster.