119 lines
4.0 KiB
Plaintext
119 lines
4.0 KiB
Plaintext
import Lake
|
|
open System Lake DSL
|
|
|
|
package «doc-gen4»
|
|
|
|
lean_lib DocGen4
|
|
|
|
@[default_target]
|
|
lean_exe «doc-gen4» {
|
|
root := `Main
|
|
supportInterpreter := true
|
|
}
|
|
|
|
require CMark from git
|
|
"https://github.com/xubaiw/CMark.lean" @ "main"
|
|
|
|
require UnicodeBasic from git
|
|
"https://github.com/fgdorais/lean4-unicode-basic" @ "main"
|
|
|
|
require Cli from git
|
|
"https://github.com/mhuisi/lean4-cli" @ "nightly"
|
|
|
|
require lake from git
|
|
"https://github.com/leanprover/lake" @ "master"
|
|
|
|
require leanInk from git
|
|
"https://github.com/hargonix/LeanInk" @ "doc-gen"
|
|
|
|
module_facet docs (mod) : FilePath := do
|
|
let some docGen4 ← findLeanExe? `«doc-gen4»
|
|
| error "no doc-gen4 executable configuration found in workspace"
|
|
let exeJob ← docGen4.exe.fetch
|
|
let modJob ← mod.leanBin.fetch
|
|
let buildDir := (← getWorkspace).root.buildDir
|
|
let docFile := mod.filePath (buildDir / "doc") "html"
|
|
exeJob.bindAsync fun exeFile exeTrace => do
|
|
modJob.bindSync fun _ modTrace => do
|
|
let depTrace := exeTrace.mix modTrace
|
|
let trace ← buildFileUnlessUpToDate docFile depTrace do
|
|
logInfo s!"Documenting module: {mod.name}"
|
|
proc {
|
|
cmd := exeFile.toString
|
|
args := #["single", mod.name.toString, "--ink"]
|
|
env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
|
|
}
|
|
return (docFile, trace)
|
|
|
|
-- TODO: technically speaking this facet does not show all file dependencies
|
|
target coreDocs : FilePath := do
|
|
let some docGen4 ← findLeanExe? `«doc-gen4»
|
|
| error "no doc-gen4 executable configuration found in workspace"
|
|
let exeJob ← docGen4.exe.fetch
|
|
let basePath := (←getWorkspace).root.buildDir / "doc"
|
|
let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
|
|
exeJob.bindSync fun exeFile exeTrace => do
|
|
let trace ← buildFileUnlessUpToDate dataFile exeTrace do
|
|
logInfo "Documenting Lean core: Init and Lean"
|
|
proc {
|
|
cmd := exeFile.toString
|
|
args := #["genCore"]
|
|
env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
|
|
}
|
|
return (dataFile, trace)
|
|
|
|
library_facet docs (lib) : FilePath := do
|
|
let some docGen4Pkg ← findPackage? `«doc-gen4»
|
|
| error "no doc-gen4 package found in workspace"
|
|
let some docGen4 := docGen4Pkg.findLeanExe? `«doc-gen4»
|
|
| error "no doc-gen4 executable configuration found in workspace"
|
|
let exeJob ← docGen4.exe.fetch
|
|
|
|
-- XXX: Workaround remove later
|
|
let coreJob ← if h : docGen4Pkg.name = _package.name then
|
|
have : Fact (docGen4Pkg.name = _package.name) := Fact.mk h
|
|
let job := fetch <| docGen4Pkg.target `coreDocs
|
|
job
|
|
else
|
|
error "wrong package"
|
|
|
|
let mods ← lib.modules.fetch
|
|
let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
|
|
-- Shared with DocGen4.Output
|
|
let basePath := (←getWorkspace).root.buildDir / "doc"
|
|
let dataFile := basePath / "declarations" / "declaration-data.bmp"
|
|
let staticFiles := #[
|
|
basePath / "style.css",
|
|
basePath / "declaration-data.js",
|
|
basePath / "nav.js",
|
|
basePath / "how-about.js",
|
|
basePath / "search.js",
|
|
basePath / "mathjax-config.js",
|
|
basePath / "instances.js",
|
|
basePath / "importedBy.js",
|
|
basePath / "index.html",
|
|
basePath / "404.html",
|
|
basePath / "navbar.html",
|
|
basePath / "search.html",
|
|
basePath / "find" / "index.html",
|
|
basePath / "find" / "find.js",
|
|
basePath / "src" / "alectryon.css",
|
|
basePath / "src" / "alectryon.js",
|
|
basePath / "src" / "docutils_basic.css",
|
|
basePath / "src" / "pygments.css"
|
|
]
|
|
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 := #["index"]
|
|
}
|
|
let traces ← staticFiles.mapM computeTrace
|
|
let indexTrace := mixTraceArray traces
|
|
|
|
return (dataFile, trace.mix indexTrace)
|