diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 476b308..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-json - lake build - - name: Checkout and compile mathlib4 run: | cd ../ diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 60d1d31..60f7a86 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 @@ -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]
@@ -197,27 +202,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 } + 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..dcd31aa 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 -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 docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do + 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 + IO.FS.writeFile srcPath srcHtml.toString + pure 0 + +def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do + let ctx ← readThe SiteContext + let baseCtx ← readThe SiteBaseContext + let outputFn := (docGenOutput · |>.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/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/DocGen4/Output.lean b/DocGen4/Output.lean index d79b8b9..d92d9d6 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" @@ -76,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 @@ -97,21 +93,20 @@ 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 - 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' -- 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 := { @@ -139,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/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index e8c1ee3..53ef5bc 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -11,6 +11,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. -/ @@ -61,6 +65,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. -/ @@ -202,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]] diff --git a/Main.lean b/Main.lean index 00606b7..e098d13 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 @@ -21,46 +11,45 @@ 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 (←findLeanInk? p) - 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 basePath + let hierarchy ← Hierarchy.fromDirectory Output.basePath let baseConfig := getSimpleBaseContext hierarchy 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 (←findLeanInk? p) + 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." 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." @@ -73,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 : String; "Path to a LeanInk binary to use for rendering the Lean sources." - - 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/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 .. diff --git a/lakefile.lean b/lakefile.lean index af7ebaf..e73161f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -25,4 +25,93 @@ require lake from git "https://github.com/leanprover/lake" @ "master" require leanInk from git - "https://github.com/hargonix/LeanInk" @ "doc-gen-json" + "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) \ No newline at end of file diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index 83376d9..85cbf43 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": "eed51a5e121233c3d15fb14642048a9bd3e00695", + "rev": "439303af06465824588a486f5f9c023ca69979f3", "name": "leanInk"}, {"url": "https://github.com/xubaiw/Unicode.lean", "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29",