feat: Fully separated builds

DocGen4/Output.lean

@@ -82,6 +82,11 @@ def Process.Module.toJson (module : Module) : HtmlM (Array Json) := do
       jsonDecls := jsonDecls.push json
     pure jsonDecls
 
+def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
+  for (_, mod) in result.moduleInfo.toArray do
+    let jsonDecls ← Module.toJson mod
+    FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (Json.arr jsonDecls).compress
+
 def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
   let config : SiteContext := {
     result := result,
@@ -96,15 +101,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
   --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
   let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
 
-  let mut declMap := HashMap.empty
+  discard $ htmlOutputDeclarationDatas result |>.run config baseConfig
-  for (_, mod) in result.moduleInfo.toArray do
-    let topLevelMod := mod.name.getRoot
-    let jsonDecls := Module.toJson mod |>.run config baseConfig
-    let currentModDecls := declMap.findD topLevelMod #[]
-    declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls)
-
-  for (topLevelMod, decls) in declMap.toList do
-    FS.writeFile (declarationsBasePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress
 
   for (modName, module) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath modName

DocGen4/Process/Analyze.lean

@@ -92,21 +92,18 @@ def getRelevantModules (imports : List Name) : MetaM (HashSet Name) := do
   let env ← getEnv
   let mut relevant := .empty
   for module in env.header.moduleNames do
-    if module.getRoot ∈ imports then
+    for import in imports do
-      relevant := relevant.insert module
+      if Name.isPrefixOf import module then
+        relevant := relevant.insert module
   pure relevant
 
 inductive AnalyzeTask where
 | loadAll (load : List Name) : AnalyzeTask
-| loadAllLimitAnalysis (load : List Name) (analyze : List Name) : AnalyzeTask
+| loadAllLimitAnalysis (analyze : List Name) : AnalyzeTask
 
 def AnalyzeTask.getLoad : AnalyzeTask → List Name
 | loadAll load => load
-| loadAllLimitAnalysis load _ => load
+| loadAllLimitAnalysis load => load
-
-def AnalyzeTask.getAnalyze : AnalyzeTask → List Name
-| loadAll load => load
-| loadAllLimitAnalysis _ analysis => analysis
 
 def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module) := do
   let env ← getEnv
@@ -136,7 +133,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
   let env ← getEnv
   let relevantModules ← match task with
     | .loadAll _ => pure $ HashSet.fromArray env.header.moduleNames
-    | .loadAllLimitAnalysis _ analysis => getRelevantModules analysis
+    | .loadAllLimitAnalysis analysis => getRelevantModules analysis
   let allModules := env.header.moduleNames
 
   let mut res ← getAllModuleDocs relevantModules.toArray

Main.lean

@@ -21,14 +21,12 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
   pure topLevelModules
 
 def runSingleCmd (p : Parsed) : IO UInt32 := do
-    let topLevelModules ← getTopLevelModules p
     let relevantModules := [p.positionalArg! "module" |>.as! String]
-    let res ← lakeSetup (relevantModules ++ topLevelModules)
+    let res ← lakeSetup (relevantModules)
     match res with
     | Except.ok ws =>
-      let relevantModules := relevantModules.map Name.mkSimple
+      let relevantModules := relevantModules.map String.toName
-      let topLevelModules := topLevelModules.map Name.mkSimple
+      let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules)
-      let (doc, hierarchy) ← load (.loadAllLimitAnalysis topLevelModules relevantModules)
       IO.println "Outputting HTML"
       let baseConfig := getSimpleBaseContext hierarchy
       htmlOutputResults baseConfig doc ws (←findLeanInk? p)
@@ -40,7 +38,7 @@ def runIndexCmd (p : Parsed) : IO UInt32 := do
   let res ← lakeSetup topLevelModules
   match res with
   | Except.ok _ =>
-    let modules := topLevelModules.map Name.mkSimple
+    let modules := topLevelModules.map String.toName
     let hierarchy ← loadInit modules
     let baseConfig := getSimpleBaseContext hierarchy
     htmlOutputIndex baseConfig
@@ -57,7 +55,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
   match res with
   | Except.ok ws =>
     IO.println s!"Loading modules from: {←searchPathRef.get}"
-    let modules := modules.map Name.mkSimple
+    let modules := modules.map String.toName
     let (doc, hierarchy) ← load (.loadAll modules)
     IO.println "Outputting HTML"
     htmlOutput doc hierarchy ws (←findLeanInk? p)
@@ -73,7 +71,6 @@ def singleCmd := `[Cli|
 
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
-    ...topLevelModules : String; "The top level modules this documentation will be for."
 ]
 
 def indexCmd := `[Cli|

README.md

@@ -27,16 +27,13 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i
 - `Lean`
 - `Mathlib`
 The first build stage is to run doc-gen for all modules separately:
-1. `doc-gen4 single Init Mathlib`
+1. `doc-gen4 single Init`
-2. `doc-gen4 single Std Mathlib`
+2. `doc-gen4 single Std`
-3. `doc-gen4 single Lean Mathlib`
+3. `doc-gen4 single Lean`
-4. `doc-gen4 single Mathlib Mathlib`
+4. `doc-gen4 single Mathlib`
-We have to pass the `Mathlib` top level module on each invocation here so
+Note that you can also just make a call to submodules so `Mathlib.Algebra`
-it can generate the navbar on the left hand side properly, it will only
+will work standalone as well. Furthermore one can use the `--ink` flag
-generate documentation for its first argument module.
+here to also generate LeanInk documentation in addition.
-
-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: