From d53565d8ac19dee92b9c3de73b36a93336950561 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 28 Sep 2024 12:17:11 +0000 Subject: [PATCH] feat: Improvements to dependency graph --- .github/workflows/docs.yml | 2 +- docs/_layouts/default.html | 2 +- scripts/MetaPrograms/informal.lean | 163 +++++++++++++++++++++++++++-- 3 files changed, 159 insertions(+), 8 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 2e8cddd..9590ca8 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -45,7 +45,7 @@ jobs: run : lake exe find_TODOs mkFile - name: make list of informal proofs and lemmas - run : lake exe informal mkFile mkDot + run : lake exe informal mkFile mkDot mkHTML - name: Generate svg from dot run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html index b7977a1..3a47872 100644 --- a/docs/_layouts/default.html +++ b/docs/_layouts/default.html @@ -28,7 +28,7 @@ Download .tar.gz {% endif %} TODO List - Help formalize + Help formalize
diff --git a/scripts/MetaPrograms/informal.lean b/scripts/MetaPrograms/informal.lean index 963d894..7b2deeb 100644 --- a/scripts/MetaPrograms/informal.lean +++ b/scripts/MetaPrograms/informal.lean @@ -212,7 +212,7 @@ def formalToNode (nameSpaces : Array Name) (d : Name) : MetaM String := do let prefixName := if nameSpaces.contains d then d else d.getPrefix let nodeStr := s!"\"{d}\"[label=\"{d}\", shape=box, style=filled, fillcolor=steelblue, - href=\"{webPath}#L{lineNo}\", tooltip=\"{docstring}\"]" + tooltip=\"{docstring}\"]" if prefixName = Lean.Name.anonymous then pure nodeStr else @@ -226,7 +226,7 @@ unsafe def informalLemmaToNode (nameSpaces : Array Name) (c : Import × Constant let prefixName := if nameSpaces.contains c.2.name then c.2.name else c.2.name.getPrefix let nodeStr := s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=ellipse, style=filled, fillcolor=lightgray, - href=\"{webPath}#L{lineNo}\", tooltip=\"{informalLemma.math}\"]" + tooltip=\"{informalLemma.math}\"]" if prefixName = Lean.Name.anonymous then pure nodeStr else @@ -240,7 +240,7 @@ unsafe def informalDefToNode (nameSpaces : Array Name) (c : Import × ConstantIn let prefixName := if nameSpaces.contains c.2.name then c.2.name else c.2.name.getPrefix let nodeStr := s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=box, style=filled, fillcolor=lightgray, - href=\"{webPath}#L{lineNo}\", tooltip=\"{informalDef.math}\"]" + tooltip=\"{informalDef.math}\"]" if prefixName = Lean.Name.anonymous then pure nodeStr else @@ -309,10 +309,8 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do packmode=\"array1\"; ]; tooltip = \"Informal HepLean graph\"; - node [margin=0.05; fontsize=10; fontname=\"Georgia\", height=0.1]; + node [margin=\"0.2,0.05\"; fontsize=10; fontname=\"Georgia\", height=0.1]; bgcolor=\"white\"; - label=\"Informal dependency graph for HepLean. - Blue nodes are formalized, gray are to be formalized.\"; labelloc=\"t\"; labeljust=\"l\"; edge [arrowhead=vee];" @@ -322,6 +320,153 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do end dotFile +section htmlFile + +/-! + +## Making the html file for dependency graph. + +-/ + +def formalToHTML (d : Name) : MetaM String := do + let lineNo ← getLineNumber d + let mod ← getModule d + let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ + (mod.toString.replace "." "/") ++ ".lean" + let docstring ← getDocString d + pure s!" +
+{d}
+Docstring: {docstring} + +
" + +unsafe def informalLemmaToHTML (c : Import × ConstantInfo) : MetaM String := do + let lineNo ← getLineNumber c.2.name + let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ + (c.1.module.toString.replace "." "/") ++ ".lean" + let informalLemma ← (constantInfoToInformalLemma c.2) + pure s!" +
+{c.2.name}
+Math description: {informalLemma.math}
+Physics description: {informalLemma.physics}
+
" + +unsafe def informalDefToHTML (c : Import × ConstantInfo) : MetaM String := do + let lineNo ← getLineNumber c.2.name + let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ + (c.1.module.toString.replace "." "/") ++ ".lean" + let informalDef ← (constantInfoToInformalDefinition c.2) + pure s!" +
+{c.2.name}
+Math description: {informalDef.math}
+Physics description: {informalDef.physics}
+
" + +unsafe def informalToHTML (c : Import × ConstantInfo) : MetaM String := do + if Informal.isInformalLemma c.2 then + informalLemmaToHTML c + else if Informal.isInformalDef c.2 then + informalDefToHTML c + else + pure "" + +unsafe def toHTML (imports : Array Import) : MetaM String := do + let informal ← imports.mapM importToInformal + let informal := informal.flatten + let deps ← (informal.map (fun c => c.2)).mapM informalDependencies + let deps := deps.flatten + let informal_name := informal.map (fun c => c.2.name) + let formal_deps := deps.filter (fun d => d ∉ informal_name) + let formal_nodes ← formal_deps.mapM (formalToHTML) + let nodes := String.intercalate "\n" formal_nodes.toList + let informalNodes ← informal.mapM (informalToHTML) + let informalNodes := String.intercalate "\n" informalNodes.toList + let header := " + + + + Interactive Graph with Node-Specific Text Display + + + + + + + + + + + +

Interactive Graph

+ + +
+ + + + +
+ +
" + let footer := " + + + +" + pure (header ++ "\n" ++ nodes ++ "\n" ++ + informalNodes ++ "\n" ++ footer) + +end htmlFile /-! ## Main function @@ -351,4 +496,10 @@ unsafe def main (args : List String) : IO UInt32 := do let dotFile : System.FilePath := {toString := "./docs/InformalDot.dot"} IO.FS.writeFile dotFile dot IO.println (s!"Dot file made.") + /- Making the html file. -/ + if "mkHTML" ∈ args then + let html ← CoreM.withImportModules #[`HepLean] (toHTML imports).run' + let htmlFile : System.FilePath := {toString := "./docs/InformalGraph.html"} + IO.FS.writeFile htmlFile html + IO.println (s!"HTML file made.") pure 0