From 5a893f4b768ecc8bb10432dfd4577c2621819087 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 26 Jul 2022 12:52:41 +0200 Subject: [PATCH] feat: LeanInk backlink step 1 --- DocGen4/LeanInk/Output.lean | 35 ++++++----------- DocGen4/LeanInk/Process.lean | 75 ++++++++++++++++++++++-------------- DocGen4/Output.lean | 19 ++++----- DocGen4/Output/Base.lean | 4 ++ Main.lean | 2 +- lean_packages/manifest.json | 2 +- 6 files changed, 70 insertions(+), 67 deletions(-) diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 60d1d31..a01ce80 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -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 -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 diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean index 26ab8db..8c327e8 100644 --- a/DocGen4/LeanInk/Process.lean +++ b/DocGen4/LeanInk/Process.lean @@ -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 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index d79b8b9..3a6bdd7 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -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 := { diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 469b77c..8fd2d7c 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -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. -/ diff --git a/Main.lean b/Main.lean index 00606b7..8b074cb 100644 --- a/Main.lean +++ b/Main.lean @@ -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 diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index a039515..ed6a9b1 100644 --- a/lean_packages/manifest.json +++ b/lean_packages/manifest.json @@ -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",