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 1/8] 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", From 14afcdbeaf52250d993c9974c2148117183ca147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 26 Jul 2022 13:56:22 +0200 Subject: [PATCH 2/8] feat: Degrade --ink to flag --- DocGen4/Output.lean | 10 +++++----- Main.lean | 18 ++++-------------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 3a6bdd7..d92d9d6 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -72,11 +72,11 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do let jsonDecls ← Module.toJson mod FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress -def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do +def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do let config : SiteContext := { result := result, sourceLinker := ←sourceLinker ws - leanInkEnabled := inkPath.isSome + leanInkEnabled := ink } FS.createDirAll basePath @@ -100,7 +100,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( let moduleHtml := moduleToHtml module |>.run config baseConfig FS.createDirAll fileDir FS.writeFile filePath moduleHtml.toString - if let some inkPath := inkPath then + if ink then if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then IO.println s!"Inking: {modName.toString}" -- path: 'basePath/src/module/components/till/last.html' @@ -134,9 +134,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do The main entrypoint for outputting the documentation HTML based on an `AnalyzerResult`. -/ -def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do +def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do let baseConfig := getSimpleBaseContext hierarchy - htmlOutputResults baseConfig result ws inkPath + htmlOutputResults baseConfig result ws ink htmlOutputIndex baseConfig end DocGen4 diff --git a/Main.lean b/Main.lean index 8b074cb..2d083eb 100644 --- a/Main.lean +++ b/Main.lean @@ -4,16 +4,6 @@ import Cli open DocGen4 Lean Cli -def findLeanInk? (p : Parsed) : IO (Option System.FilePath) := do - match p.flag? "ink" with - | some ink => - let inkPath := System.FilePath.mk ink.value - if ←inkPath.pathExists then - pure <| some inkPath - else - throw <| IO.userError "Invalid path to LeanInk binary provided" - | none => pure none - def getTopLevelModules (p : Parsed) : IO (List String) := do let topLevelModules := p.variableArgsAs! String |>.toList if topLevelModules.length == 0 then @@ -29,7 +19,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules) IO.println "Outputting HTML" let baseConfig := getSimpleBaseContext hierarchy - htmlOutputResults baseConfig doc ws (←findLeanInk? p) + htmlOutputResults baseConfig doc ws (p.hasFlag "ink") pure 0 | Except.error rc => pure rc @@ -51,7 +41,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do let modules := modules.map String.toName let (doc, hierarchy) ← load (.loadAll modules) IO.println "Outputting HTML" - htmlOutput doc hierarchy ws (←findLeanInk? p) + htmlOutput doc hierarchy ws (p.hasFlag "ink") pure 0 | Except.error rc => pure rc @@ -60,7 +50,7 @@ def singleCmd := `[Cli| "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated." FLAGS: - ink : String; "Path to a LeanInk binary to use for rendering the Lean sources." + ink; "Render the files with LeanInk in addition" ARGS: module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules." @@ -78,7 +68,7 @@ def docGenCmd : Cmd := `[Cli| "A documentation generator for Lean 4." FLAGS: - ink : String; "Path to a LeanInk binary to use for rendering the Lean sources." + ink; "Render the files with LeanInk in addition" ARGS: ...modules : String; "The modules to generate the HTML for." From 0ac64f08738109c212394d134ddbc462673a9a76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 26 Jul 2022 15:12:29 +0200 Subject: [PATCH 3/8] types, types everywhere --- DocGen4/LeanInk/Output.lean | 15 ++++++++++----- DocGen4/Output/Base.lean | 16 ++++++++-------- lean_packages/manifest.json | 2 +- 3 files changed, 19 insertions(+), 14 deletions(-) diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index a01ce80..5c719b1 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -35,7 +35,7 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do {tyi.name} : - {tyi.type} + [←DocGen4.Output.infoFormatToHtml tyi.type.fst] @@ -80,16 +80,16 @@ def Contents.toHtml : Contents → AlectryonM Html def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]] - if h.body != "" then + if h.body.snd != "" then hypParts := hypParts.push := - {h.body} + [←infoFormatToHtml h.body.fst] hypParts := hypParts.push : - {h.type} + [←infoFormatToHtml h.type.fst] pure @@ -103,6 +103,11 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do let rendered ← hyp.toHtml hypotheses := hypotheses.push rendered hypotheses := hypotheses.push
+ let conclusionHtml ← + match g.conclusion with + | .typed info _ => infoFormatToHtml info + | .untyped str => pure <| #[Html.text str] + pure
@@ -112,7 +117,7 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
{g.name}
- {g.conclusion} + [conclusionHtml]
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 8fd2d7c..c2292d1 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -209,14 +209,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do | Info.ofTermInfo i => match i.expr.consumeMData with | Expr.const name _ => - match t with - | TaggedText.text t => - let (front, t, back) := splitWhitespaces <| Html.escape t - let elem := {t} - pure #[Html.text front, elem, Html.text back] - | _ => - -- TODO: Is this ever reachable? - pure #[[←infoFormatToHtml t]] + match t with + | TaggedText.text t => + let (front, t, back) := splitWhitespaces <| Html.escape t + let elem := {t} + pure #[Html.text front, elem, Html.text back] + | _ => + -- TODO: Is this ever reachable? + pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index ed6a9b1..c8924d6 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": "3ab183e60a2aa082fb20c3bc139b992f683ae1d4", + "rev": "0c113bb4cc88d4b8dc6b2d26a4c4c9cf6008a2eb", "name": "leanInk"}, {"url": "https://github.com/xubaiw/Unicode.lean", "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0", From 5bae061b544f25d89655330e954eeb351fbbc9cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 27 Jul 2022 20:11:41 +0200 Subject: [PATCH 4/8] fix: mess of monad transformers in LeanInk adapter --- DocGen4/LeanInk/Output.lean | 2 +- DocGen4/LeanInk/Process.lean | 8 ++++---- DocGen4/Output/Base.lean | 6 ++++++ 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 5c719b1..60f7a86 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -209,7 +209,7 @@ def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List F -- 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) + let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 } pure html end LeanInk.Annotation.Alectryon diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean index 8c327e8..dcd31aa 100644 --- a/DocGen4/LeanInk/Process.lean +++ b/DocGen4/LeanInk/Process.lean @@ -13,10 +13,10 @@ namespace DocGen4.Process.LeanInk open Lean 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 some modName ← getCurrentName | unreachable! + let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as let srcDir := moduleNameToDirectory srcBasePath modName let srcPath := moduleNameToFile srcBasePath modName IO.FS.createDirAll srcDir @@ -26,7 +26,7 @@ def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.Analy def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do let ctx ← readThe SiteContext let baseCtx ← readThe SiteBaseContext - let outputFn := (λ as => docGenOutput as |>.run ctx baseCtx) + let outputFn := (docGenOutput · |>.run ctx baseCtx) return ← LeanInk.Analysis.runAnalysis { name := "doc-gen4" genOutput := outputFn diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index c2292d1..331fe58 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -66,6 +66,12 @@ def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α := ReaderT.run x ctx |>.run baseCtx |>.run +instance [Monad m] : MonadLift HtmlM (HtmlT m) where + monadLift x := do pure <| x.run (←readThe SiteContext) (←readThe SiteBaseContext) + +instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where + monadLift x := do pure <| x.run (←readThe SiteBaseContext) + /-- Obtains the root URL as a relative one to the current depth. -/ From 6534a71ccacad76aa4a2109002375378dfa9bf91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 11 Aug 2022 18:30:28 +0200 Subject: [PATCH 5/8] chore: update toolchain --- DocGen4.lean | 1 - DocGen4/IncludeStr.lean | 57 ------------------------------- DocGen4/Load.lean | 13 ++++--- DocGen4/Output/Base.lean | 1 - DocGen4/Output/SourceLinker.lean | 21 ++++++------ DocGen4/Process/Attributes.lean | 3 +- DocGen4/Process/InstanceInfo.lean | 3 +- lakefile.lean | 19 ----------- lean-toolchain | 2 +- lean_packages/manifest.json | 12 +++---- 10 files changed, 27 insertions(+), 105 deletions(-) delete mode 100644 DocGen4/IncludeStr.lean diff --git a/DocGen4.lean b/DocGen4.lean index 8456fa1..09a4641 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -5,6 +5,5 @@ Authors: Henrik Böving -/ import DocGen4.Process import DocGen4.Load -import DocGen4.IncludeStr import DocGen4.Output import DocGen4.LeanInk diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean deleted file mode 100644 index c4b28a9..0000000 --- a/DocGen4/IncludeStr.lean +++ /dev/null @@ -1,57 +0,0 @@ -/- -Copyright (c) 2021 Henrik Böving. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Henrik Böving --/ -import Lean - -namespace DocGen4 - -open Lean System IO Lean.Elab.Term FS - -deriving instance DecidableEq for FileType - -/-- - Traverse all subdirectories fo `f` to find if one satisfies `p`. --/ -partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do - if (← p f) then - return f - for d in (← System.FilePath.readDir f) do - let subDir := d.path - let metadata ← subDir.metadata - if metadata.type = FileType.dir then - if let some p ← traverseDir subDir p then - return p - return none - -syntax (name := includeStr) "include_str" str : term - -/-- -Provides a way to include the contents of a file at compile time as a String. -This is used to include things like the CSS and JS in the binary so we -don't have to carry them around as files. --/ -@[termElab includeStr] def includeStrImpl : TermElab := λ stx _ => do - let str := stx[1].isStrLit?.get! - let srcPath := FilePath.mk <| ←getFileName - let currentDir ← IO.currentDir - -- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory. - if let some path ← match srcPath.parent with - | some p => pure <| some <| p / str - | none => do - let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists - pure <| foundDir.map (· / str) - then - if ←path.pathExists then - if ←path.isDir then - throwError s!"{str} is a directory" - else - let content ← FS.readFile path - pure <| mkStrLit content - else - throwError s!"{path} does not exist as a file" - else - throwError s!"No such file in whole directory: {str}" - -end DocGen4 diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e6e9db9..d682e38 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -23,13 +23,16 @@ def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do let (leanInstall?, lakeInstall?) ← Lake.findInstall? match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with | .ok config => - let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio - let libraryLeanGitHash := ws.env.lean.githash + let ws : Lake.Workspace ← Lake.loadWorkspace config + |>.run Lake.MonadLog.eio + |>.toIO (λ _ => IO.userError "Failed to load Lake workspace") + let libraryLeanGitHash := ws.lakeEnv.lean.githash if libraryLeanGitHash ≠ Lean.githash then IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}" - let ctx ← Lake.mkBuildContext ws - (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx - initSearchPath (←findSysroot) ws.leanPaths.oleanPath + let _libs ← ws.runBuild (Lake.buildImportsAndDeps imports) false + |>.run (Lake.MonadLog.eio config.verbosity) + |>.toIO (λ _ => IO.userError "Failed to compile imports via Lake") + initSearchPath (←findSysroot) (ws.packageList.map (·.oleanDir)) pure <| Except.ok ws | .error err => throw <| IO.userError err.toString diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 331fe58..2add29d 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import DocGen4.Process -import DocGen4.IncludeStr import DocGen4.Output.ToHtmlFormat namespace DocGen4.Output diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index e403c5e..d6f66e7 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/DocGen4/Output/SourceLinker.lean @@ -55,20 +55,18 @@ compiler release to work with this provides a function to turn names of declarations into (optionally positional) Github URLs. -/ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do - let leanHash := ws.env.lean.githash + let leanHash := ws.lakeEnv.lean.githash -- Compute a map from package names to source URL let mut gitMap := Std.mkHashMap let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) let projectCommit ← getProjectCommit gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) - for pkg in ws.packageArray do - for dep in pkg.dependencies do - let value := match dep.src with - -- TODO: subdir handling - | Lake.Source.git url commit _ => (getGithubBaseUrl url, commit.getD "main") - -- TODO: What do we do here if linking a source is not possible? - | _ => ("https://example.com", "master") - gitMap := gitMap.insert dep.name value + let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile + |>.run (Lake.MonadLog.eio .normal) + |>.toIO (λ _ => IO.userError "Failed to load lake manifest") + for pkg in manifest.toArray do + let value := (getGithubBaseUrl pkg.url, pkg.rev) + gitMap := gitMap.insert pkg.name value pure λ module range => let parts := module.components.map Name.toString @@ -79,8 +77,9 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange else match ws.packageArray.find? (·.isLocalModule module) with | some pkg => - let (baseUrl, commit) := gitMap.find! pkg.name - s!"{baseUrl}/blob/{commit}/{path}.lean" + match gitMap.find? pkg.name with + | some (baseUrl, commit) => s!"{baseUrl}/blob/{commit}/{path}.lean" + | none => "https://example.com" | none => "https://example.com" match range with diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index a7b1317..3ed7ca3 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -39,7 +39,7 @@ instance : ValueAttr EnumAttributes where Obtain the value of a parametric attribute for a certain name. -/ def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do - let val ← ParametricAttribute.getParam attr env decl + let val ← ParametricAttribute.getParam? attr env decl some (attr.attr.name.toString ++ " " ++ toString val) instance : ValueAttr ParametricAttribute where @@ -108,7 +108,6 @@ def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind pure <| va.getValue attr env decl def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do - let env ← getEnv let mut res := #[] for attr in attrs do if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index dbccd67..14220ce 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -25,8 +25,7 @@ where def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do let mut info ← DefinitionInfo.ofDefinitionVal v - let some className := getClassName (←getEnv) v.type | unreachable! - + let some className ← isClass? v.type | unreachable! if let some instAttr ← getDefaultInstance v.name className then info := { info with attrs := info.attrs.push instAttr } let typeNames ← getInstanceTypes v.type diff --git a/lakefile.lean b/lakefile.lean index 6a1cd23..a9aeedb 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -26,22 +26,3 @@ require lake from git require leanInk from git "https://github.com/hargonix/LeanInk" @ "doc-gen" - -module_facet docs : FilePath := fun mod => do - let some docGen4 ← findLeanExe? `«doc-gen4» - | error "no doc-gen4 executable configuration found in workspace" - let exeTarget ← docGen4.exe.recBuild - let modTarget ← mod.leanBin.recBuild - let buildDir := (← getWorkspace).root.buildDir - let docFile := mod.filePath (buildDir / "doc") "html" - let task ← show SchedulerM _ from do - exeTarget.bindAsync fun exeFile exeTrace => do - modTarget.bindSync fun _ modTrace => do - let depTrace := exeTrace.mix modTrace - buildFileUnlessUpToDate docFile depTrace do - proc { - cmd := exeFile.toString - args := #["single", mod.name.toString] - env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] - } - return ActiveTarget.mk docFile task diff --git a/lean-toolchain b/lean-toolchain index d1e3f76..f62cade 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-07-24 +leanprover/lean4:nightly-2022-08-09 diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index c8924d6..85cbf43 100644 --- a/lean_packages/manifest.json +++ b/lean_packages/manifest.json @@ -1,20 +1,20 @@ -{"version": 1, +{"version": 2, "packages": [{"url": "https://github.com/mhuisi/lean4-cli", "rev": "112b35fc348a4a18d2111ac2c6586163330b4941", "name": "Cli"}, {"url": "https://github.com/hargonix/LeanInk", - "rev": "0c113bb4cc88d4b8dc6b2d26a4c4c9cf6008a2eb", + "rev": "439303af06465824588a486f5f9c023ca69979f3", "name": "leanInk"}, {"url": "https://github.com/xubaiw/Unicode.lean", - "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0", + "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29", "name": "Unicode"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd", "name": "mathlib"}, {"url": "https://github.com/leanprover/lake", - "rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217", + "rev": "6cfb4e3fd7ff700ace8c2cfdb85056d59f321920", "name": "lake"}, {"url": "https://github.com/xubaiw/CMark.lean", - "rev": "8f17d13d3046c517f7f02062918d81bc69e45cce", - "name": "CMark"}]} \ No newline at end of file + "rev": "8c0f9c1b16ee8047813f43b1f92de471782114ff", + "name": "CMark"}]} From cdfd8ff49c09708e0e377998fdd9d10dae2ed936 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 11 Aug 2022 21:37:10 +0200 Subject: [PATCH 6/8] feat: implement facet --- DocGen4/Load.lean | 12 +++---- Main.lean | 57 +++++++++++++++--------------- README.md | 49 +++++--------------------- lakefile.lean | 89 +++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 129 insertions(+), 78 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index d682e38..7b5f20d 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -19,20 +19,13 @@ Sets up a lake workspace for the current project. Furthermore initialize the Lean search path with the path to the proper compiler from lean-toolchain as well as all the dependencies. -/ -def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do +def lakeSetup : IO (Except UInt32 Lake.Workspace) := do let (leanInstall?, lakeInstall?) ← Lake.findInstall? match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with | .ok config => let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio |>.toIO (λ _ => IO.userError "Failed to load Lake workspace") - let libraryLeanGitHash := ws.lakeEnv.lean.githash - if libraryLeanGitHash ≠ Lean.githash then - IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}" - let _libs ← ws.runBuild (Lake.buildImportsAndDeps imports) false - |>.run (Lake.MonadLog.eio config.verbosity) - |>.toIO (λ _ => IO.userError "Failed to compile imports via Lake") - initSearchPath (←findSysroot) (ws.packageList.map (·.oleanDir)) pure <| Except.ok ws | .error err => throw <| IO.userError err.toString @@ -62,4 +55,7 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {} +def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do + load <| .loadAll [`Init, `Std, `Lean] + end DocGen4 diff --git a/Main.lean b/Main.lean index 2d083eb..e098d13 100644 --- a/Main.lean +++ b/Main.lean @@ -11,17 +11,16 @@ def getTopLevelModules (p : Parsed) : IO (List String) := do pure topLevelModules def runSingleCmd (p : Parsed) : IO UInt32 := do - let relevantModules := [p.positionalArg! "module" |>.as! String] - let res ← lakeSetup (relevantModules) - match res with - | Except.ok ws => - let relevantModules := relevantModules.map String.toName - let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules) - IO.println "Outputting HTML" - let baseConfig := getSimpleBaseContext hierarchy - htmlOutputResults baseConfig doc ws (p.hasFlag "ink") - pure 0 - | Except.error rc => pure rc + let relevantModules := [p.positionalArg! "module" |>.as! String |> String.toName] + let res ← lakeSetup + match res with + | Except.ok ws => + let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules + IO.println "Outputting HTML" + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputResults baseConfig doc ws (p.hasFlag "ink") + pure 0 + | Except.error rc => pure rc def runIndexCmd (_p : Parsed) : IO UInt32 := do let hierarchy ← Hierarchy.fromDirectory Output.basePath @@ -29,22 +28,22 @@ def runIndexCmd (_p : Parsed) : IO UInt32 := do htmlOutputIndex baseConfig pure 0 -def runDocGenCmd (p : Parsed) : IO UInt32 := do - let modules : List String := p.variableArgsAs! String |>.toList - if modules.length == 0 then - throw <| IO.userError "No modules provided." - - let res ← lakeSetup modules +def runGenCoreCmd (_p : Parsed) : IO UInt32 := do + let res ← lakeSetup match res with | Except.ok ws => - IO.println s!"Loading modules from: {←searchPathRef.get}" - let modules := modules.map String.toName - let (doc, hierarchy) ← load (.loadAll modules) + let (doc, hierarchy) ← loadCore IO.println "Outputting HTML" - htmlOutput doc hierarchy ws (p.hasFlag "ink") + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputResults baseConfig doc ws (ink := False) pure 0 | Except.error rc => pure rc +def runDocGenCmd (_p : Parsed) : IO UInt32 := do + IO.println "You most likely want to use me via Lake now, check my README on Github on how to:" + IO.println "https://github.com/leanprover/doc-gen4" + return 0 + def singleCmd := `[Cli| single VIA runSingleCmd; "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated." @@ -63,19 +62,19 @@ def indexCmd := `[Cli| ...topLevelModule : String; "The top level modules this documentation will be for." ] +def genCoreCmd := `[Cli| + genCore VIA runGenCoreCmd; + "Generate documentation for the core Lean modules: Init, Std and Lean since they are not Lake projects" +] + def docGenCmd : Cmd := `[Cli| - "doc-gen4" VIA runDocGenCmd; ["0.0.1"] + "doc-gen4" VIA runDocGenCmd; ["0.1.0"] "A documentation generator for Lean 4." - FLAGS: - ink; "Render the files with LeanInk in addition" - - ARGS: - ...modules : String; "The modules to generate the HTML for." - SUBCOMMANDS: singleCmd; - indexCmd + indexCmd; + genCoreCmd ] def main (args : List String) : IO UInt32 := diff --git a/README.md b/README.md index 75c7ba1..73b2015 100644 --- a/README.md +++ b/README.md @@ -2,48 +2,15 @@ Document Generator for Lean 4 ## Usage -You can call `doc-gen4` from the top of a Lake project like this: -```sh -$ /path/to/doc-gen4 Module +`doc-gen4` is the easiest to use via its custom Lake facet, in order +to do this you have to add it to your `lakefile.lean` like this: ``` - -where `Module` is one or more of the top level modules you want to document. -The tool will then proceed to compile the project using lake (if that hasn't happened yet), -analyze it and put the result in `./build/doc`. - -You can optionally provide the path to a `LeanInk` binary using the `--ink` flag which will make -the tool produce `Alectryon` style rendered output along the usual documentation. - -You could e.g. host the files locally with the built-in Python webserver: -```sh -$ cd build/doc && python -m http.server +meta if get_config? env = some "dev" then -- dev is so not everyone has to build it +require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" ``` - -### Multi stage -You can also use `doc-gen4` in multiple separate stages to generate the whole documentation. -For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and itself: -- `Init` -- `Std` -- `Lean` -- `Mathlib` - -The first build stage is to run doc-gen for all modules separately: - -1. `doc-gen4 single Init` -2. `doc-gen4 single Std` -3. `doc-gen4 single Lean` -4. `doc-gen4 single Mathlib` - -Note that you can also just make a call to submodules so `Mathlib.Algebra` -will work standalone as well. Furthermore one can use the `--ink` flag -here to also generate LeanInk documentation in addition. - -The second and last stage is the index one which zips up some -information relevant for the search: -```sh -$ doc-gen4 index Mathlib +Then you can generate documentation for an entire library using: ``` -Now `build/doc` should contain the same files with the same context as if one had run -``` -$ doc-gen4 Mathlib +lake -Kenv=dev build Test:docs ``` +If you have multiple libraries you want to generate documentation for +the recommended way right now is to run it for each library. diff --git a/lakefile.lean b/lakefile.lean index a9aeedb..8d172dc 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -26,3 +26,92 @@ require lake from git require leanInk from git "https://github.com/hargonix/LeanInk" @ "doc-gen" + +module_facet docs (mod) : FilePath := do + let some docGen4 ← findLeanExe? `«doc-gen4» + | error "no doc-gen4 executable configuration found in workspace" + let exeJob ← docGen4.exe.fetch + let modJob ← mod.leanBin.fetch + let buildDir := (← getWorkspace).root.buildDir + let docFile := mod.filePath (buildDir / "doc") "html" + exeJob.bindAsync fun exeFile exeTrace => do + modJob.bindSync fun _ modTrace => do + let depTrace := exeTrace.mix modTrace + let trace ← buildFileUnlessUpToDate docFile depTrace do + logInfo s!"Documenting module: {mod.name}" + proc { + cmd := exeFile.toString + args := #["single", mod.name.toString, "--ink"] + env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] + } + return (docFile, trace) + +-- TODO: technically speaking this facet does not show all file dependencies +target coreDocs : FilePath := do + let some docGen4 ← findLeanExe? `«doc-gen4» + | error "no doc-gen4 executable configuration found in workspace" + let exeJob ← docGen4.exe.fetch + let basePath := (←getWorkspace).root.buildDir / "doc" + let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp" + exeJob.bindSync fun exeFile exeTrace => do + let trace ← buildFileUnlessUpToDate dataFile exeTrace do + logInfo "Documenting Lean core: Init, Std, Lean" + proc { + cmd := exeFile.toString + args := #["genCore"] + env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] + } + return (dataFile, trace) + +library_facet docs (lib) : FilePath := do + let some docGen4Pkg ← findPackage? `«doc-gen4» + | error "no doc-gen4 package found in workspace" + let some docGen4 := docGen4Pkg.findLeanExe? `«doc-gen4» + | error "no doc-gen4 executable configuration found in workspace" + let exeJob ← docGen4.exe.fetch + + -- XXX: Workaround remove later + let coreJob ← if h : docGen4Pkg.name = _package.name then + have : Fact (docGen4Pkg.name = _package.name) := Fact.mk h + let job := fetch <| docGen4Pkg.target `coreDocs + job + else + error "wrong package" + + let moduleJobs ← BuildJob.mixArray (α := FilePath) <| ← lib.recBuildLocalModules #[`docs] + -- Shared with DocGen4.Output + let basePath := (←getWorkspace).root.buildDir / "doc" + let dataFile := basePath / "declarations" / "declaration-data.bmp" + let staticFiles := #[ + basePath / "style.css", + basePath / "declaration-data.js", + basePath / "nav.js", + basePath / "how-about.js", + basePath / "search.js", + basePath / "mathjax-config.js", + basePath / "instances.js", + basePath / "importedBy.js", + basePath / "index.html", + basePath / "404.html", + basePath / "navbar.html", + basePath / "find" / "index.html", + basePath / "find" / "find.js", + basePath / "src" / "alectryon.css", + basePath / "src" / "alectryon.js", + basePath / "src" / "docutils_basic.css", + basePath / "src" / "pygments.css" + ] + coreJob.bindAsync fun _ coreInputTrace => do + exeJob.bindAsync fun exeFile exeTrace => do + moduleJobs.bindSync fun _ inputTrace => do + let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace] + let trace ← buildFileUnlessUpToDate dataFile depTrace do + logInfo "Documentation indexing" + proc { + cmd := exeFile.toString + args := #["index"] + } + let traces ← staticFiles.mapM computeTrace + let indexTrace := mixTraceArray traces + + return (dataFile, trace.mix indexTrace) From d43b23ec9ff69ff45956fa6ddb2a6eb2c4fbd699 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 11 Aug 2022 23:19:31 +0200 Subject: [PATCH 7/8] fix: Dont linkify unknown names --- DocGen4/Output/Base.lean | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2add29d..53ef5bc 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -212,17 +212,21 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do | TaggedText.tag a t => match a.info.val.info with | Info.ofTermInfo i => - match i.expr.consumeMData with - | Expr.const name _ => - match t with - | TaggedText.text t => - let (front, t, back) := splitWhitespaces <| Html.escape t - let elem := {t} - pure #[Html.text front, elem, Html.text back] - | _ => - -- TODO: Is this ever reachable? - pure #[[←infoFormatToHtml t]] - | _ => + let cleanExpr := i.expr.consumeMData + if let Expr.const name _ := cleanExpr then + -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM + -- find a better solution + if (←getResult).name2ModIdx.contains name then + match t with + | TaggedText.text t => + let (front, t, back) := splitWhitespaces <| Html.escape t + let elem := {t} + pure #[Html.text front, elem, Html.text back] + | _ => + pure #[[←infoFormatToHtml t]] + else + pure #[[←infoFormatToHtml t]] + else pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] From de1405afd3c0ac316c54a9e55b14d8dbd6c52392 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 11 Aug 2022 23:49:30 +0200 Subject: [PATCH 8/8] fix: pipeline for new build --- .github/workflows/build.yml | 8 -------- deploy_docs.sh | 2 +- 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index ba1ad2f..8f961d9 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -25,14 +25,6 @@ jobs: run: | lake build - - name: Checkout and compile LeanInk - run: | - cd ../ - git clone https://github.com/hargonix/LeanInk - cd LeanInk - git checkout doc-gen - lake build - - name: Checkout and compile mathlib4 run: | cd ../ diff --git a/deploy_docs.sh b/deploy_docs.sh index 3eec3b8..6042795 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -23,7 +23,7 @@ fi # generate the docs cd $1 -../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib +lake -Kenv=dev build Mathlib:docs --verbose if [ "$3" = "true" ]; then cd ..