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: