diff --git a/DocGen4.lean b/DocGen4.lean
index 0ae1c74..8456fa1 100644
--- a/DocGen4.lean
+++ b/DocGen4.lean
@@ -7,3 +7,4 @@ import DocGen4.Process
import DocGen4.Load
import DocGen4.IncludeStr
import DocGen4.Output
+import DocGen4.LeanInk
diff --git a/DocGen4/LeanInk.lean b/DocGen4/LeanInk.lean
new file mode 100644
index 0000000..c4b326a
--- /dev/null
+++ b/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
diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
new file mode 100644
index 0000000..41986d9
--- /dev/null
+++ b/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 $
hello
+ | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
+
+end DocGen4.Output.LeanInk
diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean
new file mode 100644
index 0000000..0f9661f
--- /dev/null
+++ b/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
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 59ad9e7..3947a7d 100644
--- a/DocGen4/Output.lean
+++ b/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
- let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
+def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do
+ 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
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 795daa8..9d7aa10 100644
--- a/DocGen4/Output/Base.lean
+++ b/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 {module.toString}
+/--
+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 {name.toString}
+/--
+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 {name.toString}
/--
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index d1ea32b..8b1a3d4 100644
--- a/DocGen4/Output/Module.lean
+++ b/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
+ #[
+
+ ]
+ else
+ #[]
pure
@@ -121,6 +130,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
+ [leanInkHtml]
[attrsHtml]
{←docInfoHeader doc}
[docInfoHtml]
diff --git a/Main.lean b/Main.lean
index 8bb1187..686e0c9 100644
--- a/Main.lean
+++ b/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"
]
diff --git a/lakefile.lean b/lakefile.lean
index fd4d4c3..eb5e8fd 100644
--- a/lakefile.lean
+++ b/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"