From 89974630e470c695619a51a7416d4ba96ae0f1d5 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Fri, 8 Nov 2024 22:26:54 -0500 Subject: [PATCH] feat: use lake build path for output --- DocGen4/Output.lean | 55 +++++++++++++++++----------------- DocGen4/Output/Base.lean | 13 ++++---- DocGen4/Output/References.lean | 32 ++++++++++---------- Main.lean | 50 ++++++++++++++++++++++++------- lakefile.lean | 24 ++++++++------- 5 files changed, 105 insertions(+), 69 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index e61632a4..bc1593e7 100644 --- a/DocGen4/Output.lean +++ b/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,13 +37,13 @@ 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 @@ -51,7 +51,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do 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,7 +73,7 @@ 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 := #[ @@ -81,12 +81,12 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do ("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,13 +153,13 @@ 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! @@ -166,7 +167,7 @@ def headerDataOutput : IO Unit := do 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 @@ -174,8 +175,8 @@ def headerDataOutput : IO Unit := do 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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 3c0ab732..fea8bfee 100644 --- a/DocGen4/Output/Base.lean +++ b/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. -/ diff --git a/DocGen4/Output/References.lean b/DocGen4/Output/References.lean index b9b0ead4..dbc522c0 100644 --- a/DocGen4/Output/References.lean +++ b/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 diff --git a/Main.lean b/Main.lean index 778a25b0..912ea6c6 100644 --- a/Main.lean +++ b/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,18 +52,21 @@ 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 @@ -59,6 +74,9 @@ 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| diff --git a/lakefile.lean b/lakefile.lean index 26ebbf16..b315f58e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -125,18 +125,19 @@ def getSrcUri (mod : Module) : IO String := do target bibPrepass : FilePath := do let exeJob ← «doc-gen4».fetch - let dataPath := (← getWorkspace).root.buildDir / "doc-data" + let buildDir := (←getWorkspace).root.buildDir + let dataPath := buildDir / "doc-data" let inputJsonFile := (← getWorkspace).root.srcDir / "docs" / "references.json" let inputBibFile := (← getWorkspace).root.srcDir / "docs" / "references.bib" let outputFile := dataPath / "references.json" let tryJson : JobM (Array String × BuildTrace) := do let inputTrace ← mixTrace (BuildTrace.ofHash (.ofString "json")) <$> computeTrace inputJsonFile - pure (#["--json", inputJsonFile.toString], inputTrace) + pure (#["--build", buildDir.toString, "--json", inputJsonFile.toString], inputTrace) let tryBib : JobM (Array String × BuildTrace) := do let inputTrace ← mixTrace (BuildTrace.ofHash (.ofString "bib")) <$> computeTrace inputBibFile - pure (#[inputBibFile.toString], inputTrace) + pure (#["--build", buildDir.toString, inputBibFile.toString], inputTrace) let tryBibFailed : JobM (Array String × BuildTrace) := do - pure (#["--none"], .nil) + pure (#["--build", buildDir.toString, "--none"], .nil) exeJob.bindSync fun exeFile exeTrace => do let (args, inputTrace) ← tryJson <|> tryBib <|> tryBibFailed let depTrace := exeTrace.mix inputTrace @@ -166,7 +167,7 @@ module_facet docs (mod) : FilePath := do let trace ← buildFileUnlessUpToDate docFile depTrace do proc { cmd := exeFile.toString - args := #["single", mod.name.toString, srcUri] + args := #["single", "--build", buildDir.toString, mod.name.toString, srcUri] env := ← getAugmentedEnv } return (docFile, trace) @@ -177,13 +178,14 @@ target coreDocs : FilePath := do let bibPrepassJob ← bibPrepass.fetch let dataPath := (← getWorkspace).root.buildDir / "doc-data" let dataFile := dataPath / "declaration-data-Lean.bmp" + let buildDir := (←getWorkspace).root.buildDir bibPrepassJob.bindAsync fun _ bibPrepassTrace => do exeJob.bindSync fun exeFile exeTrace => do let depTrace := mixTraceArray #[exeTrace, bibPrepassTrace] let trace ← buildFileUnlessUpToDate dataFile depTrace do proc { cmd := exeFile.toString - args := #["genCore"] + args := #["genCore", "--build", buildDir.toString] env := ← getAugmentedEnv } return (dataFile, trace) @@ -194,7 +196,8 @@ 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 buildDir := (←getWorkspace).root.buildDir + let basePath := buildDir / "doc" let dataFile := basePath / "declarations" / "declaration-data.bmp" let staticFiles := #[ basePath / "style.css", @@ -224,7 +227,7 @@ library_facet docs (lib) : FilePath := do logInfo "Documentation indexing" proc { cmd := exeFile.toString - args := #["index"] + args := #["index", "--build", buildDir.toString] } let traces ← staticFiles.mapM computeTrace let indexTrace := mixTraceArray traces @@ -237,7 +240,8 @@ library_facet docsHeader (lib) : FilePath := do let coreJob ← coreDocs.fetch let exeJob ← «doc-gen4».fetch -- Shared with DocGen4.Output - let basePath := (← getWorkspace).root.buildDir / "doc" + let buildDir := (←getWorkspace).root.buildDir + let basePath := buildDir / "doc" let dataFile := basePath / "declarations" / "header-data.bmp" coreJob.bindAsync fun _ coreInputTrace => do exeJob.bindAsync fun exeFile exeTrace => do @@ -247,6 +251,6 @@ library_facet docsHeader (lib) : FilePath := do logInfo "Documentation indexing" proc { cmd := exeFile.toString - args := #["headerData"] + args := #["headerData", "--build", buildDir.toString] } return (dataFile, trace)