feat: split out header data generation

DocGen4/Output.lean

@@ -105,21 +105,31 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig
 
   let mut index : JsonIndex := {}
-  let mut headerIndex : JsonHeaderIndex := {}
   for entry in ← System.FilePath.readDir declarationsBasePath do
     if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
       let fileContent ← FS.readFile entry.path
       let .ok jsonContent := Json.parse fileContent | unreachable!
       let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
       index := index.addModule module |>.run baseConfig
-      headerIndex := headerIndex.addModule module
 
   let finalJson := toJson index
-  let finalHeaderJson := toJson headerIndex
   -- The root JSON for find
   let declarationDir := basePath / "declarations"
   FS.createDirAll declarationDir
   FS.writeFile (declarationDir / "declaration-data.bmp") finalJson.compress
+
+def headerDataOutput : IO Unit := do
+  let mut headerIndex : JsonHeaderIndex := {}
+  for entry in ← System.FilePath.readDir declarationsBasePath do
+    if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
+      let fileContent ← FS.readFile entry.path
+      let .ok jsonContent := Json.parse fileContent | unreachable!
+      let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
+      headerIndex := headerIndex.addModule module
+
+  let finalHeaderJson := toJson headerIndex
+  let declarationDir := basePath / "declarations"
+  FS.createDirAll declarationDir
   FS.writeFile (declarationDir / "header-data.bmp") finalHeaderJson.compress
 
 /--

Main.lean

@@ -10,6 +10,10 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
     throw <| IO.userError "No topLevelModules provided."
   return topLevelModules
 
+def runHeaderDataCmd (_p : Parsed) : IO UInt32 := do
+  headerDataOutput
+  return 0
+
 def runSingleCmd (p : Parsed) : IO UInt32 := do
   let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
   let sourceUri := p.positionalArg! "sourceUri" |>.as! String
@@ -47,23 +51,27 @@ def singleCmd := `[Cli|
 def indexCmd := `[Cli|
   index VIA runIndexCmd;
   "Index the documentation that has been generated by single."
-  ARGS:
-    ...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 and Lean since they are not Lake projects"
 ]
 
+def headerDataCmd := `[Cli|
+  headerData VIA runHeaderDataCmd;
+  "Produce `header-data.bmp`, this allows embedding of doc-gen declarations into other pages and more."
+]
+
 def docGenCmd : Cmd := `[Cli|
   "doc-gen4" VIA runDocGenCmd; ["0.1.0"]
   "A documentation generator for Lean 4."
 
   SUBCOMMANDS:
     singleCmd;
     indexCmd;
-    genCoreCmd
+    genCoreCmd;
+    headerDataCmd
 ]
 
 def main (args : List String) : IO UInt32 :=

lakefile.lean

@@ -197,3 +197,23 @@ library_facet docs (lib) : FilePath := do
         let indexTrace := mixTraceArray traces
 
         return (dataFile, trace.mix indexTrace)
+
+library_facet docsHeader (lib) : FilePath := do
+  let mods ← lib.modules.fetch
+  let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
+  let coreJob ← coreDocs.fetch
+  let exeJob ← «doc-gen4».fetch
+  -- Shared with DocGen4.Output
+  let basePath := (← getWorkspace).root.buildDir / "doc"
+  let dataFile := basePath / "declarations" / "header-data.bmp"
+  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 := #["headerData"]
+          }
+        return (dataFile, trace)