Skip to content

Commit

Permalink
perf: reduce size of .lake/build/doc
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Jul 5, 2024
1 parent 5cf3352 commit 7aa0886
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 7 deletions.
6 changes: 4 additions & 2 deletions DocGen4/Output.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions DocGen4/Output/Base.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
6 changes: 3 additions & 3 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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",
Expand Down

0 comments on commit 7aa0886

Please sign in to comment.