Merge branch 'main' into acmepjz_bib

# Conflicts:
#	DocGen4/Output.lean
#	Main.lean
#	lakefile.lean

DocGen4/Output.lean

@@ -138,7 +138,6 @@ 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
@@ -151,13 +150,26 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
           throw <| IO.userError s!"failed to parse file '{entry.path}': {err}"
         | .ok (module : JsonModule) =>
           index := index.addModule module |>.run baseConfig
-          headerIndex := headerIndex.addModule module
 
   let finalJson := toJson index
-  let finalHeaderJson := toJson headerIndex
   -- The root JSON for find
-  FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
-  FS.writeFile (declarationsBasePath / "header-data.bmp") finalHeaderJson.compress
+  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
 
 /--
 The main entrypoint for outputting the documentation HTML based on an

DocGen4/Output/Base.lean

@@ -11,9 +11,11 @@ namespace DocGen4.Output
 open scoped DocGen4.Jsx
 open Lean System Widget Elab Process
 
-def basePath := FilePath.mk "." / ".lake" / "build" / "doc"
+
+def lakeBuildDir := FilePath.mk "." / ".lake" / "build"
+def basePath := lakeBuildDir / "doc"
 def srcBasePath := basePath / "src"
-def declarationsBasePath := basePath / "declarations"
+def declarationsBasePath := lakeBuildDir / "doc-data"
 
 /-- The structure representing a processed bibitem. -/
 structure BibItem where

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
@@ -66,8 +70,6 @@ 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|
@@ -88,6 +90,11 @@ def bibPrepassCmd := `[Cli|
     ...source : String; "The bibliography file. We only support one file for input. Should be '.bib' or '.json' according to flags."
 ]
 
+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."
@@ -96,7 +103,8 @@ def docGenCmd : Cmd := `[Cli|
     singleCmd;
     indexCmd;
     genCoreCmd;
-    bibPrepassCmd
+    bibPrepassCmd;
+    headerDataCmd
 ]
 
 def main (args : List String) : IO UInt32 :=

lakefile.lean

@@ -175,8 +175,8 @@ module_facet docs (mod) : FilePath := do
 target coreDocs : FilePath := do
   let exeJob ← «doc-gen4».fetch
   let bibPrepassJob ← bibPrepass.fetch
-  let basePath := (←getWorkspace).root.buildDir / "doc"
-  let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
+  let dataPath := (← getWorkspace).root.buildDir / "doc-data"
+  let dataFile := dataPath / "declaration-data-Lean.bmp"
   bibPrepassJob.bindAsync fun _ bibPrepassTrace => do
     exeJob.bindSync fun exeFile exeTrace => do
       let depTrace := mixTraceArray #[exeTrace, bibPrepassTrace]
@@ -194,7 +194,7 @@ library_facet docs (lib) : FilePath := do
   let coreJob ← coreDocs.fetch
   let exeJob ← «doc-gen4».fetch
   -- Shared with DocGen4.Output
-  let basePath := (←getWorkspace).root.buildDir / "doc"
+  let basePath := (← getWorkspace).root.buildDir / "doc"
   let dataFile := basePath / "declarations" / "declaration-data.bmp"
   let staticFiles := #[
     basePath / "style.css",
@@ -230,3 +230,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)