diff --git a/.gitignore b/.gitignore
index 8560c43..3ec510d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
/build
-/lean_packages
+/lean_packages/*
!/lean_packages/manifest.json
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index c690c04..db1d156 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -12,6 +12,7 @@ import DocGen4.Output.Module
import DocGen4.Output.NotFound
import DocGen4.Output.Find
import DocGen4.Output.SourceLinker
+import DocGen4.Output.ToJson
import DocGen4.LeanInk.Output
import Std.Data.HashMap
@@ -21,18 +22,21 @@ 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
let notFoundHtml := ReaderT.run notFound config |>.toString
+ let navbarHtml := ReaderT.run navbar config |>.toString
let docGenStatic := #[
("style.css", styleCss),
("declaration-data.js", declarationDataCenterJs),
@@ -40,8 +44,11 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
("how-about.js", howAboutJs),
("search.js", searchJs),
("mathjax-config.js", mathjaxConfigJs),
+ ("instances.js", instancesJs),
+ ("importedBy.js", importedByJs),
("index.html", indexHtml),
- ("404.html", notFoundHtml)
+ ("404.html", notFoundHtml),
+ ("navbar.html", navbarHtml)
]
for (fileName, content) in docGenStatic do
FS.writeFile (basePath / fileName) content
@@ -64,19 +71,10 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
for (fileName, content) in alectryonStatic do
FS.writeFile (srcBasePath / fileName) content
-def DocInfo.toJson (module : Name) (info : DocInfo) : HtmlM Json := do
- let name := info.getName.toString
- let doc := info.getDocString.getD ""
- let docLink ← declNameToLink info.getName
- let sourceLink ← getSourceUrl module info.getDeclarationRange
- pure $ Json.mkObj [("name", name), ("doc", doc), ("docLink", docLink), ("sourceLink", sourceLink)]
-
-def Process.Module.toJson (module : Module) : HtmlM (Array Json) := do
- let mut jsonDecls := #[]
- for decl in filterMapDocInfo module.members do
- let json ← DocInfo.toJson module.name decl
- 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") (toJson jsonDecls).compress
def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
let config : SiteContext := {
@@ -86,20 +84,13 @@ 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
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 (basePath / 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
@@ -129,17 +120,39 @@ 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 := #[]
- for entry in ←System.FilePath.readDir basePath do
+ let mut allDecls : List (String × Json) := []
+ let mut allInstances : HashMap String (Array String) := .empty
+ let mut importedBy : HashMap String (Array String) := .empty
+ let mut allModules : List (String × Json) := []
+ 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)
+ let fileContent ← FS.readFile entry.path
+ let .ok jsonContent := Json.parse fileContent | unreachable!
+ let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
+ allModules := (module.name, Json.str <| moduleNameToLink (String.toName module.name) |>.run baseConfig) :: allModules
+ allDecls := (module.declarations.map (λ d => (d.name, toJson d))) ++ allDecls
+ for inst in module.instances do
+ let mut insts := allInstances.findD inst.className #[]
+ insts := insts.push inst.name
+ allInstances := allInstances.insert inst.className insts
+ for imp in module.imports do
+ let mut impBy := importedBy.findD imp #[]
+ impBy := impBy.push module.name
+ importedBy := importedBy.insert imp impBy
+ let postProcessInstances := allInstances.toList.map (λ(k, v) => (k, toJson v))
+ let postProcessImportedBy := importedBy.toList.map (λ(k, v) => (k, toJson v))
+ let finalJson := Json.mkObj [
+ ("declarations", Json.mkObj allDecls),
+ ("instances", Json.mkObj postProcessInstances),
+ ("importedBy", Json.mkObj postProcessImportedBy),
+ ("modules", Json.mkObj allModules)
+ ]
-- The root JSON for find
- FS.writeFile (basePath / "declaration-data.bmp") (Json.arr topLevelModules).compress
+ FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
/--
The main entrypoint for outputting the documentation HTML based on an
@@ -148,7 +161,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/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index daf980d..c68d218 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -132,6 +132,8 @@ are used in documentation generation, notably JS and CSS ones.
def navJs : String := include_str "../../static/nav.js"
def howAboutJs : String := include_str "../../static/how-about.js"
def searchJs : String := include_str "../../static/search.js"
+ def instancesJs : String := include_str "../../static/instances.js"
+ def importedByJs : String := include_str "../../static/importedBy.js"
def findJs : String := include_str "../../static/find/find.js"
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
@@ -215,4 +217,14 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
pure #[[←infoFormatToHtml t]]
| _ => pure #[[←infoFormatToHtml t]]
+def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
+ pure #[
+ ,
+ ,
+ ,
+ ,
+ ,
+
+ ]
+
end DocGen4.Output
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
index 5ca853e..3ce2225 100644
--- a/DocGen4/Output/Class.lean
+++ b/DocGen4/Output/Class.lean
@@ -8,21 +8,18 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
-def classInstanceToHtml (name : Name) : HtmlM Html := do
- pure
{←declNameToHtmlLink name}
+--def classInstanceToHtml (name : Name) : HtmlM Html := do
+-- pure
{←declNameToHtmlLink name}
-def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
- let instancesHtml ← instances.mapM classInstanceToHtml
+def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
Instances
-
- [instancesHtml]
-
+
def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
- pure $ (←structureToHtml i.toStructureInfo)
+ structureToHtml i
end Output
end DocGen4
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
index 7b8ab24..746b005 100644
--- a/DocGen4/Output/ClassInductive.lean
+++ b/DocGen4/Output/ClassInductive.lean
@@ -8,7 +8,7 @@ namespace DocGen4
namespace Output
def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
- pure $ (←inductiveToHtml i.toInductiveInfo)
+ inductiveToHtml i
end Output
end DocGen4
diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean
index a787ac4..d0f171c 100644
--- a/DocGen4/Output/Find.lean
+++ b/DocGen4/Output/Find.lean
@@ -10,7 +10,7 @@ def find : BaseHtmlM Html := do
pure
-
+
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index efd6a31..4aa50ee 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -78,7 +78,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
match doc with
| DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i)
- | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
+ | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i)
| _ => nodes := nodes
nodes := nodes.push :
@@ -95,18 +95,18 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i
| DocInfo.classInductiveInfo i => classInductiveToHtml i
- | i => pure #[]
+ | _ => pure #[]
-- rendered doc stirng
let docStringHtml ← match doc.getDocString with
| some s => docStringToHtml s
| none => pure #[]
-- extra information like equations and instances
let extraInfoHtml ← match doc with
- | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances]
+ | DocInfo.classInfo i => pure #[←classInstancesToHtml i.name]
| DocInfo.definitionInfo i => equationsToHtml i
- | DocInfo.instanceInfo i => equationsToHtml i
- | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
- | i => pure #[]
+ | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
+ | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.name]
+ | _ => pure #[]
let attrs := doc.getAttrs
let attrsHtml :=
if attrs.size > 0 then
@@ -143,7 +143,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
Rendering a module doc string, that is the ones with an ! after the opener
as HTML.
-/
-def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
+def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
pure
[←docStringToHtml mdoc.doc]
@@ -156,7 +156,7 @@ as HTML.
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
match member with
| ModuleMember.docInfo d => docInfoToHtml module d
- | ModuleMember.modDoc d => modDocToHtml module d
+ | ModuleMember.modDoc d => modDocToHtml d
def declarationToNavLink (module : Name) : Html :=
@@ -168,13 +168,7 @@ Returns the list of all imports this module does.
-/
def getImports (module : Name) : HtmlM (Array Name) := do
let res ← getResult
- let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
- let adj := res.importAdj.get! idx
- let mut imports := #[]
- for i in [:adj.size] do
- if adj.get! i then
- imports := imports.push (res.moduleNames.get! i)
- pure imports
+ pure $ res.moduleInfo.find! module |>.imports
/--
Sort the list of all modules this one is importing, linkify it
@@ -184,27 +178,6 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
let imports := (←getImports moduleName) |>.qsort Name.lt
imports.mapM (λ i => do pure
{←moduleToHtmlLink i}
)
-/--
-Returns a list of all modules this module is imported by.
--/
-def getImportedBy (module : Name) : HtmlM (Array Name) := do
- let res ← getResult
- let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
- let adj := res.importAdj
- let mut impBy := #[]
- for i in [:adj.size] do
- if adj.get! i |>.get! idx then
- impBy := impBy.push (res.moduleNames.get! i)
- pure impBy
-
-/--
-Sort the list of all modules this one is imported by, linkify it
-and return the HTML.
--/
-def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
- let imports := (←getImportedBy moduleName) |>.qsort Name.lt
- imports.mapM (λ i => do pure
{←moduleToHtmlLink i}
)
-
/--
Render the internal nav bar (the thing on the right on all module pages).
-/
@@ -222,9 +195,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
Imported by
-
- [←importedByHtml moduleName]
-
+
[members.map declarationToNavLink]
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index bf70e34..6f18a02 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -57,21 +57,33 @@ The main entry point to rendering the navbar on the left hand side.
-/
def navbar : BaseHtmlM Html := do
pure
-
+
+
+ [←baseHtmlHeadDeclarations]
+
+
+
+
+
+
+
+
+
+
end Output
end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index 49aa9f5..ae7878b 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -15,29 +15,28 @@ open scoped DocGen4.Jsx
The HTML template used for all pages.
-/
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
+ let moduleConstant :=
+ if let some module := (←getCurrentName) then
+ #[]
+ else
+ #[]
pure
+ [←baseHtmlHeadDeclarations]
{title}
-
-
-
-
-
-
-
-
-
+ [moduleConstant]
-
+
+
@@ -57,10 +56,10 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
[site]
- {←navbar}
-
+
-
/--
diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean
new file mode 100644
index 0000000..7d0a06c
--- /dev/null
+++ b/DocGen4/Output/ToJson.lean
@@ -0,0 +1,52 @@
+import Lean
+import DocGen4.Process
+import DocGen4.Output.Base
+import Std.Data.RBMap
+
+namespace DocGen4.Output
+
+open Lean Std
+
+structure JsonDeclaration where
+ name : String
+ doc : String
+ docLink : String
+ sourceLink : String
+ deriving FromJson, ToJson
+
+structure JsonInstance where
+ name : String
+ className : String
+ deriving FromJson, ToJson
+
+structure JsonModule where
+ name : String
+ declarations : List JsonDeclaration
+ instances : Array JsonInstance
+ imports : Array String
+ deriving FromJson, ToJson
+
+def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
+ let name := info.getName.toString
+ let doc := info.getDocString.getD ""
+ let docLink ← declNameToLink info.getName
+ let sourceLink ← getSourceUrl module info.getDeclarationRange
+ pure { name, doc, docLink, sourceLink }
+
+def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
+ let mut jsonDecls := []
+ let mut instances := #[]
+ let declInfo := Process.filterMapDocInfo module.members
+ for decl in declInfo do
+ jsonDecls := (←DocInfo.toJson module.name decl) :: jsonDecls
+ if let .instanceInfo i := decl then
+ instances := instances.push { name := i.name.toString, className := i.instClass.toString}
+ let jsonMod : JsonModule := {
+ name := module.name.toString,
+ declarations := jsonDecls,
+ instances := instances
+ imports := module.imports.map Name.toString
+ }
+ pure $ ToJson.toJson jsonMod
+
+end DocGen4.Output
diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
index 3ce5b95..35c4563 100644
--- a/DocGen4/Process/Analyze.lean
+++ b/DocGen4/Process/Analyze.lean
@@ -12,14 +12,9 @@ import DocGen4.Process.Base
import DocGen4.Process.Hierarchy
import DocGen4.Process.DocInfo
-open Std
-
-def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α :=
- xs.foldr (flip .insert) .empty
-
namespace DocGen4.Process
-open Lean Meta
+open Lean Meta Std
/--
Member of a module, either a declaration or some module doc string.
@@ -41,6 +36,7 @@ structure Module where
All members of the module, sorted according to their line numbers.
-/
members : Array ModuleMember
+ imports : Array Name
deriving Inhabited
/--
@@ -59,11 +55,6 @@ structure AnalyzerResult where
A map from module names to information about these modules.
-/
moduleInfo : HashMap Name Module
- /--
- An adjacency matrix for the import relation between modules, indexed
- my the values in `name2ModIdx`.
- -/
- importAdj : Array (Array Bool)
deriving Inhabited
namespace ModuleMember
@@ -92,41 +83,29 @@ 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 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
let mut res := mkHashMap relevantModules.size
for module in relevantModules do
let modDocs := getModuleDoc? env module |>.getD #[] |>.map .modDoc
- res := res.insert module (Module.mk module modDocs)
- pure res
-
--- TODO: This is definitely not the most efficient way to store this data
-def buildImportAdjMatrix (allModules : Array Name) : MetaM (Array (Array Bool)) := do
- let env ← getEnv
- let mut adj := Array.mkArray allModules.size (Array.mkArray allModules.size false)
- for moduleName in allModules do
- let some modIdx := env.getModuleIdx? moduleName | unreachable!
+ let some modIdx := env.getModuleIdx? module | unreachable!
let moduleData := env.header.moduleData.get! modIdx
- for imp in moduleData.imports do
- let some importIdx := env.getModuleIdx? imp.module | unreachable!
- adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
- pure adj
+ let imports := moduleData.imports.map Import.module
+ res := res.insert module $ Module.mk module modDocs imports
+ pure res
/--
Run the doc-gen analysis on all modules that are loaded into the `Environment`
@@ -136,7 +115,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
@@ -162,8 +141,6 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
catch e =>
IO.println s!"WARNING: Failed to obtain information for: {name}: {←e.toMessageData.toString}"
- let adj ← buildImportAdjMatrix allModules
-
-- TODO: This could probably be faster if we did sorted insert above instead
for (moduleName, module) in res.toArray do
res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
@@ -173,7 +150,6 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
name2ModIdx := env.const2ModIdx,
moduleNames := allModules,
moduleInfo := res,
- importAdj := adj
}
pure (analysis, hierarchy)
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index ee02fac..6a6b550 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -103,7 +103,9 @@ structure DefinitionInfo extends Info where
/--
Information about an `instance` declaration.
-/
-abbrev InstanceInfo := DefinitionInfo
+structure InstanceInfo extends DefinitionInfo where
+ instClass : Name
+ deriving Inhabited
/--
Information about an `inductive` declaration
@@ -137,16 +139,12 @@ structure StructureInfo extends Info where
/--
Information about a `class` declaration.
-/
-structure ClassInfo extends StructureInfo where
- instances : Array Name
- deriving Inhabited
+abbrev ClassInfo := StructureInfo
/--
Information about a `class inductive` declaration.
-/
-structure ClassInductiveInfo extends InductiveInfo where
- instances : Array Name
- deriving Inhabited
+abbrev ClassInductiveInfo := InductiveInfo
/--
A general type for informations about declarations.
diff --git a/DocGen4/Process/ClassInfo.lean b/DocGen4/Process/ClassInfo.lean
index 0d6df44..0c29db7 100644
--- a/DocGen4/Process/ClassInfo.lean
+++ b/DocGen4/Process/ClassInfo.lean
@@ -15,18 +15,10 @@ namespace DocGen4.Process
open Lean Meta
-def getInstances (className : Name) : MetaM (Array Name) := do
- let fn ← mkConstWithFreshMVarLevels className
- let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
- let insts ← SynthInstance.getInstances (mkAppN fn xs)
- pure $ insts.map Expr.constName!
-
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
- let sinfo ← StructureInfo.ofInductiveVal v
- pure $ ClassInfo.mk sinfo (←getInstances v.name)
+ StructureInfo.ofInductiveVal v
def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
- let info ← InductiveInfo.ofInductiveVal v
- pure $ ClassInductiveInfo.mk info (←getInstances v.name)
+ InductiveInfo.ofInductiveVal v
end DocGen4.Process
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index 32b2805..7727e15 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -6,9 +6,14 @@ Authors: Henrik Böving
import Lean
import Std.Data.HashMap
+open Std
+
+def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α :=
+ xs.foldr (flip .insert) .empty
+
namespace DocGen4
-open Lean Std Name
+open Lean Name
def getNLevels (name : Name) (levels: Nat) : Name :=
let components := name.components'
@@ -78,5 +83,38 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
partial def fromArray (names : Array Name) : Hierarchy :=
names.foldl insert! (empty anonymous false)
+def baseDirBlackList : HashSet String :=
+ HashSet.fromArray #[
+ "404.html",
+ "declaration-data.js",
+ "declarations",
+ "find",
+ "how-about.js",
+ "index.html",
+ "mathjax-config.js",
+ "navbar.html",
+ "nav.js",
+ "search.js",
+ "src",
+ "style.css"
+ ]
+
+
+partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do
+ let mut children := #[]
+ for entry in ←System.FilePath.readDir dir do
+ if (←entry.path.isDir) then
+ children := children ++ (←fromDirectoryAux entry.path (.str previous entry.fileName))
+ else
+ children := children.push $ .str previous (entry.fileName.dropRight ".html".length)
+ pure children
+
+def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
+ let mut children := #[]
+ for entry in ←System.FilePath.readDir dir do
+ if !baseDirBlackList.contains entry.fileName && (←entry.path.isDir) then
+ children := children ++ (←fromDirectoryAux entry.path (.mkSimple entry.fileName))
+ pure $ Hierarchy.fromArray children
+
end Hierarchy
end DocGen4
diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean
index 23c603b..c4c4a07 100644
--- a/DocGen4/Process/InstanceInfo.lean
+++ b/DocGen4/Process/InstanceInfo.lean
@@ -17,8 +17,8 @@ def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let info ← DefinitionInfo.ofDefinitionVal v
let some className := getClassName (←getEnv) v.type | unreachable!
if let some instAttr ← getDefaultInstance v.name className then
- pure { info with attrs := info.attrs.push instAttr }
+ pure $ InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className
else
- pure info
+ pure $ InstanceInfo.mk info className
end DocGen4.Process
diff --git a/Main.lean b/Main.lean
index 2ea998e..f514be6 100644
--- a/Main.lean
+++ b/Main.lean
@@ -21,31 +21,22 @@ 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)
pure 0
| Except.error rc => pure rc
-def runFinalizeCmd (p : Parsed) : IO UInt32 := do
- let topLevelModules ← getTopLevelModules p
- let res ← lakeSetup topLevelModules
- match res with
- | Except.ok _ =>
- let modules := topLevelModules.map Name.mkSimple
- let hierarchy ← loadInit modules
- let baseConfig := getSimpleBaseContext hierarchy
- htmlOutputFinalize baseConfig
- pure 0
- | Except.error rc => pure rc
+def runIndexCmd (p : Parsed) : IO UInt32 := do
+ let hierarchy ← Hierarchy.fromDirectory basePath
+ let baseConfig := getSimpleBaseContext hierarchy
+ htmlOutputIndex baseConfig
pure 0
def runDocGenCmd (p : Parsed) : IO UInt32 := do
@@ -57,7 +48,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,12 +64,11 @@ 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 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 +85,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..75c7ba1 100644
--- a/README.md
+++ b/README.md
@@ -26,22 +26,22 @@ For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and i
- `Std`
- `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`
-The second and last stage is the finalize one which zips up some
+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:
```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
```
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
new file mode 100644
index 0000000..a039515
--- /dev/null
+++ b/lean_packages/manifest.json
@@ -0,0 +1,20 @@
+{"version": 1,
+ "packages":
+ [{"url": "https://github.com/mhuisi/lean4-cli",
+ "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
+ "name": "Cli"},
+ {"url": "https://github.com/hargonix/LeanInk",
+ "rev": "cb529041f71a4ea8348628a8c723326e3e4bdecc",
+ "name": "leanInk"},
+ {"url": "https://github.com/xubaiw/Unicode.lean",
+ "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",
+ "name": "Unicode"},
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
+ "name": "mathlib"},
+ {"url": "https://github.com/leanprover/lake",
+ "rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217",
+ "name": "lake"},
+ {"url": "https://github.com/xubaiw/CMark.lean",
+ "rev": "8f17d13d3046c517f7f02062918d81bc69e45cce",
+ "name": "CMark"}]}
\ No newline at end of file
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 0c284dc..a12d4f1 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -8,16 +8,6 @@ const CACHE_DB_NAME = "declaration-data";
const CACHE_DB_VERSION = 1;
const CACHE_DB_KEY = "DECLARATIONS_KEY";
-async function fetchModuleData(module) {
- const moduleDataUrl = new URL(
- `${SITE_ROOT}declaration-data-${module}.bmp`,
- window.location
- );
- const moduleData = await fetch(moduleDataUrl);
- const moduleDataJson = await moduleData.json();
- return moduleDataJson;
-}
-
/**
* The DeclarationDataCenter is used for declaration searching.
*
@@ -53,7 +43,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
);
@@ -65,25 +55,7 @@ export class DeclarationDataCenter {
} else {
// undefined. then fetch the data from the server.
const dataListRes = await fetch(dataListUrl);
- const dataListJson = await dataListRes.json();
-
- // TODO: this is probably kind of inefficient
- const dataJsonUnflattened = await Promise.all(dataListJson.map(fetchModuleData));
-
- const dataJson = dataJsonUnflattened.flat();
- // the data is a map of name (original case) to declaration data.
- const data = new Map(
- dataJson.map(({ name, doc, docLink, sourceLink }) => [
- name,
- {
- name,
- lowerName: name.toLowerCase(),
- lowerDoc: doc.toLowerCase(),
- docLink,
- sourceLink,
- },
- ])
- );
+ const data = await dataListRes.json();
await cacheDeclarationData(data);
DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
}
@@ -100,12 +72,49 @@ export class DeclarationDataCenter {
return [];
}
if (strict) {
- let decl = this.declarationData.get(pattern);
+ let decl = this.declarationData.declarations[pattern];
return decl ? [decl] : [];
} else {
- return getMatches(this.declarationData, pattern);
+ return getMatches(this.declarationData.declarations, pattern);
}
}
+
+ /**
+ * Search for all instances of a certain typeclass
+ * @returns {Array}
+ */
+ instancesForClass(className) {
+ const instances = this.declarationData.instances[className];
+ if (!instances) {
+ return [];
+ } else {
+ return instances;
+ }
+ }
+
+ /**
+ * Analogous to Lean declNameToLink
+ * @returns {String}
+ */
+ declNameToLink(declName) {
+ return this.declarationData.declarations[declName].docLink;
+ }
+
+ /**
+ * Find all modules that imported the given one.
+ * @returns {Array}
+ */
+ moduleImportedBy(moduleName) {
+ return this.declarationData.importedBy[moduleName];
+ }
+
+ /**
+ * Analogous to Lean moduleNameToLink
+ * @returns {String}
+ */
+ moduleNameToLink(moduleName) {
+ return this.declarationData.modules[moduleName];
+ }
}
function isSeparater(char) {
@@ -141,13 +150,14 @@ function getMatches(declarations, pattern, maxResults = 30) {
const lowerPats = pattern.toLowerCase().split(/\s/g);
const patNoSpaces = pattern.replace(/\s/g, "");
const results = [];
- for (const {
+ for (const [_, {
name,
- lowerName,
- lowerDoc,
+ doc,
docLink,
sourceLink,
- } of declarations.values()) {
+ }] of Object.entries(declarations)) {
+ const lowerName = name.toLowerCase();
+ const lowerDoc = doc.toLowerCase();
let err = matchCaseSensitive(name, lowerName, patNoSpaces);
// match all words as substrings of docstring
if (
diff --git a/static/importedBy.js b/static/importedBy.js
new file mode 100644
index 0000000..dab932d
--- /dev/null
+++ b/static/importedBy.js
@@ -0,0 +1,19 @@
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+fillImportedBy();
+
+async function fillImportedBy() {
+ if (!MODULE_NAME) {
+ return;
+ }
+ const dataCenter = await DeclarationDataCenter.init();
+ const moduleName = MODULE_NAME;
+ const importedByList = document.querySelector(".imported-by-list");
+ const importedBy = dataCenter.moduleImportedBy(moduleName);
+ var innerHTML = "";
+ for(var module of importedBy) {
+ const moduleLink = dataCenter.moduleNameToLink(module);
+ innerHTML += `