diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 11763a5..c690c04 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -84,8 +84,9 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( sourceLinker := ←sourceLinker ws leanInkEnabled := inkPath.isSome } - let basePath := FilePath.mk "." / "build" / "doc" - let srcBasePath := basePath / "src" + + FS.createDirAll basePath + -- 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 @@ -128,7 +129,9 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext := hierarchy } -def finalizeDeclarationData : IO Unit := do +def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do + htmlOutputSetup baseConfig + let mut topLevelModules := #[] for entry in ←System.FilePath.readDir basePath do if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then @@ -144,9 +147,8 @@ The main entrypoint for outputting the documentation HTML based on an -/ def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do let baseConfig := getSimpleBaseContext hierarchy - htmlOutputSetup baseConfig htmlOutputResults baseConfig result ws inkPath - finalizeDeclarationData + htmlOutputFinalize baseConfig end DocGen4 diff --git a/Main.lean b/Main.lean index 4cbdfbc..e4f7bd0 100644 --- a/Main.lean +++ b/Main.lean @@ -48,7 +48,16 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do | Except.error rc => pure rc def runFinalizeCmd (p : Parsed) : IO UInt32 := do - finalizeDeclarationData + let topLevelModules ← getTopLevelModules p + let res ← lakeSetup topLevelModules + match res with + | Except.ok _ => + let modules := topLevelModules.map Name.mkSimple + let hierarchy ← loadInit modules + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputFinalize baseConfig + pure 0 + | Except.error rc => pure rc pure 0 def runDocGenCmd (p : Parsed) : IO UInt32 := do @@ -67,13 +76,6 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do pure 0 | Except.error rc => pure rc -def initCmd := `[Cli| - init VIA runInitCmd; - "Generate the initial directory structure and static files." - ARGS: - ...topLevelModule : String; "The top level modules this documentation will be for." -] - 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." @@ -89,6 +91,8 @@ def singleCmd := `[Cli| def finalizeCmd := `[Cli| finalize VIA runFinalizeCmd; "Finalize the documentation that has been generated by single." + ARGS: + ...topLevelModule : String; "The top level modules this documentation will be for." ] def docGenCmd : Cmd := `[Cli| @@ -102,7 +106,6 @@ def docGenCmd : Cmd := `[Cli| ...modules : String; "The modules to generate the HTML for." SUBCOMMANDS: - initCmd; singleCmd; finalizeCmd ] diff --git a/README.md b/README.md index 758f1bd..f7c2146 100644 --- a/README.md +++ b/README.md @@ -26,24 +26,22 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i - `Std` - `Lean` - `Mathlib` -The first stage in the build is: -```sh -$ doc-gen4 init Mathlib -``` -We already have to pass the `Mathlib` top level module here so it can generate the -navbar on the left hand side properly in the index and 404 HTML pages. -Next we can run the actual build stages: +The first build stage is to run doc-gen for all modules separately: 1. `doc-gen4 single Init Mathlib` 2. `doc-gen4 single Std Mathlib` 3. `doc-gen4 single Lean Mathlib` 4. `doc-gen4 single Mathlib Mathlib` -We have to pass `Mathlib` here again for the same reason, the single command -will only generate documentation for its first argument module. Furthermore -one can use the `--ink` flag here to also generate LeanInk documentation in addition. -The last stage is the finalize one which zips up some information relevant for -the search: +We have to pass the `Mathlib` top level module on each invocation here so +it can generate the navbar on the left hand side properly, it will only +generate documentation for its first argument module. + +Furthermore one can use the `--ink` flag here to also generate LeanInk +documentation in addition. + +The second and last stage is the finalize one which zips up some +information relevant for the search: ```sh -$ doc-gen4 finalize +$ doc-gen4 finalize Mathlib ``` Now `build/doc` should contain the same files with the same context as if one had run ```