diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ae4037e..4e3f32d 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -127,17 +127,21 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do htmlOutputSetup baseConfig - let mut index : JsonIndex := { } - for entry in ←System.FilePath.readDir declarationsBasePath do + let mut index : JsonIndex := {} + let mut headerIndex : JsonHeaderIndex := {} + for entry in ← System.FilePath.readDir declarationsBasePath do if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then let fileContent ← FS.readFile entry.path let .ok jsonContent := Json.parse fileContent | unreachable! let .ok (module : JsonModule) := fromJson? jsonContent | unreachable! index := index.addModule module |>.run baseConfig + headerIndex := headerIndex.addModule module 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 /-- The main entrypoint for outputting the documentation HTML based on an diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 95e84a0..8e17726 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -1,20 +1,27 @@ import Lean import DocGen4.Process import DocGen4.Output.Base +import DocGen4.Output.Module import Lean.Data.RBMap namespace DocGen4.Output open Lean -structure JsonDeclaration where +structure JsonDeclarationInfo where name : String kind : String doc : String docLink : String sourceLink : String + line : Nat deriving FromJson, ToJson +structure JsonDeclaration where + info : JsonDeclarationInfo + header : String +deriving FromJson, ToJson + structure JsonInstance where name : String className : String @@ -28,20 +35,26 @@ structure JsonModule where imports : Array String deriving FromJson, ToJson +structure JsonHeaderIndex where + headers : List (String × String) := [] + structure JsonIndex where - declarations : List (String × JsonDeclaration) := [] - instances : HashMap String (Array String) := .empty + declarations : List (String × JsonDeclarationInfo) := [] + instances : HashMap String (RBTree String Ord.compare) := .empty importedBy : HashMap String (Array String) := .empty modules : List (String × String) := [] - instancesFor : HashMap String (Array String) := .empty + instancesFor : HashMap String (RBTree String Ord.compare) := .empty + +instance : ToJson JsonHeaderIndex where + toJson idx := Json.mkObj <| idx.headers.map (fun (k, v) => (k, toJson v)) instance : ToJson JsonIndex where toJson idx := Id.run do let jsonDecls := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v)) - let jsonInstances := Json.mkObj <| idx.instances.toList.map (fun (k, v) => (k, toJson v)) + let jsonInstances := Json.mkObj <| idx.instances.toList.map (fun (k, v) => (k, toJson v.toArray)) let jsonImportedBy := Json.mkObj <| idx.importedBy.toList.map (fun (k, v) => (k, toJson v)) let jsonModules := Json.mkObj <| idx.modules.map (fun (k, v) => (k, toJson v)) - let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (fun (k, v) => (k, toJson v)) + let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (fun (k, v) => (k, toJson v.toArray)) let finalJson := Json.mkObj [ ("declarations", jsonDecls), ("instances", jsonInstances), @@ -51,22 +64,26 @@ instance : ToJson JsonIndex where ] return finalJson +def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex := + let merge idx decl := { idx with headers := (decl.info.name, decl.header) :: idx.headers } + module.declarations.foldl merge index + def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do let mut index := index let newModule := (module.name, ← moduleNameToHtmlLink (String.toName module.name)) - let newDecls := module.declarations.map (fun d => (d.name, d)) + let newDecls := module.declarations.map (fun d => (d.info.name, d.info)) index := { index with modules := newModule :: index.modules declarations := newDecls ++ index.declarations } -- TODO: In theory one could sort instances and imports by name and batch the writes for inst in module.instances do - let mut insts := index.instances.findD inst.className #[] - insts := insts.push inst.name + let mut insts := index.instances.findD inst.className {} + insts := insts.insert inst.name index := { index with instances := index.instances.insert inst.className insts } for typeName in inst.typeNames do - let mut instsFor := index.instancesFor.findD typeName #[] - instsFor := instsFor.push inst.name + let mut instsFor := index.instancesFor.findD typeName {} + instsFor := instsFor.insert inst.name index := { index with instancesFor := index.instancesFor.insert typeName instsFor } for imp in module.imports do @@ -81,7 +98,10 @@ def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclarat let doc := info.getDocString.getD "" let docLink ← declNameToLink info.getName let sourceLink ← getSourceUrl module info.getDeclarationRange - return { name, kind, doc, docLink, sourceLink } + let line := info.getDeclarationRange.pos.line + let header := (← docInfoHeader info).toString + let info := { name, kind, doc, docLink, sourceLink, line } + return { info, header } def Process.Module.toJson (module : Process.Module) : HtmlM Json := do let mut jsonDecls := [] diff --git a/lake-manifest.json b/lake-manifest.json index 397ff7d..7b844fb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -19,6 +19,12 @@ "rev": "a2ced44b7e5e30c2a6b84b420e1bbdd8d6d8e079", "name": "lake", "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "subDir?": null, + "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32", + "name": "lean4-unicode-basic", + "inputRev?": "main"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, @@ -28,7 +34,7 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "fa6fd7946dd9c980955a878da81134c4f6e01e9e", + "rev": "280a9f50ed49fc27396d06d438fde63691818268", "name": "mathlib", "inputRev?": "master"}}, {"git": @@ -40,7 +46,7 @@ {"git": {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "354432d437fb37738ed93ac6988669d78a870ed0", + "rev": "d13a9666e6f430b940ef8d092f1219e964b52a09", "name": "aesop", "inputRev?": "master"}}, {"git": @@ -49,21 +55,9 @@ "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", "name": "leanInk", "inputRev?": "doc-gen"}}, - {"git": - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "subDir?": null, - "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32", - "name": "UnicodeBasic", - "inputRev?": "main"}}, {"git": {"url": "https://github.com/leanprover/std4.git", "subDir?": null, - "rev": "7601c54efadd70b688a163f5dcc11ae0ccdf7621", - "name": "std4", - "inputRev?": "main"}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "e3c2be331da9ddeef7f82ca363f072a68d7210b3", + "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8", "name": "std", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index df0c97e..f3cc1b6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,7 +14,7 @@ require Cli from git require CMark from git "https://github.com/xubaiw/CMark.lean" @ "main" -require UnicodeBasic from git +require «lean4-unicode-basic» from git "https://github.com/fgdorais/lean4-unicode-basic" @ "main" require lake from git @@ -26,7 +26,7 @@ require leanInk from git require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master" -require std4 from git +require std from git "https://github.com/leanprover/std4.git" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 0e8c38f..e4b4851 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-07-30 \ No newline at end of file +leanprover/lean4:nightly-2023-08-03 \ No newline at end of file