feat: LeanInk backlink step 1
parent
4c55f98c54
commit
5a893f4b76
|
@ -5,7 +5,6 @@ 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
|
||||
|
||||
|
@ -17,7 +16,8 @@ open scoped DocGen4.Jsx
|
|||
structure AlectryonContext where
|
||||
counter : Nat
|
||||
|
||||
abbrev AlectryonM := StateT AlectryonContext HtmlM
|
||||
abbrev AlectryonT := StateT AlectryonContext
|
||||
abbrev AlectryonM := AlectryonT HtmlM
|
||||
|
||||
def getNextButtonLabel : AlectryonM String := do
|
||||
let val ← get
|
||||
|
@ -197,27 +197,14 @@ def baseHtml (content : Array Html) : AlectryonM Html := do
|
|||
</body>
|
||||
</html>
|
||||
|
||||
def renderFragments (fs : Array Fragment) : AlectryonM Html :=
|
||||
fs.mapM Fragment.toHtml >>= baseHtml
|
||||
def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
|
||||
let config ← read
|
||||
annotateFileWithCompounds [] config.inputFileContents as
|
||||
|
||||
-- TODO: rework monad mess
|
||||
def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
|
||||
let fs ← annotationsToFragments as
|
||||
let (html, _) := fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 } |>.run (←readThe SiteContext) (←readThe SiteBaseContext)
|
||||
pure html
|
||||
|
||||
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 := withTheReader SiteBaseContext (setCurrentName module.name) do
|
||||
let json ← runInk inkPath sourceFilePath
|
||||
let fragments := fromJson? json
|
||||
match fragments with
|
||||
| .ok fragments =>
|
||||
let render := StateT.run (LeanInk.Annotation.Alectryon.renderFragments fragments) { counter := 0 }
|
||||
let ctx ← read
|
||||
let baseCtx ← readThe SiteBaseContext
|
||||
let (html, _) := render |>.run ctx baseCtx
|
||||
pure html
|
||||
| .error err => throw <| IO.userError s!"Error while parsing LeanInk Output: {err}"
|
||||
|
||||
end DocGen4.Output.LeanInk
|
||||
|
|
|
@ -3,38 +3,55 @@ 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
|
||||
import Lean
|
||||
import LeanInk.Analysis
|
||||
import LeanInk.Annotation
|
||||
import DocGen4.LeanInk.Output
|
||||
import DocGen4.Output.Base
|
||||
|
||||
namespace DocGen4.Output.LeanInk
|
||||
namespace DocGen4.Process.LeanInk
|
||||
|
||||
open Lean
|
||||
open IO
|
||||
open DocGen4.Output
|
||||
-- TODO: rework monad mess
|
||||
def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
|
||||
let some modName := getCurrentName |>.run (←readThe SiteBaseContext) | unreachable!
|
||||
let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as |>.run (←readThe SiteContext) (←readThe SiteBaseContext)
|
||||
let srcDir := moduleNameToDirectory srcBasePath modName
|
||||
let srcPath := moduleNameToFile srcBasePath modName
|
||||
IO.FS.createDirAll srcDir
|
||||
IO.FS.writeFile srcPath srcHtml.toString
|
||||
pure 0
|
||||
|
||||
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
|
||||
def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
|
||||
let ctx ← readThe SiteContext
|
||||
let baseCtx ← readThe SiteBaseContext
|
||||
let outputFn := (λ as => docGenOutput as |>.run ctx baseCtx)
|
||||
return ← LeanInk.Analysis.runAnalysis {
|
||||
name := "doc-gen4"
|
||||
genOutput := outputFn
|
||||
}
|
||||
|
||||
def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
|
||||
execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config
|
||||
|
||||
@[implementedBy enableInitializersExecution]
|
||||
private def enableInitializersExecutionWrapper : IO Unit := pure ()
|
||||
|
||||
def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
|
||||
let contents ← IO.FS.readFile sourceFilePath
|
||||
let config := {
|
||||
inputFilePath := sourceFilePath
|
||||
inputFileContents := contents
|
||||
lakeFile := none
|
||||
verbose := false
|
||||
prettifyOutput := true
|
||||
experimentalTypeInfo := true
|
||||
experimentalDocString := true
|
||||
experimentalSemanticType := true
|
||||
}
|
||||
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}"
|
||||
enableInitializersExecutionWrapper
|
||||
if (← execAux config) != 0 then
|
||||
throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
|
||||
|
||||
end DocGen4.Output.LeanInk
|
||||
end DocGen4.Process.LeanInk
|
||||
|
|
|
@ -13,17 +13,13 @@ import DocGen4.Output.NotFound
|
|||
import DocGen4.Output.Find
|
||||
import DocGen4.Output.SourceLinker
|
||||
import DocGen4.Output.ToJson
|
||||
import DocGen4.LeanInk.Output
|
||||
import DocGen4.LeanInk.Process
|
||||
import Std.Data.HashMap
|
||||
|
||||
namespace DocGen4
|
||||
|
||||
open Lean IO System Output Process Std
|
||||
|
||||
def basePath := FilePath.mk "." / "build" / "doc"
|
||||
def srcBasePath := basePath / "src"
|
||||
def declarationsBasePath := basePath / "declarations"
|
||||
|
||||
def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
|
||||
let findBasePath := basePath / "find"
|
||||
|
||||
|
@ -97,7 +93,10 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
|
|||
let filePath := moduleNameToFile basePath modName
|
||||
-- path: 'basePath/module/components/till/last.html'
|
||||
-- The last component is the file name, so we drop it from the depth to root.
|
||||
let baseConfig := { baseConfig with depthToRoot := modName.components.dropLast.length }
|
||||
let baseConfig := { baseConfig with
|
||||
depthToRoot := modName.components.dropLast.length
|
||||
currentName := some modName
|
||||
}
|
||||
let moduleHtml := moduleToHtml module |>.run config baseConfig
|
||||
FS.createDirAll fileDir
|
||||
FS.writeFile filePath moduleHtml.toString
|
||||
|
@ -106,12 +105,8 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
|
|||
IO.println s!"Inking: {modName.toString}"
|
||||
-- path: 'basePath/src/module/components/till/last.html'
|
||||
-- The last component is the file name, however we are in src/ here so dont drop it this time
|
||||
let baseConfig := { baseConfig with depthToRoot := modName.components.length }
|
||||
let srcHtml ← LeanInk.moduleToHtml module inkPath inputPath |>.run config baseConfig
|
||||
let srcDir := moduleNameToDirectory srcBasePath modName
|
||||
let srcPath := moduleNameToFile srcBasePath modName
|
||||
FS.createDirAll srcDir
|
||||
FS.writeFile srcPath srcHtml.toString
|
||||
let baseConfig := {baseConfig with depthToRoot := modName.components.length }
|
||||
Process.LeanInk.runInk inputPath |>.run config baseConfig
|
||||
|
||||
def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
|
||||
{
|
||||
|
|
|
@ -12,6 +12,10 @@ namespace DocGen4.Output
|
|||
open scoped DocGen4.Jsx
|
||||
open Lean System Widget Elab Process
|
||||
|
||||
def basePath := FilePath.mk "." / "build" / "doc"
|
||||
def srcBasePath := basePath / "src"
|
||||
def declarationsBasePath := basePath / "declarations"
|
||||
|
||||
/--
|
||||
The context used in the `BaseHtmlM` monad for HTML templating.
|
||||
-/
|
||||
|
|
|
@ -34,7 +34,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
|
|||
| Except.error rc => pure rc
|
||||
|
||||
def runIndexCmd (_p : Parsed) : IO UInt32 := do
|
||||
let hierarchy ← Hierarchy.fromDirectory basePath
|
||||
let hierarchy ← Hierarchy.fromDirectory Output.basePath
|
||||
let baseConfig := getSimpleBaseContext hierarchy
|
||||
htmlOutputIndex baseConfig
|
||||
pure 0
|
||||
|
|
|
@ -4,7 +4,7 @@
|
|||
"rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
|
||||
"name": "Cli"},
|
||||
{"url": "https://github.com/hargonix/LeanInk",
|
||||
"rev": "cb529041f71a4ea8348628a8c723326e3e4bdecc",
|
||||
"rev": "3ab183e60a2aa082fb20c3bc139b992f683ae1d4",
|
||||
"name": "leanInk"},
|
||||
{"url": "https://github.com/xubaiw/Unicode.lean",
|
||||
"rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",
|
||||
|
|
Loading…
Reference in New Issue