feat: merge init and finalize

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
 

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
 ]

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:
+The first build stage is to run doc-gen for all modules separately:
-```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:
 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
+We have to pass the `Mathlib` top level module on each invocation here so
-will only generate documentation for its first argument module. Furthermore
+it can generate the navbar on the left hand side properly, it will only
-one can use the `--ink` flag here to also generate LeanInk documentation in addition.
+generate documentation for its first argument module.
-The last stage is the finalize one which zips up some information relevant for
+
-the search:
+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
 ```