Update to doc-gen4 commit `86d5c21`.

DocGen4/Load.lean

@@ -29,10 +29,14 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
   let config := {
     -- TODO: parameterize maxHeartbeats
     maxHeartbeats := 100000000,
-    options := ⟨[(`pp.tagAppFns, true)]⟩,
+    options := ⟨[
+      (`pp.tagAppFns, true),
+      (`pp.funBinderTypes, true)
+    ]⟩,
     -- TODO: Figure out whether this could cause some bugs
     fileName := default,
     fileMap := default,
+    catchRuntimeEx := true,
   }
 
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}

DocGen4/Output/Base.lean

@@ -11,7 +11,7 @@ namespace DocGen4.Output
 open scoped DocGen4.Jsx
 open Lean System Widget Elab Process
 
-def basePath := FilePath.mk "." / "build" / "doc"
+def basePath := FilePath.mk "." / ".lake" / "build" / "doc"
 def srcBasePath := basePath / "src"
 def declarationsBasePath := basePath / "declarations"
 
@@ -105,6 +105,13 @@ def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do
   let parts := n.name.components.map Name.toString
   return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString
 
+/--
+Returns the doc-gen4 link to a module name.
+-/
+def moduleNameToLink (n : Name) : BaseHtmlM String := do
+  let parts := n.components.map Name.toString
+  return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
 /--
 Returns the doc-gen4 link to a module name.
 -/

DocGen4/Output/Inductive.lean

@@ -10,9 +10,9 @@ open Lean
 
 def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
   pure
-    <details «class»="instances">
+    <details id={s!"instances-for-list-{typeName}"} «class»="instances-for-list">
         <summary>Instances For</summary>
-        <ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
+        <ul class="instances-for-enum"></ul>
     </details>
 
 def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do

DocGen4/Output/Module.lean

@@ -133,8 +133,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         [leanInkHtml]
         [attrsHtml]
         {← docInfoHeader doc}
-        [docInfoHtml]
         [docStringHtml]
+        [docInfoHtml]
         [extraInfoHtml]
       </div>
     </div>

DocGen4/Output/ToJson.lean

@@ -43,11 +43,15 @@ structure JsonIndexedDeclarationInfo where
   docLink : String
   deriving FromJson, ToJson
 
+structure JsonIndexedModule where
+  importedBy : Array String
+  url : String
+  deriving FromJson, ToJson
+
 structure JsonIndex where
   declarations : List (String × JsonIndexedDeclarationInfo) := []
   instances : HashMap String (RBTree String Ord.compare) := .empty
-  importedBy : HashMap String (Array String) := .empty
+  modules : HashMap String JsonIndexedModule := {}
-  modules : List (String × String) := []
   instancesFor : HashMap String (RBTree String Ord.compare) := .empty
 
 instance : ToJson JsonHeaderIndex where
@@ -57,13 +61,11 @@ 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.toArray))
-    let jsonImportedBy := Json.mkObj <| idx.importedBy.toList.map (fun (k, v) => (k, toJson v))
+    let jsonModules := Json.mkObj <| idx.modules.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.toArray))
     let finalJson := Json.mkObj [
       ("declarations", jsonDecls),
       ("instances", jsonInstances),
-      ("importedBy", jsonImportedBy),
       ("modules", jsonModules),
       ("instancesFor", jsonInstancesFor)
     ]
@@ -75,15 +77,14 @@ def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) :
 
 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.info.name, {
     kind := d.info.kind,
     docLink := d.info.docLink,
   }))
   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 {}
@@ -94,10 +95,26 @@ def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM Js
       instsFor := instsFor.insert inst.name
       index := { index with instancesFor := index.instancesFor.insert typeName instsFor }
 
+  -- TODO: dedup
+  if index.modules.find? module.name |>.isNone then
+    let moduleLink <- moduleNameToLink (String.toName module.name)
+    let indexedModule := { url := moduleLink, importedBy := #[] }
+    index := { index with modules := index.modules.insert module.name indexedModule }
+
   for imp in module.imports do
-    let mut impBy := index.importedBy.findD imp #[]
+    let indexedImp ←
-    impBy := impBy.push module.name
+      match index.modules.find? imp with
-    index := { index with importedBy := index.importedBy.insert imp impBy }
+      | some i => pure i
+      | none =>
+        let impLink ←  moduleNameToLink (String.toName imp)
+        let indexedModule := { url := impLink, importedBy := #[] }
+        pure indexedModule
+    index := { index with
+      modules :=
+        index.modules.insert
+        imp
+        { indexedImp with importedBy := indexedImp.importedBy.push module.name }
+    }
   return index
 
 def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do

DocGen4/Process/Analyze.lean

@@ -126,7 +126,8 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
         maxHeartbeats := 5000000,
         options := ← getOptions,
         fileName := ← getFileName,
-        fileMap := ← getFileMap
+        fileMap := ← getFileMap,
+        catchRuntimeEx := true,
       }
       let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
       if let some dinfo := analysis then

DocGen4/Process/DefinitionInfo.lean

@@ -36,8 +36,10 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
   let info ← Info.ofConstantVal v.toConstantVal
   let isUnsafe := v.safety == DefinitionSafety.unsafe
   let isNonComputable := isNoncomputable (← getEnv) v.name
+
   try
-    let eqs? ← getEqnsFor? v.name
+    let eqs? ←  getEqnsFor? v.name
+
     match eqs? with
     | some eqs =>
       let equations ← eqs.mapM processEq

static/declaration-data.js

@@ -128,7 +128,7 @@ export class DeclarationDataCenter {
    * @returns {Array<String>}
    */
   moduleImportedBy(moduleName) {
-    return this.declarationData.importedBy[moduleName];
+    return this.declarationData.modules[moduleName].importedBy;
   }
 
   /**
@@ -136,7 +136,7 @@ export class DeclarationDataCenter {
    * @returns {String}
    */
   moduleNameToLink(moduleName) {
-    return this.declarationData.modules[moduleName];
+    return this.declarationData.modules[moduleName].url;
   }
 }
 

static/instances.js

@@ -26,11 +26,16 @@ async function annotateInstancesFor() {
   for (const instanceForList of instanceForLists) {
     const typeName = instanceForList.id.slice("instances-for-list-".length);
     const instances = dataCenter.instancesForType(typeName);
-    var innerHTML = "";
+    if (instances.length == 0) {
-    for(var instance of instances) {
+      instanceForList.remove();
-      const instanceLink = dataCenter.declNameToLink(instance);
+    } else {
-      innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
+      var innerHTML = "";
+      for(var instance of instances) {
+        const instanceLink = dataCenter.declNameToLink(instance);
+        innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`;
+      }
+      const instanceEnum = instanceForList.querySelector(".instances-for-enum");
+      instanceEnum.innerHTML = innerHTML;
     }
-    instanceForList.innerHTML = innerHTML;
   }
 }

static/style.css

@@ -1,15 +1,20 @@
-@import url('https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro&family=Source+Code+Pro:wght@600&display=swap');
+@import url('https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css');
+@import url('https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.051/juliamono.css');
 
 * {
     box-sizing: border-box;
 }
 
 body {
-    font-family: 'Open Sans', sans-serif;
+    font-size: 17px;
+    font-variant-ligatures: none;
+    font-family: 'Lato Medium';
     color: var(--text-color);
     background: var(--body-bg);
 }
 
+input, select, textarea, button{font-family:inherit;}
+
 a {
    color: var(--link-color);
 }
@@ -19,7 +24,8 @@ a.pdf {
 }
 
 h1, h2, h3, h4, h5, h6 {
-    font-family: 'Merriweather', serif;
+   font-family: 'Lato Medium';
+   font-size: 17px;
 }
 
 body { line-height: 1.5; }
@@ -678,8 +684,10 @@ main h2, main h3, main h4, main h5, main h6 {
 }
 
 .imports li, code, .decl_header, .attributes, .structure_field_info,
-        .constructor, .instances li, .equation, .result_link, .structure_ext_ctor {
+.constructor, .instances li, .instances-for-list li, .equation,
-    font-family: 'Source Code Pro', monospace;
+.structure_ext_ctor {
+    font-size: 16px;
+    font-family: 'JuliaMono', monospace;
 }
 
 pre {
@@ -709,12 +717,14 @@ pre code { padding: 0 0; }
 
 .inductive_ctor_doc  {
     text-indent: 2ex;
-    font-family: 'Open Sans', sans-serif;
+    font-family: 'Lato Medium';
+    font-size: 17px;
 }
 
 .structure_field_doc {
     text-indent: 0;
-    font-family: 'Open Sans', sans-serif;
+    font-family: 'Lato Medium';
+    font-size: 17px;
 }
 
 .structure_ext_fields {