From 71af8db54b6b246077940d76a6f7c7423cebd6fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 21:05:19 +0200 Subject: [PATCH 01/14] feat: Declaration data into separate directory --- DocGen4/Output.lean | 11 +++++++---- static/declaration-data.js | 4 ++-- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index c690c04..0776f61 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -21,14 +21,16 @@ open Lean IO System Output Process Std def basePath := FilePath.mk "." / "build" / "doc" def srcBasePath := basePath / "src" +def declarationsBasePath := basePath / "declarations" def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do let findBasePath := basePath / "find" -- Base structure FS.createDirAll basePath - FS.createDirAll (basePath / "find") + FS.createDirAll findBasePath FS.createDirAll srcBasePath + FS.createDirAll declarationsBasePath -- All the doc-gen static stuff let indexHtml := ReaderT.run index config |>.toString @@ -86,6 +88,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( } FS.createDirAll basePath + FS.createDirAll declarationsBasePath -- Rendering the entire lean compiler takes time.... --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath @@ -99,7 +102,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls) for (topLevelMod, decls) in declMap.toList do - FS.writeFile (basePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress + FS.writeFile (declarationsBasePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress for (modName, module) in result.moduleInfo.toArray do let fileDir := moduleNameToDirectory basePath modName @@ -133,13 +136,13 @@ def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do htmlOutputSetup baseConfig let mut topLevelModules := #[] - for entry in ←System.FilePath.readDir basePath do + for entry in ←System.FilePath.readDir declarationsBasePath do if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then let module := entry.fileName.drop "declaration-data-".length |>.dropRight ".bmp".length topLevelModules := topLevelModules.push (Json.str module) -- The root JSON for find - FS.writeFile (basePath / "declaration-data.bmp") (Json.arr topLevelModules).compress + FS.writeFile (declarationsBasePath / "declaration-data.bmp") (Json.arr topLevelModules).compress /-- The main entrypoint for outputting the documentation HTML based on an diff --git a/static/declaration-data.js b/static/declaration-data.js index 0c284dc..6a74bee 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -10,7 +10,7 @@ const CACHE_DB_KEY = "DECLARATIONS_KEY"; async function fetchModuleData(module) { const moduleDataUrl = new URL( - `${SITE_ROOT}declaration-data-${module}.bmp`, + `${SITE_ROOT}/declarations/declaration-data-${module}.bmp`, window.location ); const moduleData = await fetch(moduleDataUrl); @@ -53,7 +53,7 @@ export class DeclarationDataCenter { static async init() { if (!DeclarationDataCenter.singleton) { const dataListUrl = new URL( - `${SITE_ROOT}declaration-data.bmp`, + `${SITE_ROOT}/declarations/declaration-data.bmp`, window.location ); From 80cf5bc96fc17c68622b43283fe625c6dbce0bb2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 21:12:15 +0200 Subject: [PATCH 02/14] feat: Renamed finalize to index --- DocGen4/Output.lean | 4 ++-- Main.lean | 12 ++++++------ README.md | 4 ++-- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 0776f61..7636deb 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -132,7 +132,7 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext := hierarchy } -def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do +def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do htmlOutputSetup baseConfig let mut topLevelModules := #[] @@ -151,7 +151,7 @@ The main entrypoint for outputting the documentation HTML based on an def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do let baseConfig := getSimpleBaseContext hierarchy htmlOutputResults baseConfig result ws inkPath - htmlOutputFinalize baseConfig + htmlOutputIndex baseConfig end DocGen4 diff --git a/Main.lean b/Main.lean index 2ea998e..a1bf44f 100644 --- a/Main.lean +++ b/Main.lean @@ -35,7 +35,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do pure 0 | Except.error rc => pure rc -def runFinalizeCmd (p : Parsed) : IO UInt32 := do +def runIndexCmd (p : Parsed) : IO UInt32 := do let topLevelModules ← getTopLevelModules p let res ← lakeSetup topLevelModules match res with @@ -43,7 +43,7 @@ def runFinalizeCmd (p : Parsed) : IO UInt32 := do let modules := topLevelModules.map Name.mkSimple let hierarchy ← loadInit modules let baseConfig := getSimpleBaseContext hierarchy - htmlOutputFinalize baseConfig + htmlOutputIndex baseConfig pure 0 | Except.error rc => pure rc pure 0 @@ -76,9 +76,9 @@ def singleCmd := `[Cli| ...topLevelModules : String; "The top level modules this documentation will be for." ] -def finalizeCmd := `[Cli| - finalize VIA runFinalizeCmd; - "Finalize the documentation that has been generated by single." +def indexCmd := `[Cli| + index VIA runIndexCmd; + "Index the documentation that has been generated by single." ARGS: ...topLevelModule : String; "The top level modules this documentation will be for." ] @@ -95,7 +95,7 @@ def docGenCmd : Cmd := `[Cli| SUBCOMMANDS: singleCmd; - finalizeCmd + indexCmd ] def main (args : List String) : IO UInt32 := diff --git a/README.md b/README.md index f7c2146..38248c0 100644 --- a/README.md +++ b/README.md @@ -38,10 +38,10 @@ generate documentation for its first argument module. Furthermore one can use the `--ink` flag here to also generate LeanInk documentation in addition. -The second and last stage is the finalize one which zips up some +The second and last stage is the index one which zips up some information relevant for the search: ```sh -$ doc-gen4 finalize Mathlib +$ doc-gen4 index Mathlib ``` Now `build/doc` should contain the same files with the same context as if one had run ``` From 80cb92eb94686319f2aa60b3d06969bcd3d9cd44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 22:06:26 +0200 Subject: [PATCH 03/14] feat: Use iframe for navbar to move it into the finalize stage --- DocGen4/Output.lean | 4 +++- DocGen4/Output/Base.lean | 25 +++++++++++++++++++++++++ DocGen4/Output/Navbar.lean | 35 ++++++++++++++++++++--------------- DocGen4/Output/Template.lean | 28 ++++------------------------ static/style.css | 5 +++++ 5 files changed, 57 insertions(+), 40 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 7636deb..9c40844 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -35,6 +35,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do -- All the doc-gen static stuff let indexHtml := ReaderT.run index config |>.toString let notFoundHtml := ReaderT.run notFound config |>.toString + let navbarHtml := ReaderT.run navbar config |>.toString let docGenStatic := #[ ("style.css", styleCss), ("declaration-data.js", declarationDataCenterJs), @@ -43,7 +44,8 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do ("search.js", searchJs), ("mathjax-config.js", mathjaxConfigJs), ("index.html", indexHtml), - ("404.html", notFoundHtml) + ("404.html", notFoundHtml), + ("navbar.html", navbarHtml) ] for (fileName, content) in docGenStatic do FS.writeFile (basePath / fileName) content diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index daf980d..0e6ea5a 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -215,4 +215,29 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] +def baseHtmlHead (title : String) : BaseHtmlM Html := do + pure + + {title} + + + + + + + + + + + + + + + + + + + + + end DocGen4.Output diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index bf70e34..9f71f45 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -57,21 +57,26 @@ The main entry point to rendering the navbar on the left hand side. -/ def navbar : BaseHtmlM Html := do pure - + + {←baseHtmlHead "Navbar"} + + + + end Output end DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 49aa9f5..632e4e9 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -17,29 +17,7 @@ The HTML template used for all pages. def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do pure - - - {title} - - - - - - - - - - - - - - - - - - - - + {←baseHtmlHead title} @@ -57,7 +35,9 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d [site] - {←navbar} + diff --git a/static/style.css b/static/style.css index fbf8614..4b35ab2 100644 --- a/static/style.css +++ b/static/style.css @@ -257,6 +257,11 @@ nav { text-indent: -2ex; padding-left: 2ex; } +.navframe { + height: 100%; + width: 100%; +} + .internal_nav .imports { margin-bottom: 1rem; } From eea23d332aee5a3b6536c7b60e479fd9931c64ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 22:43:33 +0200 Subject: [PATCH 04/14] feat: Fully separated builds --- DocGen4/Output.lean | 15 ++++++--------- DocGen4/Process/Analyze.lean | 15 ++++++--------- Main.lean | 13 +++++-------- README.md | 17 +++++++---------- 4 files changed, 24 insertions(+), 36 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 9c40844..b030ad3 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -82,6 +82,11 @@ def Process.Module.toJson (module : Module) : HtmlM (Array Json) := do jsonDecls := jsonDecls.push json pure jsonDecls +def htmlOutputDeclarationDatas (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") (Json.arr jsonDecls).compress + def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do let config : SiteContext := { result := result, @@ -96,15 +101,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath - let mut declMap := HashMap.empty - for (_, mod) in result.moduleInfo.toArray do - let topLevelMod := mod.name.getRoot - let jsonDecls := Module.toJson mod |>.run config baseConfig - let currentModDecls := declMap.findD topLevelMod #[] - declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls) - - for (topLevelMod, decls) in declMap.toList do - FS.writeFile (declarationsBasePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress + discard $ htmlOutputDeclarationDatas result |>.run config baseConfig for (modName, module) in result.moduleInfo.toArray do let fileDir := moduleNameToDirectory basePath modName diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index 3ce5b95..ee12e93 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -92,21 +92,18 @@ def getRelevantModules (imports : List Name) : MetaM (HashSet Name) := do let env ← getEnv let mut relevant := .empty for module in env.header.moduleNames do - if module.getRoot ∈ imports then - relevant := relevant.insert module + for import in imports do + if Name.isPrefixOf import module then + relevant := relevant.insert module pure relevant inductive AnalyzeTask where | loadAll (load : List Name) : AnalyzeTask -| loadAllLimitAnalysis (load : List Name) (analyze : List Name) : AnalyzeTask +| loadAllLimitAnalysis (analyze : List Name) : AnalyzeTask def AnalyzeTask.getLoad : AnalyzeTask → List Name | loadAll load => load -| loadAllLimitAnalysis load _ => load - -def AnalyzeTask.getAnalyze : AnalyzeTask → List Name -| loadAll load => load -| loadAllLimitAnalysis _ analysis => analysis +| loadAllLimitAnalysis load => load def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module) := do let env ← getEnv @@ -136,7 +133,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do let env ← getEnv let relevantModules ← match task with | .loadAll _ => pure $ HashSet.fromArray env.header.moduleNames - | .loadAllLimitAnalysis _ analysis => getRelevantModules analysis + | .loadAllLimitAnalysis analysis => getRelevantModules analysis let allModules := env.header.moduleNames let mut res ← getAllModuleDocs relevantModules.toArray diff --git a/Main.lean b/Main.lean index a1bf44f..2005c19 100644 --- a/Main.lean +++ b/Main.lean @@ -21,14 +21,12 @@ def getTopLevelModules (p : Parsed) : IO (List String) := do pure topLevelModules def runSingleCmd (p : Parsed) : IO UInt32 := do - let topLevelModules ← getTopLevelModules p let relevantModules := [p.positionalArg! "module" |>.as! String] - let res ← lakeSetup (relevantModules ++ topLevelModules) + let res ← lakeSetup (relevantModules) match res with | Except.ok ws => - let relevantModules := relevantModules.map Name.mkSimple - let topLevelModules := topLevelModules.map Name.mkSimple - let (doc, hierarchy) ← load (.loadAllLimitAnalysis topLevelModules relevantModules) + let relevantModules := relevantModules.map String.toName + let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules) IO.println "Outputting HTML" let baseConfig := getSimpleBaseContext hierarchy htmlOutputResults baseConfig doc ws (←findLeanInk? p) @@ -40,7 +38,7 @@ def runIndexCmd (p : Parsed) : IO UInt32 := do let res ← lakeSetup topLevelModules match res with | Except.ok _ => - let modules := topLevelModules.map Name.mkSimple + let modules := topLevelModules.map String.toName let hierarchy ← loadInit modules let baseConfig := getSimpleBaseContext hierarchy htmlOutputIndex baseConfig @@ -57,7 +55,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do match res with | Except.ok ws => IO.println s!"Loading modules from: {←searchPathRef.get}" - let modules := modules.map Name.mkSimple + let modules := modules.map String.toName let (doc, hierarchy) ← load (.loadAll modules) IO.println "Outputting HTML" htmlOutput doc hierarchy ws (←findLeanInk? p) @@ -73,7 +71,6 @@ def singleCmd := `[Cli| ARGS: module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules." - ...topLevelModules : String; "The top level modules this documentation will be for." ] def indexCmd := `[Cli| diff --git a/README.md b/README.md index 38248c0..d4d135d 100644 --- a/README.md +++ b/README.md @@ -27,16 +27,13 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i - `Lean` - `Mathlib` The first build stage is to run doc-gen for all modules separately: -1. `doc-gen4 single Init Mathlib` -2. `doc-gen4 single Std Mathlib` -3. `doc-gen4 single Lean Mathlib` -4. `doc-gen4 single Mathlib Mathlib` -We have to pass the `Mathlib` top level module on each invocation here so -it can generate the navbar on the left hand side properly, it will only -generate documentation for its first argument module. - -Furthermore one can use the `--ink` flag here to also generate LeanInk -documentation in addition. +1. `doc-gen4 single Init` +2. `doc-gen4 single Std` +3. `doc-gen4 single Lean` +4. `doc-gen4 single Mathlib` +Note that you can also just make a call to submodules so `Mathlib.Algebra` +will work standalone as well. Furthermore one can use the `--ink` flag +here to also generate LeanInk documentation in addition. The second and last stage is the index one which zips up some information relevant for the search: From 0cff3d7cda28818334b8769260de77970ccfcb32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 23:01:15 +0200 Subject: [PATCH 05/14] fix: Javascript errors in the navbar --- DocGen4/Output/Base.lean | 33 +++++++++------------------------ DocGen4/Output/Navbar.lean | 7 ++++++- DocGen4/Output/Template.lean | 17 ++++++++++++++--- 3 files changed, 29 insertions(+), 28 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 0e6ea5a..976b711 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -215,29 +215,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do pure #[[←infoFormatToHtml t]] | _ => pure #[[←infoFormatToHtml t]] -def baseHtmlHead (title : String) : BaseHtmlM Html := do - pure - - {title} - - - - - - - - - - - - - - - - - - - - +def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do + pure #[ + , + , + , + , + , + + ] end DocGen4.Output diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 9f71f45..eea77f0 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -58,7 +58,12 @@ The main entry point to rendering the navbar on the left hand side. def navbar : BaseHtmlM Html := do pure - {←baseHtmlHead "Navbar"} + + [←baseHtmlHeadDeclarations] + + + +