From 199c7af17a2a94a32ebb99fe79b6a51d706cecd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 20 Jun 2022 00:31:09 +0200 Subject: [PATCH 1/5] feat: LeanInk all the files, HTML generation missing --- DocGen4.lean | 1 + DocGen4/LeanInk.lean | 7 +++++ DocGen4/LeanInk/Output.lean | 54 ++++++++++++++++++++++++++++++++++++ DocGen4/LeanInk/Process.lean | 40 ++++++++++++++++++++++++++ DocGen4/Output.lean | 25 +++++++++++++++-- DocGen4/Output/Base.lean | 23 +++++++++++++-- DocGen4/Output/Module.lean | 10 +++++++ Main.lean | 13 ++++++++- lakefile.lean | 2 +- 9 files changed, 168 insertions(+), 7 deletions(-) create mode 100644 DocGen4/LeanInk.lean create mode 100644 DocGen4/LeanInk/Output.lean create mode 100644 DocGen4/LeanInk/Process.lean 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 + #[ +
+ ink +
+ ] + else + #[] pure
@@ -121,6 +130,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
source
+ [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" From 9f50966339d1d3bbe50305ba50cf3e293d3ed7a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 20 Jun 2022 18:39:55 +0200 Subject: [PATCH 2/5] feat: initial LeanInk HTML generation --- DocGen4/LeanInk/Output.lean | 158 +++++- DocGen4/Output.lean | 32 +- DocGen4/Output/Base.lean | 4 + DocGen4/Output/ToHtmlFormat.lean | 34 +- static/alectryon/alectryon.css | 777 ++++++++++++++++++++++++++++ static/alectryon/alectryon.js | 172 ++++++ static/alectryon/docutils_basic.css | 593 +++++++++++++++++++++ 7 files changed, 1729 insertions(+), 41 deletions(-) create mode 100644 static/alectryon/alectryon.css create mode 100644 static/alectryon/alectryon.js create mode 100644 static/alectryon/docutils_basic.css diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 41986d9..91db9b6 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -14,27 +14,151 @@ namespace LeanInk.Annotation.Alectryon open DocGen4 Output open scoped DocGen4.Jsx -def TypeInfo.toHtml : TypeInfo → HtmlM Html := sorry +structure AlectryonContext where + counter : Nat -def Token.toHtml : Token → HtmlM Html := sorry +abbrev AlectryonM := StateT AlectryonContext HtmlM -def Contents.toHtml : Contents → HtmlM Html - | .string value => sorry - | .experimentalTokens value => sorry +def getNextButtonLabel : AlectryonM String := do + let val ← get + let newCounter := val.counter + 1 + set { val with counter := newCounter } + pure s!"plain-lean4-lean-chk{val.counter}" -def Hypothesis.toHtml : Hypothesis → HtmlM Html := sorry +def TypeInfo.toHtml : TypeInfo → AlectryonM Html := sorry -def Goal.toHtml : Goal → HtmlM Html := sorry +def Token.toHtml (t : Token) : AlectryonM Html := do + -- TODO: Show rest of token + pure $ Html.text t.raw -def Message.toHtml : Message → HtmlM Html := sorry +def Contents.toHtml : Contents → AlectryonM (Array Html) + | .string value => pure #[Html.text value] + | .experimentalTokens values => values.mapM Token.toHtml -def Sentence.toHtml : Sentence → HtmlM Html := sorry +def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do + let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]] + if h.body != "" then + hypParts := hypParts.push + + := + {h.body} + + hypParts := hypParts.push + + : + {h.type} + -def Text.toHtml : Text → HtmlM Html := sorry + pure + + [hypParts] + -def Fragment.toHtml : Fragment → HtmlM Html - | .text value => sorry - | .sentence value => sorry +def Goal.toHtml (g : Goal) : AlectryonM Html := do + let mut hypotheses := #[] + for hyp in g.hypotheses do + let rendered ← hyp.toHtml + hypotheses := hypotheses.push rendered + hypotheses := hypotheses.push
+ pure +
+
+ [hypotheses] + + +
{g.name} + +
+ {g.conclusion} + + + +def Message.toHtml (m : Message) : AlectryonM Html := do + pure +
+ -- TODO: This might have to be done in a fancier way + {m.contents} + + +def Sentence.toHtml (s : Sentence) : AlectryonM Html := do + let messages := + if s.messages.size > 0 then + #[ +
+ [←s.messages.mapM Message.toHtml] + + ] + else + #[] + + let goals := + if s.goals.size > 0 then + -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it + #[ +
+ [←s.goals.mapM Goal.toHtml] + + ] + else + #[] + + let buttonLabel ← getNextButtonLabel + + pure + + +