feat: Step 1 for full separate builds with global info

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
 
@@ -43,6 +44,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("how-about.js", howAboutJs),
     ("search.js", searchJs),
     ("mathjax-config.js", mathjaxConfigJs),
+    ("instances.js", instancesJs),
     ("index.html", indexHtml),
     ("404.html", notFoundHtml),
     ("navbar.html", navbarHtml)
@@ -68,24 +70,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") (Json.arr jsonDecls).compress
+    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 := {
@@ -134,14 +122,34 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
 def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig
 
-  let mut topLevelModules := #[]
+  let mut allDecls : List (String × Json) := []
+  let mut allInstances : HashMap String (Array String) := .empty
+  let mut importedBy : HashMap String (Array String) := .empty
   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
+      IO.println s!"Processing: {entry.fileName}"
-      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!
+      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)
+  ]
   -- The root JSON for find
-  FS.writeFile (declarationsBasePath / "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

DocGen4/Output/Base.lean

@@ -132,6 +132,7 @@ 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 findJs : String := include_str "../../static/find/find.js"
   def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
   
@@ -220,9 +221,9 @@ def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
     <meta charset="UTF-8"/>,
     <meta name="viewport" content="width=device-width, initial-scale=1"/>,
     <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>,
-    <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>,
+    <link rel="stylesheet" href={s!"{←getRoot}src/pygments.css"}/>,
     <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>,
-    <link rel="prefetch" href={s!"{←getRoot}declaration-data.bmp"}/>
+    <link rel="prefetch" href={s!"{←getRoot}/declarations/declaration-data.bmp"}/>
   ]
 
 end DocGen4.Output

DocGen4/Output/Class.lean

@@ -8,21 +8,18 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
-def classInstanceToHtml (name : Name) : HtmlM Html := do
+--def classInstanceToHtml (name : Name) : HtmlM Html := do
-  pure <li>{←declNameToHtmlLink name}</li>
+--  pure <li>{←declNameToHtmlLink name}</li>
 
-def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
+def classInstancesToHtml (className : Name) : HtmlM Html := do
-  let instancesHtml ← instances.mapM classInstanceToHtml
   pure
     <details «class»="instances">
         <summary>Instances</summary>
-        <ul>
+        <ul id={s!"instances-list-{className}"}></ul>
-          [instancesHtml]
-        </ul>
     </details>
 
 def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
-  pure $ (←structureToHtml i.toStructureInfo)
+  structureToHtml i
 
 end Output
 end DocGen4

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

DocGen4/Output/Find.lean

@@ -10,7 +10,7 @@ def find : BaseHtmlM Html := do
   pure
     <html lang="en">
       <head>
-        <link rel="preload" href={s!"{←getRoot}declaration-data.bmp"}/>
+        <link rel="preload" href={s!"{←getRoot}/declarations/declaration-data.bmp"}/>
         <script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
         <script type="module" async="true" src="./find.js"></script>
       </head>

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 <span class="decl_args">:</span>
@@ -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.instanceInfo i => equationsToHtml i.toDefinitionInfo
-  | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
+  | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.name]
-  | i => pure #[]
+  | _ => 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 
     <div class="mod_doc">
       [←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 :=
   <div class="nav_link">
@@ -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!
+  pure $ res.moduleInfo.find! module |>.imports
-  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
 
 /--
 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 <li>{←moduleToHtmlLink i}</li>)
 
-/--
-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 <li>{←moduleToHtmlLink i}</li>)
-
 /--
 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
         </details>
         <details>
           <summary>Imported by</summary>
-          <ul>
+          <ul id={s!"imported-by-{moduleName}"}> </ul>
-            [←importedByHtml moduleName]
-          </ul>
         </details>
       </div>
       [members.map declarationToNavLink]

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

DocGen4/Process/Analyze.lean

@@ -36,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
 
 /--
@@ -54,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
@@ -105,20 +101,11 @@ def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module
   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)
+    let some modIdx := env.getModuleIdx? module | unreachable!
-  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 moduleData := env.header.moduleData.get! modIdx
-    for imp in moduleData.imports do
+    let imports := moduleData.imports.map Import.module
-      let some importIdx := env.getModuleIdx? imp.module | unreachable!
+    res := res.insert module $ Module.mk module modDocs imports
-      adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
+  pure res
-  pure adj
 
 /--
 Run the doc-gen analysis on all modules that are loaded into the `Environment`
@@ -154,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}
@@ -165,7 +150,6 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
     name2ModIdx := env.const2ModIdx,
     moduleNames := allModules,
     moduleInfo := res,
-    importAdj := adj
   }
   pure (analysis, hierarchy)
 

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
+abbrev ClassInfo := StructureInfo
-  instances : Array Name
-  deriving Inhabited
 
 /--
 Information about a `class inductive` declaration.
 -/
-structure ClassInductiveInfo extends InductiveInfo where
+abbrev ClassInductiveInfo := InductiveInfo
-  instances : Array Name
-  deriving Inhabited
 
 /--
 A general type for informations about declarations.

DocGen4/Process/ClassInfo.lean

@@ -22,11 +22,9 @@ def getInstances (className : Name) : MetaM (Array Name) := do
   pure $ insts.map Expr.constName!
 
 def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
-  let sinfo ← StructureInfo.ofInductiveVal v
+  StructureInfo.ofInductiveVal v
-  pure $ ClassInfo.mk sinfo (←getInstances v.name)
 
 def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
-  let info ← InductiveInfo.ofInductiveVal v
+  InductiveInfo.ofInductiveVal v
-  pure $ ClassInductiveInfo.mk info (←getInstances v.name)
 
 end DocGen4.Process

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

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}/declarations/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.
  *
@@ -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();
+        const data = 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,
-            },
-          ])
-        );
         await cacheDeclarationData(data);
         DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
       }
@@ -100,10 +72,10 @@ 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);
     }
   }
 }
@@ -141,13 +113,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,
+    doc,
-    lowerDoc,
     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 (