diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index b4ab70d..763f8f7 100644 --- a/ImportGraph/Cli.lean +++ b/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,6 +63,18 @@ 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 @@ -69,7 +82,8 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do | 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,7 +144,20 @@ 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`, " ++ @@ -138,14 +165,35 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do 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!"" s!"" + -- 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 "
Built with Sigma.js. + Node sizes indicate the number of declarations in the file.
+ +Hover over a node to show only the files importing it. Hover over a directory name to highlight only the files in that directory
+ +n)){if(c in b&&uF?T=(U-=(L-F)/2)+L:I=(P-=(F-L)/2)+F,O[0]=-1,O[1]=(P+I)/2,O[2]=(U+T)/2,O[3]=Math.max(I-P,T-U),O[4]=-1,O[5]=-1,O[6]=0,O[7]=0,O[8]=0,i=1,a=0;a
a[1]&&(a[1]=x.zIndex))}for(var y in w){if(!this.edgePrograms.hasOwnProperty(y))throw new Error('Sigma: could not find a suitable program for edge type "'+y+'"!');t||this.edgePrograms[y].allocate(w[y]),w[y]=0}for(this.settings.zIndex&&a[0]!==a[1]&&(L=(0,u.zIndexOrdering)(a,(function(t){return e.edgeDataCache[t].zIndex}),L)),f=0,p=L.length;f