feat: use lake build path for output

DocGen4/Output.lean

@@ -21,9 +21,9 @@ namespace DocGen4
 
 open Lean IO System Output Process
 
-def collectBackrefs : IO (Array BackrefItem) := do
+def collectBackrefs (buildDir : System.FilePath) : IO (Array BackrefItem) := do
   let mut backrefs : Array BackrefItem := #[]
-  for entry in ← System.FilePath.readDir declarationsBasePath do
+  for entry in ← System.FilePath.readDir (declarationsBasePath buildDir) do
     if entry.fileName.startsWith "backrefs-" && entry.fileName.endsWith ".json" then
       let fileContent ← FS.readFile entry.path
       match Json.parse fileContent with
@@ -37,21 +37,21 @@ def collectBackrefs : IO (Array BackrefItem) := do
   return backrefs
 
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
-  let findBasePath := basePath / "find"
+  let findBasePath (buildDir : System.FilePath) := basePath buildDir / "find"
 
   -- Base structure
-  FS.createDirAll basePath
-  FS.createDirAll findBasePath
-  FS.createDirAll srcBasePath
-  FS.createDirAll declarationsBasePath
+  FS.createDirAll <| basePath config.buildDir
+  FS.createDirAll <| findBasePath config.buildDir
+  FS.createDirAll <| srcBasePath config.buildDir
+  FS.createDirAll <| declarationsBasePath config.buildDir
 
   -- All the doc-gen static stuff
   let indexHtml := ReaderT.run index config |>.toString
   let notFoundHtml := ReaderT.run notFound config |>.toString
   let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
   let navbarHtml := ReaderT.run navbar config |>.toString
   let searchHtml := ReaderT.run search config |>.toString
-  let referencesHtml := ReaderT.run (references (← collectBackrefs)) config |>.toString
+  let referencesHtml := ReaderT.run (references (← collectBackrefs config.buildDir)) config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
     ("favicon.svg", faviconSvg),
@@ -73,20 +73,20 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("references.html", referencesHtml)
   ]
   for (fileName, content) in docGenStatic do
-    FS.writeFile (basePath / fileName) content
+    FS.writeFile (basePath config.buildDir / fileName) content
 
   let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString
   let findStatic := #[
     ("index.html", findHtml),
     ("find.js", findJs)
   ]
   for (fileName, content) in findStatic do
-    FS.writeFile (findBasePath / fileName) content
+    FS.writeFile (findBasePath config.buildDir / fileName) content
 
-def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
+def htmlOutputDeclarationDatas (buildDir : System.FilePath) (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") (toJson jsonDecls).compress
+    FS.writeFile (declarationsBasePath buildDir / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
 
 def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) : IO Unit := do
   let config : SiteContext := {
@@ -95,14 +95,14 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
     refsMap := .ofList (baseConfig.refs.map fun x => (x.citekey, x)).toList
   }
 
-  FS.createDirAll basePath
-  FS.createDirAll declarationsBasePath
+  FS.createDirAll <| basePath baseConfig.buildDir
+  FS.createDirAll <| declarationsBasePath baseConfig.buildDir
 
-  discard <| htmlOutputDeclarationDatas result |>.run {} config baseConfig
+  discard <| htmlOutputDeclarationDatas baseConfig.buildDir result |>.run {} config baseConfig
 
   for (modName, module) in result.moduleInfo.toArray do
-    let fileDir := moduleNameToDirectory basePath modName
-    let filePath := moduleNameToFile basePath modName
+    let fileDir := moduleNameToDirectory (basePath baseConfig.buildDir) modName
+    let filePath := moduleNameToFile (basePath baseConfig.buildDir) modName
     -- path: 'basePath/module/components/till/last.html'
     -- The last component is the file name, so we drop it from the depth to root.
     let baseConfig := { baseConfig with
@@ -114,10 +114,10 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
       throw <| IO.userError s!"There are errors when generating '{filePath}': {cfg.errors}"
     FS.createDirAll fileDir
     FS.writeFile filePath moduleHtml.toString
-    FS.writeFile (declarationsBasePath / s!"backrefs-{module.name}.json") (toString (toJson cfg.backrefs))
+    FS.writeFile (declarationsBasePath baseConfig.buildDir / s!"backrefs-{module.name}.json") (toString (toJson cfg.backrefs))
 
-def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
-  let contents ← FS.readFile (declarationsBasePath / "references.json") <|> (pure "[]")
+def getSimpleBaseContext (buildDir : System.FilePath) (hierarchy : Hierarchy) : IO SiteBaseContext := do
+  let contents ← FS.readFile (declarationsBasePath buildDir / "references.json") <|> (pure "[]")
   match Json.parse contents with
   | .error err =>
     throw <| IO.userError s!"Failed to parse 'references.json': {err}"
@@ -127,6 +127,7 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
       throw <| IO.userError s!"Failed to parse 'references.json': {err}"
     | .ok (refs : Array BibItem) =>
       return {
+        buildDir := buildDir
         depthToRoot := 0
         currentName := none
         hierarchy := hierarchy
@@ -137,7 +138,7 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig
 
   let mut index : JsonIndex := {}
-  for entry in ← System.FilePath.readDir declarationsBasePath do
+  for entry in ← System.FilePath.readDir (declarationsBasePath baseConfig.buildDir) do
     if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
       let fileContent ← FS.readFile entry.path
       match Json.parse fileContent with
@@ -152,30 +153,30 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
 
   let finalJson := toJson index
   -- The root JSON for find
-  let declarationDir := basePath / "declarations"
+  let declarationDir := basePath  baseConfig.buildDir / "declarations"
   FS.createDirAll declarationDir
   FS.writeFile (declarationDir / "declaration-data.bmp") finalJson.compress
 
-def headerDataOutput : IO Unit := do
+def headerDataOutput (buildDir : System.FilePath) : IO Unit := do
   let mut headerIndex : JsonHeaderIndex := {}
-  for entry in ← System.FilePath.readDir declarationsBasePath do
+  for entry in ← System.FilePath.readDir (declarationsBasePath buildDir) 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"
+  let declarationDir := basePath buildDir / "declarations"
   FS.createDirAll declarationDir
   FS.writeFile (declarationDir / "header-data.bmp") finalHeaderJson.compress
 
 /--
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (sourceUrl? : Option String) : IO Unit := do
-  let baseConfig ← getSimpleBaseContext hierarchy
+def htmlOutput (buildDir : System.FilePath) (result : AnalyzerResult) (hierarchy : Hierarchy) (sourceUrl? : Option String) : IO Unit := do
+  let baseConfig ← getSimpleBaseContext buildDir hierarchy
   htmlOutputResults baseConfig result sourceUrl?
   htmlOutputIndex baseConfig
 

DocGen4/Output/Base.lean

@@ -11,11 +11,9 @@ namespace DocGen4.Output
 open scoped DocGen4.Jsx
 open Lean System Widget Elab Process
 
-
-def lakeBuildDir := FilePath.mk "." / ".lake" / "build"
-def basePath := lakeBuildDir / "doc"
-def srcBasePath := basePath / "src"
-def declarationsBasePath := lakeBuildDir / "doc-data"
+def basePath (buildDir : System.FilePath) := buildDir / "doc"
+def srcBasePath (buildDir : System.FilePath) := basePath buildDir / "src"
+def declarationsBasePath (buildDir : System.FilePath) := buildDir / "doc-data"
 
 /-- The structure representing a processed bibitem. -/
 structure BibItem where
@@ -48,6 +46,11 @@ The context used in the `BaseHtmlM` monad for HTML templating.
 -/
 structure SiteBaseContext where
 
+  /--
+  The build directory (provided by lake).
+  -/
+  buildDir : System.FilePath
+
   /--
   The module hierarchy as a tree structure.
   -/

DocGen4/Output/References.lean

@@ -25,39 +25,39 @@ namespace DocGen4
 
 /-- Preprocess (using the user provided `process` function)
 and save the bib file to the output path. -/
-def preprocessBibFile (contents : String) (process : String → IO (Array BibItem)) : IO Unit := do
+def preprocessBibFile (buildDir : System.FilePath) (contents : String) (process : String → IO (Array BibItem)) : IO Unit := do
   -- create directories
-  IO.FS.createDirAll basePath
-  IO.FS.createDirAll declarationsBasePath
+  IO.FS.createDirAll <| basePath buildDir
+  IO.FS.createDirAll <| declarationsBasePath buildDir
   -- save the contents to "references.bib" and erase "references.json"
-  IO.FS.writeFile (basePath / "references.bib") contents
-  IO.FS.writeFile (declarationsBasePath / "references.json") "[]"
+  IO.FS.writeFile (basePath buildDir / "references.bib") contents
+  IO.FS.writeFile (declarationsBasePath buildDir / "references.json") "[]"
   -- if contents is empty, just do nothing
   if contents.trim.isEmpty then
     return
   -- run the user provided process function
   let items ← process contents
   -- save the result to "references.json"
-  IO.FS.writeFile (declarationsBasePath / "references.json") (toString (toJson items))
+  IO.FS.writeFile (declarationsBasePath buildDir / "references.json") (toString (toJson items))
 
 /-- Save the bib json to the output path. -/
-def preprocessBibJson (contents : String) : IO Unit := do
+def preprocessBibJson (buildDir : System.FilePath) (contents : String) : IO Unit := do
   -- create directories
-  IO.FS.createDirAll basePath
-  IO.FS.createDirAll declarationsBasePath
+  IO.FS.createDirAll <| basePath buildDir
+  IO.FS.createDirAll <| declarationsBasePath buildDir
   -- erase "references.bib" (since we can't recover it from json)
   -- and save the contents to "references.json"
-  IO.FS.writeFile (basePath / "references.bib") ""
-  IO.FS.writeFile (declarationsBasePath / "references.json") contents
+  IO.FS.writeFile (basePath buildDir / "references.bib") ""
+  IO.FS.writeFile (declarationsBasePath buildDir / "references.json") contents
 
 /-- Erase the contents of bib file in the output path. -/
-def disableBibFile : IO Unit := do
+def disableBibFile (buildDir : System.FilePath) : IO Unit := do
   -- create directories
-  IO.FS.createDirAll basePath
-  IO.FS.createDirAll declarationsBasePath
+  IO.FS.createDirAll <| basePath buildDir
+  IO.FS.createDirAll <| declarationsBasePath buildDir
   -- erase files
-  IO.FS.writeFile (basePath / "references.bib") ""
-  IO.FS.writeFile (declarationsBasePath / "references.json") "[]"
+  IO.FS.writeFile (basePath buildDir / "references.bib") ""
+  IO.FS.writeFile (declarationsBasePath buildDir / "references.json") "[]"
 
 namespace Output
 

Main.lean

@@ -10,27 +10,39 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
     throw <| IO.userError "No topLevelModules provided."
   return topLevelModules
 
-def runHeaderDataCmd (_p : Parsed) : IO UInt32 := do
-  headerDataOutput
+def runHeaderDataCmd (p : Parsed) : IO UInt32 := do
+  let buildDir := match p.flag? "build" with
+    | some dir => dir.as! String
+    | none => ".lake/build"
+  headerDataOutput buildDir
   return 0
 
 def runSingleCmd (p : Parsed) : IO UInt32 := do
+  let buildDir := match p.flag? "build" with
+    | some dir => dir.as! String
+    | none => ".lake/build"
   let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
   let sourceUri := p.positionalArg! "sourceUri" |>.as! String
   let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
-  let baseConfig ← getSimpleBaseContext hierarchy
+  let baseConfig ← getSimpleBaseContext buildDir hierarchy
   htmlOutputResults baseConfig doc (some sourceUri)
   return 0
 
-def runIndexCmd (_p : Parsed) : IO UInt32 := do
-  let hierarchy ← Hierarchy.fromDirectory Output.basePath
-  let baseConfig ← getSimpleBaseContext hierarchy
+def runIndexCmd (p : Parsed) : IO UInt32 := do
+  let buildDir := match p.flag? "build" with
+    | some dir => dir.as! String
+    | none => ".lake/build"
+  let hierarchy ← Hierarchy.fromDirectory (Output.basePath buildDir)
+  let baseConfig ← getSimpleBaseContext buildDir hierarchy
   htmlOutputIndex baseConfig
   return 0
 
-def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
+def runGenCoreCmd (p : Parsed) : IO UInt32 := do
+  let buildDir := match p.flag? "build" with
+    | some dir => dir.as! String
+    | none => ".lake/build"
   let (doc, hierarchy) ← loadCore
-  let baseConfig ← getSimpleBaseContext hierarchy
+  let baseConfig ← getSimpleBaseContext buildDir hierarchy
   htmlOutputResults baseConfig doc none
   return 0
 
@@ -40,25 +52,31 @@ def runDocGenCmd (_p : Parsed) : IO UInt32 := do
   return 0
 
 def runBibPrepassCmd (p : Parsed) : IO UInt32 := do
+  let buildDir := match p.flag? "build" with
+    | some dir => dir.as! String
+    | none => ".lake/build"
   if p.hasFlag "none" then
     IO.println "INFO: reference page disabled"
-    disableBibFile
+    disableBibFile buildDir
   else
     match p.variableArgsAs! String with
     | #[source] =>
       let contents ← IO.FS.readFile source
       if p.hasFlag "json" then
         IO.println "INFO: 'references.json' will be copied to the output path; there will be no 'references.bib'"
-        preprocessBibJson contents
+        preprocessBibJson buildDir contents
       else
-        preprocessBibFile contents Bibtex.process
+        preprocessBibFile buildDir contents Bibtex.process
     | _ => throw <| IO.userError "there should be exactly one source file"
   return 0
 
 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."
 
+  FLAGS:
+    b, build : String; "Build directory."
+
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
     sourceUri : String; "The sourceUri as computed by the Lake facet"
@@ -67,11 +85,17 @@ def singleCmd := `[Cli|
 def indexCmd := `[Cli|
   index VIA runIndexCmd;
   "Index the documentation that has been generated by single."
+
+  FLAGS:
+    b, build : String; "Build directory."
 ]
 
 def genCoreCmd := `[Cli|
   genCore VIA runGenCoreCmd;
   "Generate documentation for the core Lean modules: Init, Lean, Lake and Std since they are not Lake projects"
+
+  FLAGS:
+    b, build : String; "Build directory."
 ]
 
 def bibPrepassCmd := `[Cli|
@@ -81,6 +105,7 @@ def bibPrepassCmd := `[Cli|
   FLAGS:
     n, none; "Disable bibliography in this project."
     j, json; "The input file is '.json' which contains an array of objects with 4 fields: 'citekey', 'tag', 'html' and 'plaintext'."
+    b, build : String; "Build directory."
 
   ARGS:
     ...source : String; "The bibliography file. We only support one file for input. Should be '.bib' or '.json' according to flags."
@@ -89,6 +114,9 @@ def bibPrepassCmd := `[Cli|
 def headerDataCmd := `[Cli|
   headerData VIA runHeaderDataCmd;
   "Produce `header-data.bmp`, this allows embedding of doc-gen declarations into other pages and more."
+
+  FLAGS:
+    b, build : String; "Build directory."
 ]
 
 def docGenCmd : Cmd := `[Cli|