diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 52c605b..d158b4c 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -117,8 +117,10 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do 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 + FS.writeFile (declarationDir / "header-data.bmp") finalHeaderJson.compress /-- The main entrypoint for outputting the documentation HTML based on an diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 1ea53c9..9f2e01c 100644 --- a/DocGen4/Output/Base.lean +++ b/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 context used in the `BaseHtmlM` monad for HTML templating. diff --git a/lakefile.lean b/lakefile.lean index 5b7c669..d259a4f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -144,8 +144,8 @@ module_facet docs (mod) : FilePath := do -- TODO: technically speaking this target does not show all file dependencies target coreDocs : FilePath := do let exeJob ← «doc-gen4».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" exeJob.bindSync fun exeFile exeTrace => do let trace ← buildFileUnlessUpToDate dataFile exeTrace do proc { @@ -161,7 +161,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",