feat: LeanInk all the files, HTML generation missing

DocGen4.lean

@@ -7,3 +7,4 @@ import DocGen4.Process
 import DocGen4.Load
 import DocGen4.IncludeStr
 import DocGen4.Output
+import DocGen4.LeanInk

DocGen4/LeanInk.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.LeanInk.Process
+import DocGen4.LeanInk.Output

DocGen4/LeanInk/Output.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Xubai Wang
+-/
+import DocGen4.Output.Base
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.LeanInk.Process
+import Lean.Data.Json
+import LeanInk.Annotation.Alectryon
+
+namespace LeanInk.Annotation.Alectryon
+
+open DocGen4 Output
+open scoped DocGen4.Jsx
+
+def TypeInfo.toHtml : TypeInfo → HtmlM Html := sorry
+
+def Token.toHtml : Token → HtmlM Html := sorry
+
+def Contents.toHtml : Contents → HtmlM Html
+  | .string value => sorry
+  | .experimentalTokens value => sorry
+
+def Hypothesis.toHtml : Hypothesis → HtmlM Html := sorry
+
+def Goal.toHtml : Goal → HtmlM Html := sorry
+
+def Message.toHtml : Message → HtmlM Html := sorry
+
+def Sentence.toHtml : Sentence → HtmlM Html := sorry
+
+def Text.toHtml : Text → HtmlM Html := sorry
+
+def Fragment.toHtml : Fragment → HtmlM Html
+  | .text value => sorry
+  | .sentence value => sorry
+
+end LeanInk.Annotation.Alectryon
+
+namespace DocGen4.Output.LeanInk
+
+open Lean
+open LeanInk.Annotation.Alectryon
+open scoped DocGen4.Jsx
+
+def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withReader (setCurrentName module.name) do
+  let json ← runInk inkPath sourceFilePath
+  let fragments : Except String (Array Fragment) := fromJson? json
+  match fragments with
+  | .ok fragments => pure $ <div>hello</div>
+  | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
+
+end DocGen4.Output.LeanInk

DocGen4/LeanInk/Process.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean.Data.Json
+
+namespace DocGen4.Output.LeanInk
+
+open Lean
+open IO
+
+def runInk (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : IO Json := do
+  let arguments := #[
+    "analyze", sourceFilePath.toString,
+    "--lake", "lakefile.lean",
+    "--x-enable-type-info",
+    "--x-enable-docStrings",
+    "--x-enable-semantic-token"
+  ]
+  let inkProcess ← Process.spawn {
+    stdin := Process.Stdio.null
+    stdout := Process.Stdio.piped
+    stderr := Process.Stdio.piped
+    cmd := inkPath.toString
+    args := arguments
+  }
+  match (←inkProcess.wait) with
+  | 0 =>
+    let outputFilePath := sourceFilePath.withExtension "lean.leanInk"
+    let output ← FS.readFile outputFilePath
+    FS.removeFile outputFilePath
+    match Json.parse output with
+    | .ok out => pure out
+    | .error err =>
+      throw $ IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
+  | code =>
+    throw $ IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
+
+end DocGen4.Output.LeanInk

DocGen4/Output.lean

@@ -13,6 +13,7 @@ import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.Semantic
 import DocGen4.Output.SourceLinker
+import DocGen4.LeanInk.Output
 
 namespace DocGen4
 
@@ -22,15 +23,27 @@ open Lean IO System Output Process
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do
-  let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
+  let config := {
+    depthToRoot := 0,
+    result := result,
+    currentName := none,
+    sourceLinker := ←sourceLinker ws leanHash
+    leanInkEnabled := inkPath.isSome
+  }
   let basePath := FilePath.mk "." / "build" / "doc"
+  let srcBasePath := basePath / "src"
   let indexHtml := ReaderT.run index config 
   let findHtml := ReaderT.run find { config with depthToRoot := 1 }
   let notFoundHtml := ReaderT.run notFound config
+  -- Rendering the entire lean compiler takes time....
+  --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
+  let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
+
   FS.createDirAll basePath
   FS.createDirAll (basePath / "find")
   FS.createDirAll (basePath / "semantic")
+  FS.createDirAll srcBasePath
 
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
@@ -46,6 +59,14 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
       declList := declList.push obj
       let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config 
       FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
+    if let some inkPath := inkPath then
+      if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" mod.name then
+        IO.println s!"Inking: {mod.name.toString}"
+        let srcHtml ← ReaderT.run (LeanInk.moduleToHtml mod inkPath inputPath) config
+        let srcDir := moduleNameToDirectory srcBasePath mod.name
+        let srcPath := moduleNameToFile srcBasePath mod.name
+        FS.createDirAll srcDir
+        FS.writeFile srcPath srcHtml.toString
   let json := Json.arr declList
 
   FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config 

DocGen4/Output/Base.lean

@@ -33,6 +33,10 @@ structure SiteContext where
   A function to link declaration names to their source URLs, usually Github ones.
   -/
   sourceLinker : Name → Option DeclarationRange → String
+  /--
+  Whether LeanInk is enabled
+  -/
+  leanInkEnabled : Bool
 
 def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name}
 
@@ -52,6 +56,7 @@ def getRoot : HtmlM String := do
 def getResult : HtmlM AnalyzerResult := do pure (←read).result
 def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
 def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
+def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
 
 /--
 If a template is meant to be extended because it for example only provides the
@@ -73,6 +78,13 @@ Returns the HTML doc-gen4 link to a module name.
 def moduleToHtmlLink (module : Name) : HtmlM Html := do
   pure <a href={←moduleNameToLink module}>{module.toString}</a>
 
+/--
+Returns the LeanInk link to a module name.
+-/
+def moduleNameToInkLink (n : Name) : HtmlM String := do
+  let parts := "src" :: n.components.map Name.toString
+  pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
 /--
 Returns the path to the HTML file that contains information about a module.
 -/
@@ -87,7 +99,6 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
   let parts := n.components.dropLast.map Name.toString
   basePath / parts.foldl (· / ·) (FilePath.mk ".")
 
-
 section Static
 /-!
 The following section contains all the statically included files that
@@ -114,15 +125,21 @@ def declNameToLink (name : Name) : HtmlM String := do
 Returns the HTML doc-gen4 link to a declaration name.
 -/
 def declNameToHtmlLink (name : Name) : HtmlM Html := do
-  let link ← declNameToLink name
   pure <a href={←declNameToLink name}>{name.toString}</a>
 
+/--
+Returns the LeanInk link to a declaration name.
+-/
+def declNameToInkLink (name : Name) : HtmlM String := do
+  let res ← getResult
+  let module := res.moduleNames[res.name2ModIdx.find! name]
+  pure $ (←moduleNameToInkLink module) ++ "#" ++ name.toString
+
 /--
 Returns the HTML doc-gen4 link to a declaration name with "break_within"
 set as class.
 -/
 def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
-  let link ← declNameToLink name
   pure <a class="break_within" href={←declNameToLink name}>{name.toString}</a>
 
 /--

DocGen4/Output/Module.lean

@@ -114,6 +114,15 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
     else
       #[]
+  let leanInkHtml :=
+    if ←leanInkEnabled? then
+      #[
+        <div class="ink_link">
+          <a href={←declNameToInkLink doc.getName}>ink</a>
+        </div>
+      ]
+    else
+      #[]
 
   pure
     <div class="decl" id={doc.getName.toString}>
@@ -121,6 +130,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         <div class="gh_link">
           <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
         </div>
+        [leanInkHtml]
         [attrsHtml]
         {←docInfoHeader doc}
         [docInfoHtml]

Main.lean

@@ -5,6 +5,7 @@ import Cli
 open DocGen4 Lean Cli
 
 def runDocGenCmd (p : Parsed) : IO UInt32 := do
+  IO.println s!"{p}"
   let modules : List String := p.variableArgsAs! String |>.toList
   let res ← lakeSetup modules
   match res with
@@ -12,7 +13,14 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
     IO.println s!"Loading modules from: {←searchPathRef.get}"
     let doc ← load $ modules.map Name.mkSimple
     IO.println "Outputting HTML"
-    htmlOutput doc ws leanHash
+    match p.flag? "ink" with
+    | some ink =>
+      let inkPath := System.FilePath.mk ink.value
+      if ←inkPath.pathExists then
+         htmlOutput doc ws leanHash inkPath
+      else
+        throw $ IO.userError "Invalid path to LeanInk binary provided"
+    | none => htmlOutput doc ws leanHash none
     pure 0
   | Except.error rc => pure rc
 
@@ -20,6 +28,9 @@ def docGenCmd : Cmd := `[Cli|
   "doc-gen4" VIA runDocGenCmd; ["0.0.1"]
   "A documentation generator for Lean 4."
 
+  FLAGS:
+    ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
+
   ARGS:
     ...modules : String; "The modules to generate the HTML for"
 ]

lakefile.lean

@@ -24,4 +24,4 @@ require lake from git
   "https://github.com/leanprover/lake" @ "12e2463b35829368a59d18a5504dd2f73ac1621d"
 
 require leanInk from git
-  "https://github.com/leanprover/LeanInk" @ "0a160d91458c1873937449a7c78d25b34b8686df"
+  "https://github.com/hargonix/LeanInk" @ "doc-gen"