Polish further.

.envrc

@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-
-use flake

.gitignore

@@ -4,7 +4,6 @@ lakefile.olean
 lake-packages
 _target
 leanpkg.path
-.lake/
 
 # TeX
 *.aux
@@ -22,9 +21,3 @@ leanpkg.path
 *.synctex.gz
 *.toc
 .*.lb
-
-# direnv
-.direnv/
-
-# nix
-result

Bookshelf/Apostol/Chapter_1_11.lean

@@ -50,7 +50,7 @@ theorem exercise_4c (x y : ℝ)
   : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ∨ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by
   have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl)
   have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl)
-  by_cases h : Int.fract x + Int.fract y < 1
+  by_cases Int.fract x + Int.fract y < 1
   · refine Or.inl ?_
     rw [Int.floor_eq_iff]
     simp only [Int.cast_add]

Bookshelf/Apostol/Chapter_I_03.lean

@@ -1,5 +1,5 @@
 import Common.Set
-import Mathlib.Data.Real.Archimedean
+import Mathlib.Data.Real.Basic
 
 /-! # Apostol.Chapter_I_03
 

Bookshelf/Enderton/Logic/Chapter_1.lean

@@ -481,7 +481,7 @@ theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k)
       exact absurd hr hk
     unfold σ
     rw [hn₁]
-    simp only [Nat.add_eq, add_zero, imp_false, not_not]
+    simp only [Nat.add_eq, add_zero, not_forall, exists_prop, and_true]
     exact exercise_1_2_2b_i False Q hn₂
 
 end Exercise_1_2_2

Bookshelf/Enderton/Set/Chapter_2.lean

@@ -616,7 +616,7 @@ lemma right_diff_eq_insert_one_three : A \ (B \ C) = {1, 3} := by
       rw [hy] at hz
       unfold Membership.mem Set.instMembershipSet Set.Mem at hz
       unfold singleton Set.instSingletonSet Set.singleton setOf at hz
-      simp at hz
+      simp only at hz
     · intro hy
       refine ⟨Or.inr (Or.inr hy), ?_⟩
       intro hz

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -542,7 +542,7 @@ theorem exercise_3_1 {x y z u v w : ℕ}
   · rw [hx, hy, hz, hu, hv, hw]
     simp
   · rw [hy, hv]
-    simp
+    simp only
 
 /-- ### Exercise 3.2a
 

Bookshelf/Enderton/Set/Chapter_4.lean

@@ -702,7 +702,7 @@ theorem exercise_4_17 (m n p : ℕ)
   | zero => calc m ^ (n + 0)
     _ = m ^ n := rfl
     _ = m ^ n * 1 := by rw [right_mul_id]
-    _ = m ^ n * m ^ 0 := by rfl
+    _ = m ^ n * m ^ 0 := rfl
   | succ p ih => calc m ^ (n + p.succ)
     _ = m ^ (n + p).succ := rfl
     _ = m ^ (n + p) * m := rfl

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -512,7 +512,7 @@ theorem corollary_6d_b
     ]
     refine ⟨1, ?_⟩
     intro x nx
-    simp only [mul_eq_one, OfNat.ofNat_ne_one, false_and] at nx
+    simp only [mul_eq_one, false_and] at nx
 
 /-- ### Corollary 6E
 
@@ -935,23 +935,76 @@ natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥
 theorem finite_dom_ran_size [Nonempty α] {A B : Set α}
   (hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B)
   : ∃ m n : ℕ, A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by
+/-
+> Let `A` and `B` be finite sets and `f : A → B` be a function. By definition of
+> finite sets, there exists natural numbers `m, p ∈ ω` such that `A ≈ m` and
+> `B ≈ p`. By definition of the domain of a function, `dom f = A`. Thus
+> `dom f ≈ m`.
+-/
   have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA
   have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB
+/-
+> By *Theorem 6A*, there exists a one-to-one correspondence `g` between `m` and
+> `dom f = A`.
+-/
   have ⟨g, hg⟩ := Set.equinumerous_symm hm
-
+/-
+> For all `y ∈ ran f`, consider `f⁻¹⟦{y}⟧`. Let
+>
+> `A_y = {x ∈ m | f(g(x)) = y}`.
+-/
   let A_y y := { x ∈ Set.Iio m | f (g x) = y }
-  have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by
+/-
+> Since `g` is a one-to-one correspondence, it follows that `A_y ≈ f⁻¹⟦{y}⟧`.
+-/
+  have hA₁ : ∀ y, y ∈ f '' A → A_y y ≈ A ∩ f ⁻¹' {y} := by
+    intro y hy
+    refine ⟨fun x => g x, ?_, ?_, ?_⟩
+    · -- `Set.MapsTo`
+      intro x hx
+      simp only [Set.mem_Iio, Set.mem_setOf_eq, Set.mem_preimage, Set.mem_singleton_iff] at hx ⊢
+      exact ⟨hg.left hx.left, hx.right⟩
+    · -- `Set.InjOn`
+      intro x₁ hx₁ x₂ hx₂ hf
+      exact hg.right.left hx₁.left hx₂.left hf
+    · -- `Set.SurjOn`
+      unfold Set.SurjOn Set.preimage Set.image
+      rw [Set.subset_def]
+      simp only [Set.mem_singleton_iff, Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_Iio]
+      intro x ⟨hx₁, hx₂⟩
+      have hx₃ := hg.right.right hx₁
+      simp only [Set.mem_image, Set.mem_Iio] at hx₃
+      have ⟨z, hz⟩ := hx₃
+      exact ⟨z, ⟨hz.left, hz.right ▸ hx₂⟩, hz.right⟩
+/-
+> Since `A_y` is a nonempty subset of natural numbers, the
+> *Well Ordering of `ω`* implies there exists a least element, say `q_y`.
+-/
+  have hA₂ : ∀ y, y ∈ f '' A → Set.Nonempty (A_y y) := by
+    intro y hy
+    unfold Set.Nonempty
+    simp only [Set.mem_image, Set.mem_Iio, Set.mem_setOf_eq] at hy ⊢
+    have ⟨x, hx⟩ := hy
+    have ⟨z, hz⟩ := hg.right.right hx.left
+    simp only [Set.mem_Iio] at hz
+    exact ⟨z, hz.left, hz.right ▸ hx.right⟩
+  have hA₃ : ∀ y, y ∈ f '' A → ∃ q, q ∈ A_y y ∧ ∀ p ∈ A_y y, q ≤ p := by
     sorry
-  have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by
-    sorry
-  have hA₃ : ∀ y ∈ B, ∃ q : ℕ, ∀ p ∈ A_y y, q ≤ p := by
-    sorry
-
-  let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p }
+/-
+> Define `C = {q_y | y ∈ ran f}`.
+-/
+  let C := { q | ∃ y, y ∈ f '' A ∧ (∀ p ∈ A_y y, q ≤ p) }
+/-
+> Thus `h : C → ran f` given by `h(x) = f(g(x))` is a one-to-on ecorrespondence
+> between `C` and `ran f` by construction. That is, `C ≈ ran f`.
+-/
   let h x := f (g x)
   have hh : C ≈ f '' A := by
     sorry
-
+/-
+> By *Lemma 6F*, there exists some `n ≤ m` such that `C ≈ n`. By *Theorem 6A*,
+> `n ≈ ran f`.
+-/
   sorry
 
 /-- ### Set Difference Size
@@ -992,7 +1045,7 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α]
       simp only [Set.diff_empty]
       exact hA
     rw [this]
-    refine ⟨by simp, hB', Set.equinumerous_emptyset_emptyset⟩
+    refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩
   | succ m ih =>
 /-
 > #### (ii)

Common/List/Basic.lean

@@ -162,7 +162,7 @@ theorem length_zipWith_self_tail_eq_length_sub_one
   rw [length_zipWith]
   simp only [length_cons, ge_iff_le, min_eq_right_iff]
   show length as ≤ length as + 1
-  simp only [le_add_iff_nonneg_right, zero_le]
+  simp only [le_add_iff_nonneg_right]
 
 /--
 The output `List` of a `zipWith` is nonempty **iff** both of its inputs are

Common/Nat/Basic.lean

@@ -9,4 +9,23 @@ If `n < m⁺`, then `n < m` or `n = m`.
 theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m ∨ n = m :=
   lt_or_eq_of_le (lt_succ.mp h)
 
+/--
+The following cancellation law holds for `m`, `n`, and `p` in `ω`:
+```
+m ⬝ p = n ⬝ p ∧ p ≠ 0 → m = n
+```
+-/
+theorem mul_right_cancel (m n p : ℕ) (hp : 0 < p) : m * p = n * p → m = n := by
+  intro hmn
+  match @trichotomous ℕ LT.lt _ m n with
+  | Or.inl h =>
+    have : m * p < n * p := Nat.mul_lt_mul_of_pos_right h hp
+    rw [hmn] at this
+    simp at this
+  | Or.inr (Or.inl h) => exact h
+  | Or.inr (Or.inr h) =>
+    have : n * p < m * p := Nat.mul_lt_mul_of_pos_right h hp
+    rw [hmn] at this
+    simp at this
+
 end Nat

Common/Real/Floor.lean

@@ -1,5 +1,6 @@
 import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.Data.Real.Archimedean
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Finset.Basic
 
 /-! # Common.Real.Floor
 

DocGen4.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Process
+import DocGen4.Load
+import DocGen4.Output
+import DocGen4.LeanInk

DocGen4/LeanInk.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.LeanInk.Process
+import DocGen4.LeanInk.Output

DocGen4/LeanInk/Output.lean

@@ -0,0 +1,215 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Xubai Wang
+-/
+import DocGen4.Output.Base
+import DocGen4.Output.ToHtmlFormat
+import Lean.Data.Json
+import LeanInk.Annotation.Alectryon
+
+namespace LeanInk.Annotation.Alectryon
+
+open DocGen4 Output
+open scoped DocGen4.Jsx
+
+structure AlectryonContext where
+  counter : Nat
+
+abbrev AlectryonT := StateT AlectryonContext
+abbrev AlectryonM := AlectryonT HtmlM
+
+def getNextButtonLabel : AlectryonM String := do
+  let val ← get
+  let newCounter := val.counter + 1
+  set { val with counter := newCounter }
+  return s!"plain-lean4-lean-chk{val.counter}"
+
+def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
+  pure
+    <div class="alectryon-type-info-wrapper">
+      <small class="alectryon-type-info">
+        <div class="alectryon-goals">
+          <blockquote class="alectryon-goal">
+            <div class="goal-hyps">
+              <span class="hyp-type">
+                <var>{tyi.name}</var>
+                <b>: </b>
+                <span>[← DocGen4.Output.infoFormatToHtml tyi.type.fst]</span>
+              </span>
+            </div>
+          </blockquote>
+        </div>
+      </small>
+    </div>
+
+def Token.processSemantic (t : Token) : Html :=
+  match t.semanticType with
+  | some "Name.Attribute" => <span class="na">{t.raw}</span>
+  | some "Name.Variable" => <span class="nv">{t.raw}</span>
+  | some "Keyword" => <span class="k">{t.raw}</span>
+  | _ => Html.text t.raw
+
+def Token.toHtml (t : Token) : AlectryonM Html := do
+  -- Right now t.link is always none from LeanInk, ignore it
+  -- TODO: render docstring
+  let mut parts := #[]
+  if let some tyi := t.typeinfo then
+    parts := parts.push <| ← tyi.toHtml
+
+  parts := parts.push t.processSemantic
+
+  pure
+    -- TODO: Show rest of token
+    <span class="alectryon-token">
+      [parts]
+    </span>
+
+def Contents.toHtml : Contents → AlectryonM Html
+  | .string value =>
+    pure
+      <span class="alectryon-wsp">
+        {value}
+      </span>
+  | .experimentalTokens values => do
+    let values ← values.mapM Token.toHtml
+    pure
+      <span class="alectryon-wsp">
+        [values]
+      </span>
+
+def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
+  let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]</var>]
+  if h.body.snd != "" then
+    hypParts := hypParts.push
+      <span class="hyp-body">
+        <b>:= </b>
+        <span>[← infoFormatToHtml h.body.fst]</span>
+      </span>
+  hypParts := hypParts.push
+      <span class="hyp-type">
+        <b>: </b>
+        <span >[← infoFormatToHtml h.type.fst]</span>
+      </span>
+
+  pure
+    <span>
+      [hypParts]
+    </span>
+
+def Goal.toHtml (g : Goal) : AlectryonM Html := do
+  let mut hypotheses := #[]
+  for hyp in g.hypotheses do
+    let rendered ← hyp.toHtml
+    hypotheses := hypotheses.push rendered
+    hypotheses := hypotheses.push <br/>
+  let conclusionHtml ←
+    match g.conclusion with
+    | .typed info _ => infoFormatToHtml info
+    | .untyped str => pure #[Html.text str]
+
+  pure
+    <blockquote class="alectryon-goal">
+      <div class="goal-hyps">
+        [hypotheses]
+      </div>
+      <span class="goal-separator">
+        <hr><span class="goal-name">{g.name}</span></hr>
+      </span>
+      <div class="goal-conclusion">
+        [conclusionHtml]
+      </div>
+    </blockquote>
+
+def Message.toHtml (m : Message) : AlectryonM Html := do
+  pure
+    <blockquote class="alectryon-message">
+      -- TODO: This might have to be done in a fancier way
+      {m.contents}
+    </blockquote>
+
+def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
+  let messages :=
+    if s.messages.size > 0 then
+      #[
+        <div class="alectryon-messages">
+          [← s.messages.mapM Message.toHtml]
+        </div>
+      ]
+    else
+      #[]
+  
+  let goals :=
+    if s.goals.size > 0 then
+      -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
+      #[
+        <div class="alectryon-goals">
+          [← s.goals.mapM Goal.toHtml]
+        </div>
+      ]
+    else
+      #[]
+
+  let buttonLabel ← getNextButtonLabel
+
+  pure
+    <span class="alectryon-sentence">
+      <input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/>
+      <label class="alectryon-input" for={buttonLabel}>
+        {← s.contents.toHtml}
+      </label>
+      <small class="alectryon-output">
+        [messages]
+        [goals]
+      </small>
+    </span>
+
+def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
+
+def Fragment.toHtml : Fragment → AlectryonM Html
+  | .text value => value.toHtml
+  | .sentence value => value.toHtml
+
+def baseHtml (content : Array Html) : AlectryonM Html := do
+  let banner :=
+    <div «class»="alectryon-banner">
+      Built with <a href="https://github.com/leanprover/doc-gen4">doc-gen4</a>, running Lean4.
+      Bubbles (<span class="alectryon-bubble"></span>) indicate interactive fragments: hover for details, tap to reveal contents.
+      Use <kbd>Ctrl+↑</kbd> <kbd>Ctrl+↓</kbd> to navigate, <kbd>Ctrl+🖱️</kbd> to focus.
+      On Mac, use <kbd>Cmd</kbd> instead of <kbd>Ctrl</kbd>.
+    </div>
+
+  pure
+    <html lang="en" class="alectryon-standalone">
+      <head>
+        <meta charset="UTF-8"/>
+        <meta name="viewport" content="width=device-width, initial-scale=1"/>
+
+        <link rel="stylesheet" href={s!"{← getRoot}src/alectryon.css"}/>
+        <link rel="stylesheet" href={s!"{← getRoot}src/pygments.css"}/>
+        <link rel="stylesheet" href={s!"{← getRoot}src/docutils_basic.css"}/>
+        <link rel="shortcut icon" href={s!"{← getRoot}favicon.ico"}/>
+
+        <script defer="true" src={s!"{← getRoot}src/alectryon.js"}></script>
+      </head>
+      <body>
+        <article class="alectryon-root alectryon-centered">
+          {banner}
+          <pre class="alectryon-io highlight">
+            [content]
+          </pre>
+        </article>
+      </body>
+    </html>
+
+def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
+  let config ← read
+  annotateFileWithCompounds [] config.inputFileContents as
+
+-- TODO: rework monad mess
+def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
+  let fs ← annotationsToFragments as
+  let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
+  return html
+
+end LeanInk.Annotation.Alectryon

DocGen4/LeanInk/Process.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import LeanInk.Analysis
+import LeanInk.Annotation
+import DocGen4.LeanInk.Output
+import DocGen4.Output.Base
+
+namespace DocGen4.Process.LeanInk
+
+open Lean
+open DocGen4.Output
+
+def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
+  let some modName ← getCurrentName | unreachable!
+  let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
+  let srcDir := moduleNameToDirectory srcBasePath modName
+  let srcPath := moduleNameToFile srcBasePath modName
+  IO.FS.createDirAll srcDir
+  IO.FS.writeFile srcPath srcHtml.toString
+  return 0
+
+def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
+  let ctx ← readThe SiteContext
+  let baseCtx ← readThe SiteBaseContext
+  let outputFn := (docGenOutput · |>.run ctx baseCtx)
+  return ← LeanInk.Analysis.runAnalysis {
+    name := "doc-gen4"
+    genOutput := outputFn
+  }
+
+def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
+  execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config
+
+@[implemented_by enableInitializersExecution]
+private def enableInitializersExecutionWrapper : IO Unit := return ()
+
+def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
+  let contents ← IO.FS.readFile sourceFilePath
+  let config := {
+    inputFilePath := sourceFilePath
+    inputFileContents := contents
+    lakeFile := none
+    verbose := false
+    prettifyOutput := true
+    experimentalTypeInfo := true
+    experimentalDocString := true
+    experimentalSemanticType := true
+  }
+  enableInitializersExecutionWrapper
+  if (← execAux config) != 0 then
+    throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
+
+end DocGen4.Process.LeanInk

DocGen4/Load.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+import DocGen4.Process
+import Lean.Data.HashMap
+
+namespace DocGen4
+
+open Lean System IO
+
+def envOfImports (imports : Array Name) : IO Environment := do
+ importModules (imports.map (Import.mk · false)) Options.empty
+
+def loadInit (imports : Array Name) : IO Hierarchy := do
+ let env ← envOfImports imports
+ pure <| Hierarchy.fromArray env.header.moduleNames
+
+/--
+Load a list of modules from the current Lean search path into an `Environment`
+to process for documentation.
+-/
+def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
+  initSearchPath (← findSysroot)
+  let env ← envOfImports task.getLoad
+  let config := {
+    -- TODO: parameterize maxHeartbeats
+    maxHeartbeats := 100000000,
+    options := ⟨[(`pp.tagAppFns, true)]⟩,
+    -- TODO: Figure out whether this could cause some bugs
+    fileName := default,
+    fileMap := default,
+  }
+
+  Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
+
+def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
+  load <| .loadAll #[`Init, `Lean, `Lake]
+
+end DocGen4

DocGen4/Output.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import DocGen4.Process
+import DocGen4.Output.Base
+import DocGen4.Output.Index
+import DocGen4.Output.Module
+import DocGen4.Output.NotFound
+import DocGen4.Output.Find
+import DocGen4.Output.SourceLinker
+import DocGen4.Output.Search
+import DocGen4.Output.ToJson
+import DocGen4.Output.FoundationalTypes
+import DocGen4.LeanInk.Process
+import Lean.Data.HashMap
+
+namespace DocGen4
+
+open Lean IO System Output Process
+
+def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
+  let findBasePath := basePath / "find"
+
+  -- Base structure
+  FS.createDirAll basePath
+  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 foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
+  let navbarHtml := ReaderT.run navbar config |>.toString
+  let searchHtml := ReaderT.run search config |>.toString
+  let docGenStatic := #[
+    ("style.css", styleCss),
+    ("declaration-data.js", declarationDataCenterJs),
+    ("color-scheme.js", colorSchemeJs),
+    ("nav.js", navJs),
+    ("jump-src.js", jumpSrcJs),
+    ("expand-nav.js", expandNavJs),
+    ("how-about.js", howAboutJs),
+    ("search.html", searchHtml),
+    ("search.js", searchJs),
+    ("mathjax-config.js", mathjaxConfigJs),
+    ("instances.js", instancesJs),
+    ("importedBy.js", importedByJs),
+    ("index.html", indexHtml),
+    ("foundational_types.html", foundationalTypesHtml),
+    ("404.html", notFoundHtml),
+    ("navbar.html", navbarHtml)
+  ]
+  for (fileName, content) in docGenStatic do
+    FS.writeFile (basePath / fileName) content
+
+  let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString
+  let findStatic := #[
+    ("index.html", findHtml),
+    ("find.js", findJs)
+  ]
+  for (fileName, content) in findStatic do
+    FS.writeFile (findBasePath / fileName) content
+
+  let alectryonStatic := #[
+    ("alectryon.css", alectryonCss),
+    ("alectryon.js", alectryonJs),
+    ("docutils_basic.css", docUtilsCss),
+    ("pygments.css", pygmentsCss)
+  ]
+
+  for (fileName, content) in alectryonStatic do
+    FS.writeFile (srcBasePath / fileName) content
+
+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) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
+  let config : SiteContext := {
+    result := result,
+    sourceLinker := ← SourceLinker.sourceLinker gitUrl?
+    leanInkEnabled := ink
+  }
+
+  FS.createDirAll basePath
+  FS.createDirAll declarationsBasePath
+
+  let some p := (← IO.getEnv "LEAN_SRC_PATH") | throw <| IO.userError "LEAN_SRC_PATH not found in env"
+  let sourceSearchPath := System.SearchPath.parse p
+
+  discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
+
+  for (modName, module) in result.moduleInfo.toArray do
+    let fileDir := moduleNameToDirectory basePath modName
+    let filePath := moduleNameToFile basePath modName
+    -- path: 'basePath/module/components/till/last.html'
+    -- The last component is the file name, so we drop it from the depth to root.
+    let baseConfig := { baseConfig with
+      depthToRoot := modName.components.dropLast.length
+      currentName := some modName
+    }
+    let moduleHtml := moduleToHtml module |>.run config baseConfig
+    FS.createDirAll fileDir
+    FS.writeFile filePath moduleHtml.toString
+    if ink then
+      if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
+        -- path: 'basePath/src/module/components/till/last.html'
+        -- The last component is the file name, however we are in src/ here so dont drop it this time
+        let baseConfig := {baseConfig with depthToRoot := modName.components.length }
+        Process.LeanInk.runInk inputPath |>.run config baseConfig
+
+def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
+  return {
+    depthToRoot := 0,
+    currentName := none,
+    hierarchy
+  }
+
+def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
+  htmlOutputSetup baseConfig
+
+  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
+`AnalyzerResult`.
+-/
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
+  let baseConfig ← getSimpleBaseContext hierarchy
+  htmlOutputResults baseConfig result gitUrl? ink
+  htmlOutputIndex baseConfig
+
+end DocGen4

DocGen4/Output/Base.lean

@@ -0,0 +1,278 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Process
+import DocGen4.Output.ToHtmlFormat
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+open Lean System Widget Elab Process
+
+def basePath := FilePath.mk "." / "build" / "doc"
+def srcBasePath := basePath / "src"
+def declarationsBasePath := basePath / "declarations"
+
+/--
+The context used in the `BaseHtmlM` monad for HTML templating.
+-/
+structure SiteBaseContext where
+
+  /--
+  The module hierarchy as a tree structure.
+  -/
+  hierarchy : Hierarchy
+  /--
+  How far away we are from the page root, used for relative links to the root.
+  -/
+  depthToRoot: Nat
+  /--
+  The name of the current module if there is one, there exist a few
+  pages that don't have a module name.
+  -/
+  currentName : Option Name
+
+/--
+The context used in the `HtmlM` monad for HTML templating.
+-/
+structure SiteContext where
+  /--
+  The full analysis result from the Process module.
+  -/
+  result : AnalyzerResult
+  /--
+  A function to link declaration names to their source URLs, usually Github ones.
+  -/
+  sourceLinker : Name → Option DeclarationRange → String
+  /--
+  Whether LeanInk is enabled
+  -/
+  leanInkEnabled : Bool
+
+def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
+
+abbrev BaseHtmlT := ReaderT SiteBaseContext
+abbrev BaseHtmlM := BaseHtmlT Id
+
+abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
+abbrev HtmlM := HtmlT Id
+
+def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
+  ReaderT.run x ctx |>.run baseCtx
+
+def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
+  ReaderT.run x ctx |>.run baseCtx |>.run
+
+instance [Monad m] : MonadLift HtmlM (HtmlT m) where
+  monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
+
+instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
+  monadLift x := do return x.run (← readThe SiteBaseContext)
+
+/--
+Obtains the root URL as a relative one to the current depth.
+-/
+def getRoot : BaseHtmlM String := do
+  let rec go: Nat -> String
+  | 0 => "./"
+  | Nat.succ n' => "../" ++ go n'
+  let d <- SiteBaseContext.depthToRoot <$> read
+  return (go d)
+
+def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy
+def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
+def getResult : HtmlM AnalyzerResult := do return (← read).result
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
+def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
+
+/--
+If a template is meant to be extended because it for example only provides the
+header but no real content this is the way to fill the template with content.
+This is untyped so HtmlM and BaseHtmlM can be mixed.
+-/
+def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β :=
+  new >>= base
+
+def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β :=
+  new >>= (monadLift ∘ base)
+
+/-
+Returns the doc-gen4 link to a module `NameExt`.
+-/
+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 moduleNameToHtmlLink (n : Name) : BaseHtmlM String :=
+  moduleNameExtToLink ⟨n, .html⟩
+
+/--
+Returns the HTML doc-gen4 link to a module name.
+-/
+def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
+  return <a href={← moduleNameToHtmlLink module}>{module.toString}</a>
+
+/--
+Returns the LeanInk link to a module name.
+-/
+def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
+  let parts := "src" :: n.components.map Name.toString
+  return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
+/--
+Returns the path to the HTML file that contains information about a module.
+-/
+def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
+  let parts := n.components.map Name.toString
+  FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
+
+/--
+Returns the directory of the HTML file that contains information about a module.
+-/
+def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
+  let parts := n.components.dropLast.map Name.toString
+  basePath / parts.foldl (· / ·) (FilePath.mk ".")
+
+section Static
+/-!
+The following section contains all the statically included files that
+are used in documentation generation, notably JS and CSS ones.
+-/
+  def styleCss : String := include_str "../../static/style.css"
+  def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
+  def colorSchemeJs : String := include_str "../../static/color-scheme.js"
+  def jumpSrcJs : String := include_str "../../static/jump-src.js"
+  def navJs : String := include_str "../../static/nav.js"
+  def expandNavJs : String := include_str "../../static/expand-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"
+
+  def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
+  def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
+  def docUtilsCss : String  := include_str "../../static/alectryon/docutils_basic.css"
+  def pygmentsCss : String  := include_str "../../static/alectryon/pygments.css"
+end Static
+
+/--
+Returns the doc-gen4 link to a declaration name.
+-/
+def declNameToLink (name : Name) : HtmlM String := do
+  let res ← getResult
+  let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
+  return (← moduleNameToHtmlLink module) ++ "#" ++ name.toString
+
+/--
+Returns the HTML doc-gen4 link to a declaration name.
+-/
+def declNameToHtmlLink (name : Name) : HtmlM Html := do
+  return <a href={← declNameToLink name}>{name.toString}</a>
+
+/--
+Returns the LeanInk link to a declaration name.
+-/
+def declNameToInkLink (name : Name) : HtmlM String := do
+  let res ← getResult
+  let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
+  return (← moduleNameToInkLink module) ++ "#" ++ name.toString
+
+/--
+Returns a name splitted into parts.
+Together with "break_within" CSS class this helps browser to break a name
+nicely.
+-/
+def breakWithin (name: String) : (Array Html) :=
+  name.splitOn "."
+    |> .map (fun (s: String) => <span class="name">{s}</span>)
+    |> .intersperse "."
+    |> List.toArray
+
+/--
+Returns the HTML doc-gen4 link to a declaration name with "break_within"
+set as class.
+-/
+def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
+  return <a class="break_within" href={← declNameToLink name}>
+      [breakWithin name.toString]
+    </a>
+
+/--
+In Lean syntax declarations the following pattern is quite common:
+```
+syntax term " + " term : term
+```
+that is, we place spaces around the operator in the middle. When the
+`InfoTree` framework provides us with information about what source token
+corresponds to which identifier it will thus say that `" + "` corresponds to
+`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
+only `+` should be linked, taking care of this is what this function is
+responsible for.
+-/
+def splitWhitespaces (s : String) : (String × String × String) := Id.run do
+  let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
+  let mut s := s.trimLeft
+  let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
+  s := s.trimRight
+  (front, s, back)
+
+/--
+Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
+information about what the identifiers mean, into an HTML object that links
+to as much information as possible.
+-/
+partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
+  match i with
+  | .text t => return #[Html.escape t]
+  | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[]
+  | .tag a t =>
+    match a.info.val.info with
+    | Info.ofTermInfo i =>
+      let cleanExpr :=  i.expr.consumeMData
+      match cleanExpr with
+      | .const name _ =>
+        -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
+        -- find a better solution
+        if (← getResult).name2ModIdx.contains name then
+          match t with
+          | .text t =>
+            let (front, t, back) := splitWhitespaces <| Html.escape t
+            let elem := <a href={← declNameToLink name}>{t}</a>
+            return #[Html.text front, elem, Html.text back]
+          | _ =>
+            return #[<a href={← declNameToLink name}>[← infoFormatToHtml t]</a>]
+        else
+         return #[<span class="fn">[← infoFormatToHtml t]</span>]
+      | .sort _ =>
+        match t with
+        | .text t =>
+          let sortPrefix :: rest := t.splitOn " " | unreachable!
+          let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
+          let mut restStr := String.intercalate " " rest
+          if restStr.length != 0 then
+            restStr := " " ++ restStr
+          return #[sortLink, Html.text restStr]
+        | _ =>
+          return #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
+      | _ =>
+         return #[<span class="fn">[← infoFormatToHtml t]</span>]
+    | _ => return #[<span class="fn">[← infoFormatToHtml t]</span>]
+
+def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
+  return #[
+    <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}src/pygments.css"}/>,
+    <link rel="shortcut icon" href={s!"{← getRoot}favicon.ico"}/>,
+    <link rel="prefetch" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
+  ]
+
+end DocGen4.Output

DocGen4/Output/Class.lean

@@ -0,0 +1,22 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Structure
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def classInstancesToHtml (className : Name) : HtmlM Html := do
+  pure
+    <details «class»="instances">
+        <summary>Instances</summary>
+        <ul id={s!"instances-list-{className}"} class="instances-list"></ul>
+    </details>
+
+def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
+  structureToHtml i
+
+end Output
+end DocGen4

DocGen4/Output/ClassInductive.lean

@@ -0,0 +1,14 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Class
+import DocGen4.Output.Inductive
+import DocGen4.Process
+
+
+namespace DocGen4
+namespace Output
+
+def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
+  inductiveToHtml i
+
+end Output
+end DocGen4

DocGen4/Output/Definition.lean

@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean Widget
+
+/-- This is basically an arbitrary number that seems to work okay. -/
+def equationLimit : Nat := 200
+
+def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
+  return <li class="equation">[← infoFormatToHtml c]</li>
+
+/--
+Attempt to render all `simp` equations for this definition. At a size
+defined in `equationLimit` we stop trying since they:
+- are too ugly to read most of the time
+- take too long
+-/
+def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
+  if let some eqs := i.equations then
+    let equationsHtml ← eqs.mapM equationToHtml
+    let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit)
+    if equationsHtml.size ≠ filteredEquationsHtml.size then
+      return #[
+        <details>
+          <summary>Equations</summary>
+          <ul class="equations">
+            <li class="equation">One or more equations did not get rendered due to their size.</li>
+            [filteredEquationsHtml]
+          </ul>
+        </details>
+      ]
+    else
+      return #[
+        <details>
+          <summary>Equations</summary>
+          <ul class="equations">
+            [filteredEquationsHtml]
+          </ul>
+        </details>
+      ]
+  else
+    return #[]
+
+end Output
+end DocGen4
+

DocGen4/Output/DocString.lean

@@ -0,0 +1,220 @@
+import CMark
+import DocGen4.Output.Template
+import Lean.Data.Parsec
+import UnicodeBasic
+
+open Lean Xml Parser Parsec DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+/-- Auxiliary function for `splitAround`. -/
+@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String :=
+  if s.atEnd i then
+    let r := (s.extract b i)::r
+    r.reverse
+  else
+    let c := s.get i
+    if p c then
+      let i := s.next i
+      splitAroundAux s p i i (c.toString::s.extract b (i-⟨1⟩)::r)
+    else
+      splitAroundAux s p b (s.next i) r
+
+/--
+  Similar to `String.split` in Lean core, but keeps the separater.
+  e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
+-/
+def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
+
+instance : Inhabited Element := ⟨"", Lean.RBMap.empty, #[]⟩
+
+/-- Parse an array of Xml/Html document from String. -/
+def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
+
+/--
+  Generate id for heading elements, with the following rules:
+
+  1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved.
+  2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash.
+  3. Cases (upper and lower) are preserved.
+  4. Xml/Html tags are ignored.
+-/
+partial def xmlGetHeadingId (el : Xml.Element) : String :=
+  elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
+  where
+    elementToPlainText el := match el with
+    | (Element.Element _ _ contents) =>
+      "".intercalate (contents.toList.map contentToPlainText)
+    contentToPlainText c := match c with
+    | Content.Element el => elementToPlainText el
+    | Content.Comment _ => ""
+    | Content.Character s => s
+    replaceCharSeq pattern replacement s :=
+      s.split pattern
+      |>.filter (!·.isEmpty)
+      |> replacement.intercalate
+    unicodeToDrop (c : Char) : Bool :=
+      let cats := [
+        Unicode.GeneralCategory.P, -- punctuation
+        Unicode.GeneralCategory.Z, -- separator
+        Unicode.GeneralCategory.C -- other
+      ]
+      cats.any (Unicode.isInGeneralCategory c)
+
+/--
+  This function try to find the given name, both globally and in current module.
+
+  For global search, a precise name is need. If the global search fails, the function
+  tries to find a local one that ends with the given search name.
+-/
+def nameToLink? (s : String) : HtmlM (Option String) := do
+  let res ← getResult
+  if s.endsWith ".lean" && s.contains '/' then
+    return (← getRoot) ++ s.dropRight 5 ++ ".html"
+  else if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
+    -- with exactly the same name
+    if res.name2ModIdx.contains name then
+      declNameToLink name
+    -- module name
+    else if res.moduleNames.contains name then
+      moduleNameToHtmlLink name
+    -- find similar name in the same module
+    else
+      match (← getCurrentName) with
+      | some currentName =>
+        match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
+        | some info =>
+          declNameToLink info.getName
+        | _ => return none
+      | _ => return none
+  else
+    return none
+  where
+    -- check if two names have the same ending components
+    sameEnd n1 n2 :=
+      List.zip n1.componentsRev n2.componentsRev
+      |>.all fun ⟨a, b⟩ => a == b
+
+/--
+  Extend links with following rules:
+
+  1. if the link starts with `##`, a name search is used and will panic if not found
+  2. if the link starts with `#`, it's treated as id link, no modification
+  3. if the link starts with `http`, it's an absolute one, no modification
+  4. otherwise it's a relative link, extend it with base url
+-/
+def extendLink (s : String)  : HtmlM String := do
+  -- for intra doc links
+  if s.startsWith "##" then
+    if let some link ← nameToLink? (s.drop 2) then
+      return link
+    else
+      panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
+  -- for id
+  else if s.startsWith "#" then
+    return s
+  -- for absolute and relative urls
+  else if s.startsWith "http" then
+    return s
+  else return ((← getRoot) ++ s)
+
+/-- Add attributes for heading. -/
+def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents => do
+    let id := xmlGetHeadingId el
+    let anchorAttributes := Lean.RBMap.empty
+      |>.insert "class" "hover-link"
+      |>.insert "href" s!"#{id}"
+    let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
+    let newAttrs := attrs
+      |>.insert "id" id
+      |>.insert "class" "markdown-heading"
+    let newContents := (←
+      contents.mapM (fun c => match c with
+      | Content.Element e => return Content.Element (← modifyElement e)
+      | _ => pure c))
+      |>.push (Content.Character " ")
+      |>.push (Content.Element anchor)
+    return ⟨ name, newAttrs, newContents⟩
+
+/-- Extend anchor links. -/
+def extendAnchor (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let newAttrs ← match attrs.find? "href" with
+    | some href => pure (attrs.insert "href" (← extendLink href))
+    | none => pure attrs
+    return ⟨ name, newAttrs, contents⟩
+
+/-- Automatically add intra documentation link for inline code span. -/
+def autoLink (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let mut newContents := #[]
+    for c in contents do
+      match c with
+      | Content.Character s =>
+        newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
+      | _ => newContents := newContents.push c
+    return ⟨ name, attrs, newContents ⟩
+  where
+    linkify s := do
+      let link? ← nameToLink? s
+      match link? with
+      | some link =>
+        let attributes := Lean.RBMap.empty.insert "href" link
+        return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
+      | none =>
+        let sHead := s.dropRightWhile (· != '.')
+        let sTail := s.takeRightWhile (· != '.')
+        let link'? ← nameToLink? sTail
+        match link'? with
+        | some link' =>
+          let attributes := Lean.RBMap.empty.insert "href" link'
+          return [
+            Content.Character sHead,
+            Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
+          ]
+        | none =>
+          return [Content.Character s]
+    unicodeToSplit (c : Char) : Bool :=
+      let cats := [
+        Unicode.GeneralCategory.Z, -- separator
+        Unicode.GeneralCategory.C -- other
+      ]
+      cats.any (Unicode.isInGeneralCategory c)
+
+/-- Core function of modifying the cmark rendered docstring html. -/
+partial def modifyElement (element : Element) : HtmlM Element :=
+  match element with
+  | el@(Element.Element name attrs contents) => do
+    -- add id and class to <h_></h_>
+    if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
+      addHeadingAttributes el modifyElement
+    -- extend relative href for <a></a>
+    else if name = "a" then
+      extendAnchor el
+    -- auto link for inline <code></code>
+    else if name = "code" ∧
+      -- don't linkify code blocks explicitly tagged with a language other than lean
+      (((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
+      autoLink el
+    -- recursively modify
+    else
+      let newContents ← contents.mapM fun c => match c with
+        | Content.Element e => return Content.Element (← modifyElement e)
+        | _ => pure c
+      return ⟨ name, attrs, newContents ⟩
+
+/-- Convert docstring to Html. -/
+def docStringToHtml (s : String) : HtmlM (Array Html) := do
+  let rendered := CMark.renderHtml (Html.escape s)
+  match manyDocument rendered.mkIterator with
+  | Parsec.ParseResult.success _ res =>
+    res.mapM fun x => do return Html.text <| toString (← modifyElement x)
+  | _ => return #[Html.text rendered]
+
+end Output
+end DocGen4

DocGen4/Output/Find.lean

@@ -0,0 +1,22 @@
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def find : BaseHtmlM Html := do
+  pure
+    <html lang="en">
+      <head>
+        <link rel="preload" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
+        <script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
+        <script type="module" async="true" src="./find.js"></script>
+      </head>
+      <body></body>
+    </html>
+
+end Output
+end DocGen4
+

DocGen4/Output/FoundationalTypes.lean

@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Inductive
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+
+def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
+  pure <|
+    <main>
+      <a id="top"></a>
+      <h1>Foundational Types</h1>
+
+      <p>Some of Lean's types are not defined in any Lean source files (even the <code>prelude</code>) since they come from its foundational type theory. This page provides basic documentation for these types.</p>
+      <p>For a more in-depth explanation of Lean's type theory, refer to
+      <a href="https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html">TPiL</a>.</p>
+      
+      
+      <h2 id="codesort-ucode"><code>Sort u</code></h2>
+      <p><code>Sort u</code> is the type of types in Lean, and <code>Sort u : Sort (u + 1)</code>.</p>
+      {← instancesForToHtml `_builtin_sortu}
+    
+      <h2 id="codetype-ucode"><code>Type u</code></h2>
+      <p><code>Type u</code> is notation for <code>Sort (u + 1)</code>.</p>    
+      {← instancesForToHtml `_builtin_typeu}
+      
+      <h2 id="codepropcode"><code>Prop</code></h2>
+      <p><code>Prop</code> is notation for <code>Sort 0</code>.</p>    
+      {← instancesForToHtml `_builtin_prop}
+    
+      <h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"(a : α) → β a"}</code></h2>
+      <p>The type of dependent functions is known as a pi type.
+      Non-dependent functions and implications are a special case.</p>
+      <p>Note that these can also be written with the alternative notations:</p>
+      <ul>
+      <li><code>∀ a : α, β a</code>, conventionally used where <code>β a : Prop</code>.</li>
+      <li><code>(a : α) → β a</code></li>
+      <li><code>α → γ</code>, possible only if <code>β a = γ</code> for all <code>a</code>.</li>
+      </ul>
+      <p>Lean also permits ASCII-only spellings of the three variants:</p>
+      <ul>
+      <li><code>forall a : A, B a</code> for <code>{"∀ a : α, β a"}</code></li>
+      <li><code>(a : A) -&gt; B a</code>, for <code>(a : α) → β a</code></li>
+      <li><code>A -&gt; B</code>, for <code>α → β</code></li>
+      </ul>
+      <p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
+      <code>{"fun α β, α → β"}</code>.</p>    
+      -- TODO: instances for pi types 
+    </main>
+
+end DocGen4.Output

DocGen4/Output/Index.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
+  pure <|
+    <main>
+      <a id="top"></a>
+      <h1>Bookshelf</h1>
+      <p>
+        A study of the books listed below. Most proofs are conducted in LaTeX.
+        Where feasible, theorems are also formally proven in
+        <a target="_blank" href="https://leanprover.github.io/">Lean</a>.
+      </p>
+
+      <h2>In Progress</h2>
+      <ul>
+        <li><a href={s!"{← getRoot}Bookshelf/Apostol.html"}>Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Logic.html"}>Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Set.html"}>Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Fraleigh.html"}>Fraleigh, John B. A First Course in Abstract Algebra, n.d.</a></li>
+      </ul>
+
+      <h2>Complete</h2>
+      <ul>
+        <li><a href={s!"{← getRoot}Bookshelf/Avigad.html"}>Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.</a></li>
+      </ul>
+
+      <h2>Pending</h2>
+      <ul>
+        <li>Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.</li>
+        <li>Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.</li>
+        <li>Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.</li>
+        <li>Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.</li>
+        <li>Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.</li>
+        <li>Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.</li>
+      </ul>
+
+      <h2>Legend</h2>
+      <p>
+        A color/symbol code is used on generated PDF headers to indicate their
+        status:
+        <ul>
+          <li>
+            <span style="color:darkgray">Dark gray statements </span> are
+            reserved for definitions and axioms that have been encoded in LaTeX.
+            A reference to a definition in Lean may also be provided.
+          </li>
+          <li>
+            <span style="color:teal">Teal statements </span> are reserved for
+            statements, theorems, lemmas, etc. that have been proven in LaTeX
+            and have a corresponding proof in Lean.
+          </li>
+          <li>
+            <span style="color:olive">Olive statements </span> are reserved for
+            statements, theorems, lemmas, etc. that have been proven in LaTeX.
+            A reference to a statement in Lean may also be provided.
+          </li>
+          <li>
+            <span style="color:fuchsia">Fuchsia statements </span> are reserved
+            for statements, theorems, lemmas, etc. that have been proven in
+            LaTeX and <i>will </i> have a corresponding proof in Lean.
+          </li>
+          <li>
+            <span style="color:maroon">Maroon </span> serves as a catch-all for
+            statements that don't fit the above categorizations. Incomplete
+            definitions, statements without proof, etc. belong here.
+          </li>
+        </ul>
+      </p>
+      <p>This was built using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
+    </main>
+
+end Output
+end DocGen4

DocGen4/Output/Inductive.lean

@@ -0,0 +1,39 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
+  pure
+    <details «class»="instances">
+        <summary>Instances For</summary>
+        <ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
+    </details>
+
+def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+  let shortName := c.name.componentsRev.head!.toString
+  let name := c.name.toString
+  if let some doc := c.doc then
+    let renderedDoc ← docStringToHtml doc
+    pure
+      <li class="constructor" id={name}>
+        {shortName} : [← infoFormatToHtml c.type]
+        <div class="inductive_ctor_doc">[renderedDoc]</div>
+      </li>
+  else
+    pure
+      <li class="constructor" id={name}>
+        {shortName} : [← infoFormatToHtml c.type]
+      </li>
+
+def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
+  let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
+  return #[constructorsHtml]
+
+end Output
+end DocGen4

DocGen4/Output/Instance.lean

@@ -0,0 +1,8 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Definition
+
+namespace DocGen4
+namespace Output
+
+end Output
+end DocGen4

DocGen4/Output/Module.lean

@@ -0,0 +1,219 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.Template
+import DocGen4.Output.Inductive
+import DocGen4.Output.Structure
+import DocGen4.Output.Class
+import DocGen4.Output.Definition
+import DocGen4.Output.Instance
+import DocGen4.Output.ClassInductive
+import DocGen4.Output.DocString
+import DocGen4.Process
+import Lean.Data.Xml.Parser
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean Process
+
+/--
+Render an `Arg` as HTML, adding opacity effects etc. depending on what
+type of binder it has.
+-/
+def argToHtml (arg : Arg) : HtmlM Html := do
+  let (l, r, implicit) := match arg.binderInfo with
+  | BinderInfo.default => ("(", ")", false)
+  | BinderInfo.implicit => ("{", "}", true)
+  | BinderInfo.strictImplicit => ("⦃", "⦄", true)
+  | BinderInfo.instImplicit => ("[", "]", true)
+  let mut nodes :=
+    match arg.name with
+    | some name => #[Html.text s!"{l}{name.toString} : "]
+    | none => #[Html.text s!"{l}"]
+  nodes := nodes.append (← infoFormatToHtml arg.type)
+  nodes := nodes.push r
+  let inner := <span class="fn">[nodes]</span>
+  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+  if implicit then
+    return <span class="impl_arg">{html}</span>
+  else
+    return html
+
+/--
+Render the structures this structure extends from as HTML so it can be
+added to the top level.
+-/
+def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
+  let mut nodes := #[]
+  if s.parents.size > 0 then
+    nodes := nodes.push <span class="decl_extends">extends</span>
+    let mut parents := #[]
+    for parent in s.parents do
+      let link ← declNameToHtmlBreakWithinLink parent
+      let inner := <span class="fn">{link}</span>
+      let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
+      parents := parents.push html
+    nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
+  return nodes
+
+/--
+Render the general header of a declaration containing its declaration type
+and name.
+-/
+def docInfoHeader (doc : DocInfo) : HtmlM Html := do
+  let mut nodes := #[]
+  nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
+  nodes := nodes.push
+    <span class="decl_name">
+      {← declNameToHtmlBreakWithinLink doc.getName}
+    </span>
+  for arg in doc.getArgs do
+    nodes := nodes.push (← argToHtml arg)
+
+  match doc with
+  | DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i)
+  | DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
+  | _ => nodes := nodes
+
+  nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
+  nodes := nodes.push <div class="decl_type">[← infoFormatToHtml doc.getType]</div>
+  return <div class="decl_header"> [nodes] </div>
+
+/--
+The main entry point for rendering a single declaration inside a given module.
+-/
+def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
+  -- basic info like headers, types, structure fields, etc.
+  let docInfoHtml ← match doc with
+  | DocInfo.inductiveInfo i => inductiveToHtml i
+  | DocInfo.structureInfo i => structureToHtml i
+  | DocInfo.classInfo i => classToHtml i
+  | DocInfo.classInductiveInfo i => classInductiveToHtml i
+  | _ => 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.name]
+  | DocInfo.definitionInfo i => pure ((← equationsToHtml i) ++ #[← instancesForToHtml i.name])
+  | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
+  | DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
+  | DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
+  | DocInfo.structureInfo i => pure #[← instancesForToHtml i.name]
+  | _ => pure #[]
+  let attrs := doc.getAttrs
+  let attrsHtml :=
+    if attrs.size > 0 then
+      let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
+      #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+    else
+      #[]
+  let leanInkHtml :=
+    if ← leanInkEnabled? then
+      #[
+        <div class="ink_link">
+          <a href={← declNameToInkLink doc.getName}>ink</a>
+        </div>
+      ]
+    else
+      #[]
+
+  pure
+    <div class="decl" id={doc.getName.toString}>
+      <div class={doc.getKind}>
+        <div class="gh_link">
+          <a href={← getSourceUrl module doc.getDeclarationRange}>source</a>
+        </div>
+        [leanInkHtml]
+        [attrsHtml]
+        {← docInfoHeader doc}
+        [docInfoHtml]
+        [docStringHtml]
+        [extraInfoHtml]
+      </div>
+    </div>
+
+/--
+Rendering a module doc string, that is the ones with an ! after the opener
+as HTML.
+-/
+def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
+  pure
+    <div class="mod_doc">
+      [← docStringToHtml mdoc.doc]
+    </div>
+
+/--
+Render a module member, that is either a module doc string or a declaration
+as HTML.
+-/
+def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
+  match member with
+  | ModuleMember.docInfo d => docInfoToHtml module d
+  | ModuleMember.modDoc d => modDocToHtml d
+
+def declarationToNavLink (module : Name) : Html :=
+  <div class="nav_link">
+    <a class="break_within" href={s!"#{module.toString}"}>
+      [breakWithin module.toString]
+    </a>
+  </div>
+
+/--
+Returns the list of all imports this module does.
+-/
+def getImports (module : Name) : HtmlM (Array Name) := do
+  let res ← getResult
+  return res.moduleInfo.find! module |>.imports
+
+/--
+Sort the list of all modules this one is importing, linkify it
+and return the HTML.
+-/
+def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
+  let imports := (← getImports moduleName).qsort Name.lt
+  imports.mapM (fun i => do return <li>{← moduleToHtmlLink i}</li>)
+
+/--
+Render the internal nav bar (the thing on the right on all module pages).
+-/
+def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
+  pure
+    <nav class="internal_nav">
+      <h3><a class="break_within" href="#top">[breakWithin moduleName.toString]</a></h3>
+      <p class="gh_nav_link"><a href={← getSourceUrl moduleName none}>source</a></p>
+      <div class="imports">
+        <details>
+          <summary>Imports</summary>
+          <ul>
+            [← importsHtml moduleName]
+          </ul>
+        </details>
+        <details>
+          <summary>Imported by</summary>
+          <ul id={s!"imported-by-{moduleName}"} class="imported-by-list"> </ul>
+        </details>
+      </div>
+      [members.map declarationToNavLink]
+    </nav>
+
+/--
+The main entry point to rendering the HTML for an entire module.
+-/
+def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
+  let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
+  let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
+  let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
+  templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
+    ← internalNav memberNames module.name,
+    Html.element "main" false #[] memberDocs
+  ]
+
+end Output
+end DocGen4

DocGen4/Output/Navbar.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Base
+
+namespace DocGen4
+namespace Output
+
+open Lean
+open scoped DocGen4.Jsx
+
+def moduleListFile (file : NameExt) : BaseHtmlM Html := do
+  let contents :=
+    if file.ext == .pdf then
+      <span>{s!"🗎 {file.getString!} (<a class=\"pdf\" target=\"_blank\" href={← moduleNameExtToLink file}>pdf</a>)"}</span>
+    else
+      <a href={← moduleNameExtToLink file}>{file.getString!}</a>
+  return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}>
+    {contents}
+  </div>
+
+/--
+Build the HTML tree representing the module hierarchy.
+-/
+partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
+  let children := Array.mk (h.getChildren.toList.map Prod.snd)
+  let nodes ← children.mapM (fun c =>
+    if c.getChildren.toList.length != 0 then
+      moduleListDir c
+    else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then
+      moduleListFile (Hierarchy.getNameExt c)
+    else
+      pure ""
+  )
+  let moduleLink ← moduleNameToHtmlLink h.getName
+  let summary :=
+    if h.isFile then
+      <summary>{s!"{h.getName.getString!} ({<a href={← moduleNameToHtmlLink h.getName}>file</a>})"} </summary>
+    else
+      <summary>{h.getName.getString!}</summary>
+
+  pure
+    <details class="nav_sect" "data-path"={moduleLink} [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
+      {summary}
+      [nodes]
+    </details>
+
+/--
+Return a list of top level modules, linkified and rendered as HTML
+-/
+def moduleList : BaseHtmlM Html := do
+  let hierarchy ← getHierarchy
+  let mut list := Array.empty
+  for (_, cs) in hierarchy.getChildren do
+    list := list.push <| ← moduleListDir cs
+  return <div class="module_list">[list]</div>
+
+/--
+The main entry point to rendering the navbar on the left hand side.
+-/
+def navbar : BaseHtmlM Html := do
+  pure
+    <html lang="en">
+      <head>
+        [← baseHtmlHeadDeclarations]
+
+        <script type="module" src={s!"{← getRoot}nav.js"}></script>
+        <script type="module" src={s!"{← getRoot}color-scheme.js"}></script>
+        <base target="_parent" />
+      </head>
+
+      <body>
+        <div class="navframe">
+        <nav class="nav">
+          <h3>General documentation</h3>
+          <div class="nav_link"><a href={s!"{← getRoot}"}>index</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}foundational_types.html"}>foundational types</a></div>
+          /-
+          TODO: Add these in later
+          <div class="nav_link"><a href={s!"{← getRoot}tactics.html"}>tactics</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}commands.html"}>commands</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}hole_commands.html"}>hole commands</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}attributes.html"}>attributes</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}notes.html"}>notes</a></div>
+          <div class="nav_link"><a href={s!"{← getRoot}references.html"}>references</a></div>
+          -/
+          <h3>Library</h3>
+          {← moduleList}
+          <div id="settings" hidden="hidden">
+            -- `input` is a void tag, but can be self-closed to make parsing easier.
+            <h3>Color scheme</h3>
+            <form id="color-theme-switcher">
+                <label for="color-theme-dark">
+                    <input type="radio" name="color_theme" id="color-theme-dark" value="dark" autocomplete="off"/>dark</label>
+                <label for="color-theme-system" title="Match system theme settings">
+                    <input type="radio" name="color_theme" id="color-theme-system" value="system" autocomplete="off"/>system</label>
+                <label for="color-theme-light">
+                    <input type="radio" name="color_theme" id="color-theme-light" value="light" autocomplete="off"/>light</label>
+            </form>
+          </div>
+        </nav>
+        </div>
+      </body>
+    </html>
+
+end Output
+end DocGen4

DocGen4/Output/NotFound.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+/--
+Render the 404 page.
+-/
+def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <|
+  pure <|
+    <main>
+      <h1>404 Not Found</h1>
+      <p> Unfortunately, the page you were looking for is no longer here. </p>
+      <div id="howabout"></div>
+    </main>
+
+end Output
+end DocGen4

DocGen4/Output/Search.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2023 Jeremy Salwen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Salwen
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
+  pure <|
+    <main>
+      <h1> Search Results </h1>
+      <label for="search_page_query">Query:</label>
+      <input id="search_page_query" />
+      <div id="kinds">
+        Allowed Kinds:
+        <input type="checkbox" id="def_checkbox" class="kind_checkbox" value="def" checked="checked" />
+        <label for="def_checkbox">def</label>
+        <input type="checkbox" id="theorem_checkbox" class="kind_checkbox" value="theorem" checked="checked" />
+        <label for="theorem_checkbox">theorem</label>
+        <input type="checkbox" id="inductive_checkbox" class="kind_checkbox" value="inductive" checked="checked" />
+        <label for="inductive_checkbox">inductive</label>
+        <input type="checkbox" id="structure_checkbox" class="kind_checkbox" value="structure" checked="checked" />
+        <label for="structure_checkbox">structure</label>
+        <input type="checkbox" id="class_checkbox" class="kind_checkbox" value="class" checked="checked" />
+        <label for="class_checkbox">class</label>
+        <input type="checkbox" id="instance_checkbox" class="kind_checkbox" value="instance" checked="checked" />
+        <label for="instance_checkbox">instance</label>
+        <input type="checkbox" id="axiom_checkbox" class="axiom_checkbox" value="axiom" checked="checked" />
+        <label for="axiom_checkbox">axiom</label>
+        <input type="checkbox" id="opaque_checkbox" class="kind_checkbox" value="opaque" checked="checked" />
+        <label for="opaque_checkbox">opaque</label>
+      </div>
+      
+      <script>
+        document.getElementById("search_page_query").value = new URL(window.location.href).searchParams.get("q")
+      </script>
+      <div id="search_results">
+      </div>
+    </main>
+
+end Output
+end DocGen4

DocGen4/Output/SourceLinker.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+namespace DocGen4.Output.SourceLinker
+
+open Lean
+
+/--
+Given a lake workspace with all the dependencies as well as the hash of the
+compiler release to work with this provides a function to turn names of
+declarations into (optionally positional) Github URLs.
+-/
+def sourceLinker (gitUrl? : Option String) : IO (Name → Option DeclarationRange → String) := do
+  -- TOOD: Refactor this, we don't need to pass in the module into the returned closure
+  -- since we have one sourceLinker per module
+
+  return fun module range =>
+    let parts := module.components.map Name.toString
+    let path := String.intercalate "/" parts
+    let root := module.getRoot
+    let leanHash := Lean.githash
+    let basic := if root == `Lean ∨ root == `Init then
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+    else if root == `Lake then
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
+    else
+      gitUrl?.get!
+
+    match range with
+    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
+    | none => basic
+
+end DocGen4.Output.SourceLinker

DocGen4/Output/Structure.lean

@@ -0,0 +1,51 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import DocGen4.Process
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+/--
+Render a single field consisting of its documentation, its name and its type as HTML.
+-/
+def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
+  let shortName := f.name.componentsRev.head!.toString
+  let name := f.name.toString
+  if let some doc := f.doc then
+    let renderedDoc ← docStringToHtml doc
+    pure
+      <li id={name} class="structure_field">
+        <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
+        <div class="structure_field_doc">[renderedDoc]</div>
+      </li>
+  else
+    pure
+      <li id={name} class="structure_field">
+        <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
+      </li>
+
+/--
+Render all information about a structure as HTML.
+-/
+def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
+  let structureHtml :=
+    if Name.isSuffixOf `mk i.ctor.name then
+      (<ul class="structure_fields" id={i.ctor.name.toString}>
+        [← i.fieldInfo.mapM fieldToHtml]
+      </ul>)
+    else
+      let ctorShortName := i.ctor.name.componentsRev.head!.toString
+      (<ul class="structure_ext">
+        <li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
+        <ul class="structure_ext_fields">
+          [← i.fieldInfo.mapM fieldToHtml]
+        </ul>
+        <li class="structure_ext_ctor">)</li>
+      </ul>)
+  return #[structureHtml]
+
+end Output
+end DocGen4

DocGen4/Output/Template.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import DocGen4.Output.ToHtmlFormat
+import DocGen4.Output.Navbar
+
+namespace DocGen4
+namespace Output
+
+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
+      #[<script>{s!"const MODULE_NAME={String.quote module.toString};"}</script>]
+    else
+      #[]
+  pure
+    <html lang="en">
+      <head>
+        [← baseHtmlHeadDeclarations]
+
+        <title>{title}</title>
+        <script defer="true" src={s!"{← getRoot}mathjax-config.js"}></script>
+        <script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
+        <script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
+
+        <script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
+        [moduleConstant]
+        <script type="module" src={s!"{← getRoot}jump-src.js"}></script>
+        <script type="module" src={s!"{← getRoot}search.js"}></script>
+        <script type="module" src={s!"{← getRoot}expand-nav.js"}></script>
+        <script type="module" src={s!"{← getRoot}how-about.js"}></script>
+        <script type="module" src={s!"{← getRoot}instances.js"}></script>
+        <script type="module" src={s!"{← getRoot}importedBy.js"}></script>
+      </head>
+
+      <body>
+
+        <input id="nav_toggle" type="checkbox"/>
+
+        <header>
+          <h1><label for="nav_toggle"></label>Documentation</h1>
+          <p class="header_filename break_within">[breakWithin title]</p>
+          <form action="https://google.com/search" method="get" id="search_form">
+            <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
+            <input type="text" name="q" autocomplete="off"/>&#32;
+            <button id="search_button" onclick={s!"javascript: form.action='{← getRoot}search.html';"}>Search</button>
+            <button>Google site search</button>
+          </form>
+        </header>
+
+        [site]
+
+        <nav class="nav">
+          <iframe src={s!"{← getRoot}navbar.html"} class="navframe" frameBorder="0"></iframe>
+        </nav>
+      </body>
+    </html>
+
+/--
+A comfortability wrapper around `baseHtmlGenerator`.
+-/
+def baseHtml (title : String) (site : Html) : BaseHtmlM Html := baseHtmlGenerator title #[site]
+
+end Output
+end DocGen4

DocGen4/Output/ToHtmlFormat.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2021 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving
+-/
+import Lean.Data.Json
+import Lean.Parser
+
+/-! This module defines:
+- a representation of HTML trees
+- together with a JSX-like DSL for writing them
+- and widget support for visualizing any type as HTML. -/
+
+namespace DocGen4
+
+open Lean
+
+inductive Html where
+  -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
+  -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
+  | element : String → Bool → Array (String × String) → Array Html → Html
+  | text : String → Html
+  deriving Repr, BEq, Inhabited, FromJson, ToJson
+
+instance : Coe String Html :=
+  ⟨Html.text⟩
+
+namespace Html
+
+def attributesToString (attrs : Array (String × String)) :String :=
+  attrs.foldl (fun acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
+
+-- TODO: Termination proof
+partial def toStringAux : Html → String
+| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
+| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
+| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
+| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
+| text s => s
+
+def toString (html : Html) : String :=
+  html.toStringAux.trimRight
+
+instance : ToString Html :=
+  ⟨toString⟩
+
+partial def textLength : Html → Nat
+| text s => s.length
+| element _ _ _ children =>
+  let lengths := children.map textLength
+  lengths.foldl Nat.add 0
+
+def escapePairs : Array (String × String) :=
+  #[
+    ("&", "&amp;"),
+    ("<", "&lt;"),
+    (">", "&gt;"),
+    ("\"", "&quot;")
+  ]
+
+def escape (s : String) : String :=
+  escapePairs.foldl (fun acc (o, r) => acc.replace o r) s
+
+end Html
+
+namespace Jsx
+open Parser PrettyPrinter
+
+declare_syntax_cat jsxElement
+declare_syntax_cat jsxChild
+
+-- JSXTextCharacter : SourceCharacter but not one of {, <, > or }
+def jsxText : Parser :=
+  withAntiquot (mkAntiquot "jsxText" `jsxText) {
+    fn := fun c s =>
+      let startPos := s.pos
+      let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
+      mkNodeToken `jsxText startPos c s }
+
+@[combinator_formatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
+@[combinator_parenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
+
+syntax jsxAttrName := rawIdent <|> str
+syntax jsxAttrVal := str <|> group("{" term "}")
+syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
+syntax jsxAttrSpread := "[" term "]"
+syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
+
+syntax "<" rawIdent jsxAttr* "/>" : jsxElement
+syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
+
+syntax jsxText      : jsxChild
+syntax "{" term "}" : jsxChild
+syntax "[" term "]" : jsxChild
+syntax jsxElement   : jsxChild
+
+scoped syntax:max jsxElement : term
+
+def translateAttrs (attrs : Array (TSyntax `DocGen4.Jsx.jsxAttr)) : MacroM (TSyntax `term) := do
+  let mut as ← `(#[])
+  for attr in attrs.map TSyntax.raw do
+    as ← match attr with
+    | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
+      let n ← match n with
+        | `(jsxAttrName| $n:str) => pure n
+        | `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId)
+        | _ => Macro.throwUnsupported
+      let v ← match v with
+        | `(jsxAttrVal| {$v}) => pure v
+        | `(jsxAttrVal| $v:str) => pure v
+        | _ => Macro.throwUnsupported
+      `(($as).push ($n, ($v : String)))
+    | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
+    | _ => Macro.throwUnsupported
+  return as
+
+private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × (TSyntax `term)):= do
+  unless n.getId == m.getId do
+    withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
+  let mut cs ← `(#[])
+  for child in children do
+    cs ← match child with
+    | `(jsxChild|$t:jsxText)    => `(($cs).push (Html.text $(quote t.raw[0]!.getAtomVal)))
+    -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
+    | `(jsxChild|{$t})          => `(($cs).push ($t : Html))
+    | `(jsxChild|[$t])          => `($cs ++ ($t : Array Html))
+    | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
+    | _                         => Macro.throwUnsupported
+  let tag := toString n.getId
+  pure <| (tag, cs)
+
+macro_rules
+  | `(<$n $attrs* />) => do
+    let kind := quote (toString n.getId)
+    let attrs ← translateAttrs attrs
+    `(Html.element $kind true $attrs #[])
+  | `(<$n $attrs* >$children*</$m>) => do
+    let (tag, children) ← htmlHelper n children m
+    `(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
+
+end Jsx
+
+/-- A type which implements `ToHtmlFormat` will be visualized
+as the resulting HTML in editors which support it. -/
+class ToHtmlFormat (α : Type u) where
+  formatHtml : α → Html
+
+end DocGen4

DocGen4/Output/ToJson.lean

@@ -0,0 +1,134 @@
+import Lean
+import DocGen4.Process
+import DocGen4.Output.Base
+import DocGen4.Output.Module
+import Lean.Data.RBMap
+
+namespace DocGen4.Output
+
+open Lean
+
+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
+  typeNames : Array String
+  deriving FromJson, ToJson
+
+structure JsonModule where
+  name : String
+  declarations : List JsonDeclaration
+  instances : Array JsonInstance
+  imports : Array String
+  deriving FromJson, ToJson
+
+structure JsonHeaderIndex where
+  declarations : List (String × JsonDeclaration) := []
+
+structure JsonIndexedDeclarationInfo where
+  kind : String
+  docLink : 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 : List (String × String) := []
+  instancesFor : HashMap String (RBTree String Ord.compare) := .empty
+
+instance : ToJson JsonHeaderIndex where
+  toJson idx := Json.mkObj <| idx.declarations.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.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.toArray))
+    let finalJson := Json.mkObj [
+      ("declarations", jsonDecls),
+      ("instances", jsonInstances),
+      ("importedBy", jsonImportedBy),
+      ("modules", jsonModules),
+      ("instancesFor", jsonInstancesFor)
+    ]
+    return finalJson
+
+def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex :=
+  let merge idx decl := { idx with declarations := (decl.info.name, decl) :: idx.declarations }
+  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.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 {}
+    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.insert inst.name
+      index := { index with instancesFor := index.instancesFor.insert typeName instsFor }
+
+  for imp in module.imports do
+    let mut impBy := index.importedBy.findD imp #[]
+    impBy := impBy.push module.name
+    index := { index with importedBy := index.importedBy.insert imp impBy }
+  return index
+
+def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
+  let name := info.getName.toString
+  let kind := info.getKind
+  let doc := info.getDocString.getD ""
+  let docLink ← declNameToLink info.getName
+  let sourceLink ← getSourceUrl module info.getDeclarationRange
+  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 := []
+    let mut instances := #[]
+    let declInfo := Process.filterDocInfo 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.className.toString
+          typeNames := i.typeNames.map Name.toString
+        }
+    let jsonMod : JsonModule :=  {
+      name := module.name.toString,
+      declarations := jsonDecls,
+      instances,
+      imports := module.imports.map Name.toString
+    }
+    return ToJson.toJson jsonMod
+
+end DocGen4.Output

DocGen4/Process.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import DocGen4.Process.Analyze
+import DocGen4.Process.Attributes
+import DocGen4.Process.AxiomInfo
+import DocGen4.Process.Base
+import DocGen4.Process.ClassInfo
+import DocGen4.Process.DefinitionInfo
+import DocGen4.Process.DocInfo
+import DocGen4.Process.Hierarchy
+import DocGen4.Process.InductiveInfo
+import DocGen4.Process.InstanceInfo
+import DocGen4.Process.NameExt
+import DocGen4.Process.NameInfo
+import DocGen4.Process.OpaqueInfo
+import DocGen4.Process.StructureInfo
+import DocGen4.Process.TheoremInfo

DocGen4/Process/Analyze.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+import Lean.Data.HashMap
+import Lean.Data.HashSet
+
+import DocGen4.Process.Base
+import DocGen4.Process.Hierarchy
+import DocGen4.Process.DocInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+/--
+Member of a module, either a declaration or some module doc string.
+-/
+inductive ModuleMember where
+| docInfo (info : DocInfo) : ModuleMember
+| modDoc (doc : ModuleDoc) : ModuleMember
+deriving Inhabited
+
+/--
+A Lean module.
+-/
+structure Module where
+  /--
+  Name of the module.
+  -/
+  name : Name
+  /--
+  All members of the module, sorted according to their line numbers.
+  -/
+  members : Array ModuleMember
+  imports : Array Name
+  deriving Inhabited
+
+/--
+The result of running a full doc-gen analysis on a project.
+-/
+structure AnalyzerResult where
+  /--
+  The map from module names to indices of the `moduleNames` array.
+  -/
+  name2ModIdx : HashMap Name ModuleIdx
+  /--
+  The list of all modules, accessible nicely via `name2ModIdx`.
+  -/
+  moduleNames : Array Name
+  /--
+  A map from module names to information about these modules.
+  -/
+  moduleInfo : HashMap Name Module
+  deriving Inhabited
+
+namespace ModuleMember
+
+def getDeclarationRange : ModuleMember → DeclarationRange
+| docInfo i => i.getDeclarationRange
+| modDoc i => i.declarationRange
+
+/--
+An order for module members, based on their declaration range.
+-/
+def order (l r : ModuleMember) : Bool :=
+  Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
+
+def getName : ModuleMember → Name
+| docInfo i => i.getName
+| modDoc _ => Name.anonymous
+
+def getDocString : ModuleMember → Option String
+| docInfo i => i.getDocString
+| modDoc i => i.doc
+
+def shouldRender : ModuleMember → Bool
+| docInfo i => i.shouldRender
+| modDoc _ => true
+
+end ModuleMember
+
+inductive AnalyzeTask where
+| loadAll (load : Array Name) : AnalyzeTask
+| loadAllLimitAnalysis (analyze : Array Name) : AnalyzeTask
+
+def AnalyzeTask.getLoad : AnalyzeTask → Array Name
+| loadAll load => load
+| 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
+    let some modIdx := env.getModuleIdx? module | unreachable!
+    let moduleData := env.header.moduleData.get! modIdx
+    let imports := moduleData.imports.map Import.module
+    res := res.insert module <| Module.mk module modDocs imports
+  return res
+
+/--
+Run the doc-gen analysis on all modules that are loaded into the `Environment`
+of this `MetaM` run and mentioned by the `AnalyzeTask`.
+-/
+def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
+  let env ← getEnv
+  let relevantModules := match task with
+    | .loadAll _ => HashSet.fromArray env.header.moduleNames
+    | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis
+  let allModules := env.header.moduleNames
+
+  let mut res ← getAllModuleDocs relevantModules.toArray
+
+  for (name, cinfo) in env.constants.toList do
+    let some modidx := env.getModuleIdxFor? name | unreachable!
+    let moduleName := env.allImportedModuleNames.get! modidx
+    if !relevantModules.contains moduleName then
+      continue
+
+    try
+      let config := {
+        maxHeartbeats := 5000000,
+        options := ← getOptions,
+        fileName := ← getFileName,
+        fileMap := ← getFileMap
+      }
+      let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
+      if let some dinfo := analysis then
+        let moduleName := env.allImportedModuleNames.get! modidx
+        let module := res.find! moduleName
+        res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
+    catch e =>
+      if let some pos := e.getRef.getPos? then
+        let pos := (← getFileMap).toPosition pos
+        IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
+      else
+        IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
+
+  -- 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}
+
+  let hierarchy := Hierarchy.fromArray allModules
+  let analysis := {
+    name2ModIdx := env.const2ModIdx,
+    moduleNames := allModules,
+    moduleInfo := res,
+  }
+  return (analysis, hierarchy)
+
+def filterDocInfo (ms : Array ModuleMember) : Array DocInfo :=
+  ms.filterMap filter
+  where
+    filter : ModuleMember → Option DocInfo
+    | ModuleMember.docInfo i => some i
+    | _ => none
+
+end DocGen4.Process

DocGen4/Process/Attributes.lean

@@ -0,0 +1,182 @@
+import Lean
+
+namespace DocGen4
+
+open Lean Meta
+-- The following is probably completely overengineered but I love it
+
+/--
+Captures the notion of a value based attributes, `attrKind` is things like
+`EnumAttributes`.
+-/
+class ValueAttr (attrKind : Type → Type) where
+  /--
+  Given a certain value based attribute, an `Environment` and the `Name` of
+  a declaration returns the value of the attribute on this declaration if present.
+  -/
+  getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
+
+/--
+Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).
+-/
+structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
+  {α : Type}
+  attr : attrKind α
+  [str : ToString α]
+  [inhab : Inhabited α]
+
+/--
+Obtain the value of an enum attribute for a certain name.
+-/
+def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := do
+  let val ← EnumAttributes.getValue attr env decl
+  some (toString val)
+
+instance : ValueAttr EnumAttributes where
+  getValue := enumGetValue
+
+/--
+Obtain the value of a parametric attribute for a certain name.
+-/
+def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
+  let val ← ParametricAttribute.getParam? attr env decl
+  some (attr.attr.name.toString ++ " " ++ toString val)
+
+instance : ValueAttr ParametricAttribute where
+  getValue := parametricGetValue
+
+abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
+abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
+
+/--
+The list of all tag based attributes doc-gen knows about and can recover.
+-/
+def tagAttributes : Array TagAttribute :=
+  #[IR.UnboxResult.unboxAttr, neverExtractAttr,
+    Elab.Term.elabWithoutExpectedTypeAttr, matchPatternAttr]
+
+deriving instance Repr for Compiler.InlineAttributeKind
+deriving instance Repr for Compiler.SpecializeAttributeKind
+
+open Compiler in
+instance : ToString InlineAttributeKind where
+  toString kind :=
+    match kind with
+    | .inline => "inline"
+    | .noinline => "noinline"
+    | .macroInline => "macro_inline"
+    | .inlineIfReduce => "inline_if_reduce"
+    | .alwaysInline => "always_inline"
+
+open Compiler in
+instance : ToString SpecializeAttributeKind where
+  toString kind :=
+    match kind with
+    | .specialize => "specialize"
+    | .nospecialize => "nospecialize"
+
+instance : ToString ReducibilityStatus where
+  toString kind :=
+    match kind with
+    | .reducible => "reducible"
+    | .semireducible => "semireducible"
+    | .irreducible => "irreducible"
+
+/--
+The list of all enum based attributes doc-gen knows about and can recover.
+-/
+@[reducible]
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
+
+instance : ToString ExternEntry where
+  toString entry :=
+    match entry with
+    | .adhoc `all => ""
+    | .adhoc backend => s!"{backend} adhoc"
+    | .standard `all fn => fn
+    | .standard backend fn => s!"{backend} {fn}"
+    | .inline backend pattern => s!"{backend} inline {String.quote pattern}"
+    -- TODO: The docs in the module dont specific how to render this
+    | .foreign backend fn  => s!"{backend} foreign {fn}"
+
+instance : ToString ExternAttrData where
+  toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
+
+/--
+The list of all parametric attributes (that is, attributes with any kind of information attached)
+doc-gen knows about and can recover.
+-/
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩, ⟨Compiler.specializeAttr⟩]
+
+def getTags (decl : Name) : MetaM (Array String) := do
+  let env ← getEnv
+  return tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (·.attr.name.toString)
+
+def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
+  let env ← getEnv
+  return va.getValue attr env decl
+
+def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
+  let mut res := #[]
+  for attr in attrs do
+    if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
+      res := res.push val
+  return res
+
+def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
+def getParametricValues (decl : Name) : MetaM (Array String) := do
+  let mut uniform ← getValues decl parametricAttributes
+  -- This attribute contains an `Option Name` but we would like to pretty print it better
+  if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
+    let str := match depTag with
+    | some alt => s!"deprecated {alt.toString}"
+    | none => "deprecated"
+    uniform := uniform.push str
+  return uniform
+
+def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
+  let insts ← getDefaultInstances className
+  for (inst, prio) in insts do
+    if inst == decl then
+      return some s!"defaultInstance {prio}"
+  return none
+
+def hasSimp (decl : Name) : MetaM (Option String) := do
+  let thms ← simpExtension.getTheorems
+  if thms.isLemma (.decl decl) then
+    return "simp"
+  else
+    return none
+
+def hasCsimp (decl : Name) : MetaM (Option String) := do
+  let env ← getEnv
+  if Compiler.hasCSimpAttribute env decl then
+    return some "csimp"
+  else
+    return none
+
+/--
+The list of custom attributes, that don't fit in the parametric or enum
+attribute kinds, doc-gen konws about and can recover.
+-/
+def customAttrs := #[hasSimp, hasCsimp]
+
+def getCustomAttrs (decl : Name) : MetaM (Array String) := do
+  let mut values := #[]
+  for attr in customAttrs do
+    if let some value ← attr decl then
+      values := values.push value
+  return values
+
+/--
+The main entry point for recovering all attribute values for a given
+declaration.
+-/
+def getAllAttributes (decl : Name) : MetaM (Array String) := do
+  let tags ← getTags decl
+  let enums ← getEnumValues decl
+  let parametric ← getParametricValues decl
+  let customs ← getCustomAttrs decl
+  return customs ++ tags ++ enums ++ parametric
+
+end DocGen4

DocGen4/Process/AxiomInfo.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  return {
+    toInfo := info,
+    isUnsafe := v.isUnsafe
+  } 
+
+end DocGen4.Process

DocGen4/Process/Base.lean

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+
+namespace DocGen4.Process
+open Lean Widget Meta
+
+/--
+Stores information about a typed name.
+-/
+structure NameInfo where
+  /--
+  The name that has this info attached.
+  -/
+  name  : Name
+  /--
+  The pretty printed type of this name.
+  -/
+  type : CodeWithInfos
+  /--
+  The doc string of the name if it exists.
+  -/
+  doc : Option String
+  deriving Inhabited
+
+
+/--
+An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
+-/
+structure Arg where
+  /--
+  The name of the argument. For auto generated argument names like `[Monad α]`
+  this is none
+  -/
+  name : Option Name
+  /--
+  The pretty printed type of the argument.
+  -/
+  type : CodeWithInfos
+  /--
+  What kind of binder was used for the argument.
+  -/
+  binderInfo : BinderInfo
+
+/--
+A base structure for information about a declaration.
+-/
+structure Info extends NameInfo where
+  /--
+  The list of arguments to the declaration.
+  -/
+  args : Array Arg
+  /--
+  In which lines the declaration was created.
+  -/
+  declarationRange : DeclarationRange
+  /--
+  A list of (known) attributes that are attached to the declaration.
+  -/
+  attrs : Array String
+  /--
+  Whether this info item should be rendered
+  -/
+  render : Bool := true
+  deriving Inhabited
+
+/--
+Information about an `axiom` declaration.
+-/
+structure AxiomInfo extends Info where
+  isUnsafe : Bool
+  deriving Inhabited
+
+/--
+Information about a `theorem` declaration.
+-/
+structure TheoremInfo extends Info
+  deriving Inhabited
+
+/--
+Information about an `opaque` declaration.
+-/
+structure OpaqueInfo extends Info where
+  /--
+  The pretty printed value of the declaration.
+  -/
+  value : CodeWithInfos
+  /--
+  A value of partial is interpreted as this opaque being part of a partial def
+  since the actual definition for a partial def is hidden behind an inaccessible value.
+  -/
+  definitionSafety : DefinitionSafety
+  deriving Inhabited
+
+/--
+Information about a `def` declaration, note that partial defs are handled by `OpaqueInfo`.
+-/
+structure DefinitionInfo extends Info where
+  isUnsafe : Bool
+  hints : ReducibilityHints
+  equations : Option (Array CodeWithInfos)
+  isNonComputable : Bool
+  deriving Inhabited
+
+/--
+Information about an `instance` declaration.
+-/
+structure InstanceInfo extends DefinitionInfo where
+  className : Name
+  typeNames : Array Name
+  deriving Inhabited
+
+/--
+Information about an `inductive` declaration
+-/
+structure InductiveInfo extends Info where
+  /--
+  List of all constructors of this inductive type.
+  -/
+  ctors : List NameInfo
+  isUnsafe : Bool
+  deriving Inhabited
+
+/--
+Information about a `structure` declaration.
+-/
+structure StructureInfo extends Info where
+  /--
+  Information about all the fields of the structure.
+  -/
+  fieldInfo : Array NameInfo
+  /--
+  All the structures this one inherited from.
+  -/
+  parents : Array Name
+  /--
+  The constructor of the structure.
+  -/
+  ctor : NameInfo
+  deriving Inhabited
+
+/--
+Information about a `class` declaration.
+-/
+abbrev ClassInfo := StructureInfo
+
+/--
+Information about a `class inductive` declaration.
+-/
+abbrev ClassInductiveInfo := InductiveInfo
+
+
+/--
+Information about a constructor of an inductive type
+-/
+abbrev ConstructorInfo := Info
+
+/--
+A general type for informations about declarations.
+-/
+inductive DocInfo where
+| axiomInfo (info : AxiomInfo) : DocInfo
+| theoremInfo (info : TheoremInfo) : DocInfo
+| opaqueInfo (info : OpaqueInfo) : DocInfo
+| definitionInfo (info : DefinitionInfo) : DocInfo
+| instanceInfo (info : InstanceInfo) : DocInfo
+| inductiveInfo (info : InductiveInfo) : DocInfo
+| structureInfo (info : StructureInfo) : DocInfo
+| classInfo (info : ClassInfo) : DocInfo
+| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
+| ctorInfo (info : ConstructorInfo) : DocInfo
+  deriving Inhabited
+
+/--
+Turns an `Expr` into a pretty printed `CodeWithInfos`.
+-/
+def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
+  let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos expr
+  let tt := TaggedText.prettyTagged fmt
+  let ctx := {
+    env := ← getEnv
+    mctx := ← getMCtx
+    options := ← getOptions
+    currNamespace := ← getCurrNamespace
+    openDecls := ← getOpenDecls
+    fileMap := default,
+    ngen := ← getNGen
+  }
+  return tagCodeInfos ctx infos tt
+
+def isInstance (declName : Name) : MetaM Bool := do
+  return (instanceExtension.getState (← getEnv)).instanceNames.contains declName
+
+end DocGen4.Process

DocGen4/Process/ClassInfo.lean

@@ -0,0 +1,24 @@
+
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+import DocGen4.Process.StructureInfo
+import DocGen4.Process.InductiveInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
+  StructureInfo.ofInductiveVal v
+
+def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
+  InductiveInfo.ofInductiveVal v
+
+end DocGen4.Process

DocGen4/Process/DefinitionInfo.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta Widget
+
+partial def stripArgs (e : Expr) (k : Expr → MetaM α) : MetaM α :=
+  match e.consumeMData with
+  | Expr.forallE name type body bi =>
+    let name := name.eraseMacroScopes
+    Meta.withLocalDecl name bi type fun fvar => do
+      stripArgs (Expr.instantiate1 body fvar) k
+  | _ => k e
+
+def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
+  withOptions (tactic.hygienic.set . false) do
+    lambdaTelescope v.value fun xs body => do
+      let us := v.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
+      let type ← mkForallFVars xs type
+      return type
+
+def processEq (eq : Name) : MetaM CodeWithInfos := do
+  let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
+  stripArgs type prettyPrintTerm
+
+def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let isUnsafe := v.safety == DefinitionSafety.unsafe
+  let isNonComputable := isNoncomputable (← getEnv) v.name
+  try
+    let eqs? ← getEqnsFor? v.name
+    match eqs? with
+    | some eqs =>
+      let equations ← eqs.mapM processEq
+      return {
+        toInfo := info,
+        isUnsafe,
+        hints := v.hints,
+        equations,
+        isNonComputable
+      }
+    | none =>
+      let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
+      return {
+        toInfo := info,
+        isUnsafe,
+        hints := v.hints,
+        equations,
+        isNonComputable
+      }
+  catch err =>
+    IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
+    return {
+      toInfo := info,
+      isUnsafe,
+      hints := v.hints,
+      equations := none,
+      isNonComputable
+    }
+
+
+
+end DocGen4.Process

DocGen4/Process/DocInfo.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.AxiomInfo
+import DocGen4.Process.TheoremInfo
+import DocGen4.Process.OpaqueInfo
+import DocGen4.Process.InstanceInfo
+import DocGen4.Process.DefinitionInfo
+import DocGen4.Process.ClassInfo
+import DocGen4.Process.StructureInfo
+import DocGen4.Process.InductiveInfo
+
+
+namespace DocGen4.Process
+namespace DocInfo
+
+open Lean Meta Widget
+
+def getDeclarationRange : DocInfo → DeclarationRange
+| axiomInfo i => i.declarationRange
+| theoremInfo i => i.declarationRange
+| opaqueInfo i => i.declarationRange
+| definitionInfo i => i.declarationRange
+| instanceInfo i => i.declarationRange
+| inductiveInfo i => i.declarationRange
+| structureInfo i => i.declarationRange
+| classInfo i => i.declarationRange
+| classInductiveInfo i => i.declarationRange
+| ctorInfo i => i.declarationRange
+
+def getName : DocInfo → Name
+| axiomInfo i => i.name
+| theoremInfo i => i.name
+| opaqueInfo i => i.name
+| definitionInfo i => i.name
+| instanceInfo i => i.name
+| inductiveInfo i => i.name
+| structureInfo i => i.name
+| classInfo i => i.name
+| classInductiveInfo i => i.name
+| ctorInfo i => i.name
+
+def getKind : DocInfo → String
+| axiomInfo _ => "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo _ => "opaque"
+| definitionInfo _ => "def"
+| instanceInfo _ => "instance"
+| inductiveInfo _ => "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
+| classInductiveInfo _ => "class"
+| ctorInfo _ => "ctor" -- TODO: kind ctor support in js
+
+def getType : DocInfo → CodeWithInfos
+| axiomInfo i => i.type
+| theoremInfo i => i.type
+| opaqueInfo i => i.type
+| definitionInfo i => i.type
+| instanceInfo i => i.type
+| inductiveInfo i => i.type
+| structureInfo i => i.type
+| classInfo i => i.type
+| classInductiveInfo i => i.type
+| ctorInfo i => i.type
+
+def getArgs : DocInfo → Array Arg
+| axiomInfo i => i.args
+| theoremInfo i => i.args
+| opaqueInfo i => i.args
+| definitionInfo i => i.args
+| instanceInfo i => i.args
+| inductiveInfo i => i.args
+| structureInfo i => i.args
+| classInfo i => i.args
+| classInductiveInfo i => i.args
+| ctorInfo i => i.args
+
+def getAttrs : DocInfo → Array String
+| axiomInfo i => i.attrs
+| theoremInfo i => i.attrs
+| opaqueInfo i => i.attrs
+| definitionInfo i => i.attrs
+| instanceInfo i => i.attrs
+| inductiveInfo i => i.attrs
+| structureInfo i => i.attrs
+| classInfo i => i.attrs
+| classInductiveInfo i => i.attrs
+| ctorInfo i => i.attrs
+
+def getDocString : DocInfo → Option String
+| axiomInfo i => i.doc
+| theoremInfo i => i.doc
+| opaqueInfo i => i.doc
+| definitionInfo i => i.doc
+| instanceInfo i => i.doc
+| inductiveInfo i => i.doc
+| structureInfo i => i.doc
+| classInfo i => i.doc
+| classInductiveInfo i => i.doc
+| ctorInfo i => i.doc
+
+def shouldRender : DocInfo → Bool
+| axiomInfo i => i.render
+| theoremInfo i => i.render
+| opaqueInfo i => i.render
+| definitionInfo i => i.render
+| instanceInfo i => i.render
+| inductiveInfo i => i.render
+| structureInfo i => i.render
+| classInfo i => i.render
+| classInductiveInfo i => i.render
+| ctorInfo i => i.render
+
+def isBlackListed (declName : Name) : MetaM Bool := do
+  match ← findDeclarationRanges? declName with
+  | some _ =>
+    let env ← getEnv
+    pure (declName.isInternal)
+    <||> (pure <| isAuxRecursor env declName)
+    <||> (pure <| isNoConfusion env declName)
+    <||> isRec declName
+    <||> isMatcher declName
+  -- TODO: Evaluate whether filtering out declarations without range is sensible
+  | none => return true
+
+-- TODO: Is this actually the best way?
+def isProjFn (declName : Name) : MetaM Bool := do
+  let env ← getEnv
+  match declName with
+  | Name.str parent name =>
+    if isStructure env parent then
+      match getStructureInfo? env parent with
+      | some i =>
+        match i.fieldNames.find? (· == name) with
+        | some _ => return true
+        | none => return false
+      | none => panic! s!"{parent} is not a structure"
+    else
+      return false
+  | _ => return false
+
+def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do
+  if ← isBlackListed name then
+    return none
+  match info with
+  | ConstantInfo.axiomInfo i => return some <| axiomInfo (← AxiomInfo.ofAxiomVal i)
+  | ConstantInfo.thmInfo i => return some <| theoremInfo (← TheoremInfo.ofTheoremVal i)
+  | ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
+  | ConstantInfo.defnInfo i =>
+    if ← isProjFn i.name then
+      let info ← DefinitionInfo.ofDefinitionVal i
+      return some <| definitionInfo { info with render := false }
+    else
+      if ← isInstance i.name then
+        let info ← InstanceInfo.ofDefinitionVal i
+        return some <| instanceInfo info
+      else
+        let info ← DefinitionInfo.ofDefinitionVal i
+        return some <| definitionInfo  info
+  | ConstantInfo.inductInfo i =>
+    let env ← getEnv
+    if isStructure env i.name then
+      if isClass env i.name then
+        return some <| classInfo (← ClassInfo.ofInductiveVal i)
+      else
+        return some <| structureInfo (← StructureInfo.ofInductiveVal i)
+    else
+      if isClass env i.name then
+        return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i)
+      else
+        return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i)
+  | ConstantInfo.ctorInfo i =>
+    let info ← Info.ofConstantVal i.toConstantVal
+    return some <| ctorInfo { info with render := false }
+  -- we ignore these for now
+  | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
+
+def getKindDescription : DocInfo → String
+| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo i =>
+  match i.definitionSafety with
+  | DefinitionSafety.safe => "opaque"
+  | DefinitionSafety.unsafe => "unsafe opaque"
+  | DefinitionSafety.partial => "partial def"
+| definitionInfo i => Id.run do
+  let mut modifiers := #[]
+  if i.isUnsafe then
+    modifiers := modifiers.push "unsafe"
+  if i.isNonComputable then
+    modifiers := modifiers.push "noncomputable"
+
+  let defKind :=
+    if i.hints.isAbbrev then
+      "abbrev"
+    else
+      "def"
+  modifiers := modifiers.push defKind
+  return String.intercalate " " modifiers.toList
+| instanceInfo i => Id.run do
+  let mut modifiers := #[]
+  if i.isUnsafe then
+    modifiers := modifiers.push "unsafe"
+  if i.isNonComputable then
+    modifiers := modifiers.push "noncomputable"
+
+  modifiers := modifiers.push "instance"
+  return String.intercalate " " modifiers.toList
+| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
+| classInductiveInfo _ => "class inductive"
+| ctorInfo _ => "constructor"
+
+end DocInfo
+
+end DocGen4.Process

DocGen4/Process/Hierarchy.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2021 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import Lean.Data.HashMap
+
+import DocGen4.Process.NameExt
+
+def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
+  xs.foldr (flip .insert) .empty
+
+namespace DocGen4
+
+open Lean Name
+
+def getNLevels (name : Name) (levels: Nat) : Name :=
+  let components := name.componentsRev
+  (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
+
+inductive Hierarchy where
+| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy
+
+instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨.anonymous, .html⟩ false RBNode.leaf⟩
+
+abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy)
+
+-- Everything in this namespace is adapted from stdlib's RBNode
+namespace HierarchyMap
+
+def toList : HierarchyMap → List (NameExt × Hierarchy)
+| t => t.revFold (fun ps k v => (k, v)::ps) []
+
+def toArray : HierarchyMap → Array (NameExt × Hierarchy)
+| t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[]
+
+def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
+  t.forIn init (fun a b acc => f (a, b) acc)
+
+instance : ForIn m HierarchyMap (NameExt × Hierarchy) where
+  forIn := HierarchyMap.hForIn
+
+end HierarchyMap
+
+namespace Hierarchy
+
+def empty (n : NameExt) (isFile : Bool) : Hierarchy :=
+  node n isFile RBNode.leaf
+
+def getName : Hierarchy → Name
+| node n _ _ => n.name
+
+def getNameExt : Hierarchy → NameExt
+| node n _ _ => n
+
+def getChildren : Hierarchy → HierarchyMap
+| node _ _ c => c
+
+def isFile : Hierarchy → Bool
+| node _ f _ => f
+
+partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do
+  let hn := h.getNameExt
+  let mut cs := h.getChildren
+
+  if getNumParts hn.name + 1 == getNumParts n.name then
+    match cs.find NameExt.cmp n with
+    | none =>
+      node hn h.isFile (cs.insert NameExt.cmp n <| empty n true)
+    | some (node _ true _) => h
+    | some (node _ false ccs) =>
+        cs := cs.erase NameExt.cmp n
+        node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs)
+  else
+    let leveled := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩
+    match cs.find NameExt.cmp leveled with
+    | some nextLevel =>
+      cs := cs.erase NameExt.cmp leveled
+      -- BUG?
+      node hn h.isFile <| cs.insert NameExt.cmp leveled (nextLevel.insert! n)
+    | none =>
+      let child := (insert! (empty leveled false) n)
+      node hn h.isFile <| cs.insert NameExt.cmp leveled child
+
+partial def fromArray (names : Array Name) : Hierarchy :=
+   (names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false)
+
+partial def fromArrayExt (names : Array NameExt) : Hierarchy :=
+  names.foldl insert! (empty ⟨anonymous, .html⟩ false)
+
+def baseDirBlackList : HashSet String :=
+  HashSet.fromArray #[
+    "404.html",
+    "color-scheme.js",
+    "declaration-data.js",
+    "declarations",
+    "expand-nav.js",
+    "find",
+    "foundational_types.html",
+    "how-about.js",
+    "index.html",
+    "jump-src.js",
+    "mathjax-config.js",
+    "navbar.html",
+    "nav.js",
+    "search.html",
+    "search.js",
+    "src",
+    "style.css"
+  ]
+
+partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := 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 if entry.path.extension = some "html" then
+      children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩
+    else if entry.path.extension = some "pdf" then
+      children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩
+  return 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 then
+        continue
+      else if ← entry.path.isDir then
+        children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName))
+      else if entry.path.extension = some "html" then
+        children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩
+      else if entry.path.extension = some "pdf" then
+        children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩
+    return Hierarchy.fromArrayExt children
+
+end Hierarchy
+end DocGen4

DocGen4/Process/InductiveInfo.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+def getConstructorType (ctor : Name) : MetaM Expr := do
+  let env ← getEnv
+  match env.find? ctor with
+  | some (ConstantInfo.ctorInfo i) => pure i.type
+  | _ => panic! s!"Constructor {ctor} was requested but does not exist"
+
+def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let ctors ← v.ctors.mapM (fun name => do NameInfo.ofTypedName name (← getConstructorType name))
+  return {
+    toInfo := info,
+    ctors,
+    isUnsafe := v.isUnsafe
+  }
+
+end DocGen4.Process

DocGen4/Process/InstanceInfo.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+import DocGen4.Process.DefinitionInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
+  let (_, _, tail) ← forallMetaTelescopeReducing typ
+  let args := tail.getAppArgs
+  let (_, bis, _) ← forallMetaTelescopeReducing (← inferType tail.getAppFn)
+  let (_, names) ← (bis.zip args).mapM findName |>.run .empty
+  return names
+where
+  findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit
+    | (.default, .sort .zero) => modify (·.push "_builtin_prop")
+    | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu")
+    | (.default, .sort _) => modify (·.push "_builtin_sortu")
+    | (.default, e) =>
+      match e.getAppFn with
+      | .const name .. => modify (·.push name)
+      | _ => return ()
+    | _ => return ()
+
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+  let mut info ← DefinitionInfo.ofDefinitionVal v
+  let some className ← isClass? v.type | panic! s!"isClass? on {v.name} returned none"
+  if let some instAttr ← getDefaultInstance v.name className then
+    info := { info with attrs := info.attrs.push instAttr }
+  let typeNames ← getInstanceTypes v.type
+  return {
+    toDefinitionInfo := info,
+    className,
+    typeNames
+  }
+
+end DocGen4.Process

DocGen4/Process/NameExt.lean

@@ -0,0 +1,48 @@
+/-
+A generalization of `Lean.Name` that includes a file extension.
+-/
+import Lean
+
+open Lean Name
+
+inductive Extension where
+| html
+| pdf
+deriving Repr
+
+namespace Extension
+
+def cmp : Extension → Extension → Ordering
+  | html, html => Ordering.eq
+  | html, _ => Ordering.lt
+  | pdf, pdf => Ordering.eq
+  | pdf, _ => Ordering.gt
+
+instance : BEq Extension where
+  beq e1 e2 :=
+    match cmp e1 e2 with
+    | Ordering.eq => true
+    | _ => false
+
+def toString : Extension → String
+  | html => "html"
+  | pdf => "pdf"
+
+end Extension
+
+structure NameExt where
+  name : Name
+  ext : Extension
+
+namespace NameExt
+
+def cmp (n₁ n₂ : NameExt) : Ordering :=
+  match Name.cmp n₁.name n₂.name with
+  | Ordering.eq => Extension.cmp n₁.ext n₂.ext
+  | ord => ord
+
+def getString! : NameExt → String
+  | ⟨str _ s, _⟩ => s
+  | _       => unreachable!
+
+end NameExt

DocGen4/Process/NameInfo.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.Attributes
+
+namespace DocGen4.Process
+open Lean Meta
+
+def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
+  let env ← getEnv
+  return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
+
+partial def argTypeTelescope {α : Type} (e : Expr) (k : Array ((Option Name) × Expr × BinderInfo) → Expr → MetaM α) : MetaM α :=
+  go e #[]
+where
+  go (e : Expr) (args : Array ((Option Name) × Expr × BinderInfo)) : MetaM α := do
+    let helper := fun name type body bi =>
+      -- Once we hit a name with a macro scope we stop traversing the expression
+      -- and print what is left after the : instead. The only exception
+      -- to this is instances since these almost never have a name
+      -- but should still be printed as arguments instead of after the :.
+      if bi.isInstImplicit && name.hasMacroScopes then
+        let arg := (none, type, bi)
+        Meta.withLocalDecl name bi type fun fvar => do
+          go (Expr.instantiate1 body fvar) (args.push arg)
+      else if name.hasMacroScopes then
+        k args e
+      else
+        let arg := (some name, type, bi)
+        Meta.withLocalDecl name bi type fun fvar => do
+          go (Expr.instantiate1 body fvar) (args.push arg)
+    match e.consumeMData with
+    | Expr.forallE name type body binderInfo => helper name type body binderInfo
+    | _ => k args e
+
+def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
+  argTypeTelescope v.type fun args type => do
+    let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b)
+    let nameInfo ← NameInfo.ofTypedName v.name type
+    match ← findDeclarationRanges? v.name with
+    -- TODO: Maybe selection range is more relevant? Figure this out in the future
+    | some range =>
+      return {
+        toNameInfo := nameInfo,
+        args,
+        declarationRange := range.range,
+        attrs := ← getAllAttributes v.name
+      }
+    | none => panic! s!"{v.name} is a declaration without position"
+
+end DocGen4.Process

DocGen4/Process/OpaqueInfo.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let value ← prettyPrintTerm v.value
+  let env ← getEnv
+  let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
+  let definitionSafety :=
+    if isPartial then
+      DefinitionSafety.partial
+    else if v.isUnsafe then
+      DefinitionSafety.unsafe
+    else
+      DefinitionSafety.safe
+  return {
+    toInfo := info,
+    value,
+    definitionSafety
+  }
+
+end DocGen4.Process

DocGen4/Process/StructureInfo.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+/--
+  Execute `k` with an array containing pairs `(fieldName, fieldType)`.
+  `k` is executed in an updated local context which contains local declarations for the `structName` parameters.
+-/
+def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do
+  let structName := info.name
+  let us := info.levelParams.map mkLevelParam
+  forallTelescopeReducing info.type fun params _ =>
+  withLocalDeclD `s (mkAppN (mkConst structName us) params) fun s => do
+    let mut info := #[]
+    for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
+      let proj ← mkProjection s fieldName
+      info := info.push (fieldName, (← inferType proj))
+    k info
+
+def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
+  withFields v fun fields =>
+    fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
+
+def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let env ← getEnv
+  let parents := getParentStructures env v.name
+  let ctorVal := getStructureCtor env v.name
+  let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
+  match getStructureInfo? env v.name with
+  | some i =>
+    if i.fieldNames.size - parents.size > 0 then
+      return {
+        toInfo := info,
+        fieldInfo := ← getFieldTypes v,
+        parents,
+        ctor
+      }
+    else
+      return {
+        toInfo := info,
+        fieldInfo := #[],
+        parents,
+        ctor
+      }
+  | none => panic! s!"{v.name} is not a structure"
+
+end DocGen4.Process

DocGen4/Process/TheoremInfo.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  return { toInfo := info }
+
+end DocGen4.Process

Makefile

@@ -0,0 +1,14 @@
+all:
+	@echo "Please specify a build target."
+
+docs:
+	-ls build/doc | \
+		grep -v -E 'Init|Lean|Mathlib' | \
+		xargs -I {} rm -r "build/doc/{}"
+	-./scripts/run_pdflatex.sh build > /dev/null
+	lake build Bookshelf:docs
+
+docs!:
+	-rm -r build/doc
+	-./scripts/run_pdflatex.sh build > /dev/null
+	lake build Bookshelf:docs

README.md

@@ -1,11 +1,7 @@
 # bookshelf
 
-A study of the books listed below.
-
-## Overview
-
-Most proofs are conducted in LaTeX. Where feasible, theorems are also formally
-proven in [Lean](https://leanprover.github.io/).
+A study of the books listed below. Most proofs are conducted in LaTeX. Where
+feasible, theorems are also formally proven in [Lean](https://leanprover.github.io/).
 
 - [ ] Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
 - [x] Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
@@ -18,21 +14,23 @@ proven in [Lean](https://leanprover.github.io/).
 - [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
 - [ ] Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.
 
-## Building
+## Documentation
+
+This project has absorbed [doc-gen4](https://github.com/leanprover/doc-gen4) to
+ease customization. In particular, the `DocGen4` module found in this project
+allows generating PDFs and including them in the navbar. To generate
+documentation and serve files locally, run the following:
 
-[direnv](https://direnv.net/) can be used to launch a dev shell upon entering
-this directory (refer to `.envrc`). Otherwise run via:
 ```bash
-$ nix develop
+> make docs[!]
+> lake run server
 ```
-If you prefer not to use `nix`, you can also use the [elan](https://github.com/leanprover/elan)
-package manager like normal. Afterward, build the project by running
-```bash
-$ lake build
-```
-Optionally build documentation by running:
-```bash
-$ lake build Bookshelf:docs
-```
-Afterward, you can view the generated files by running `python3 -m http.server`
-from within the `.lake/build/doc` directory.
+
+The `docs` build target avoids cleaning files that are expected to not change
+often (e.g. `Lean`, `Init`, and `Mathlib` related content). If you've upgraded
+Lean or Mathlib, run `make docs!` instead to generate documentation from
+scratch.
+
+Both assume you have `pdflatex` and `python3` available in your `$PATH`. To
+change how the server behaves, refer to the `.env` file located in the root
+directory of this project.

flake.lock

@@ -1,76 +0,0 @@
-{
-  "nodes": {
-    "flake-compat": {
-      "locked": {
-        "lastModified": 1696426674,
-        "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=",
-        "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33",
-        "revCount": 57,
-        "type": "tarball",
-        "url": "https://api.flakehub.com/f/pinned/edolstra/flake-compat/1.0.1/018afb31-abd1-7bff-a5e4-cff7e18efb7a/source.tar.gz"
-      },
-      "original": {
-        "type": "tarball",
-        "url": "https://flakehub.com/f/edolstra/flake-compat/1.tar.gz"
-      }
-    },
-    "flake-utils": {
-      "inputs": {
-        "systems": "systems"
-      },
-      "locked": {
-        "lastModified": 1701680307,
-        "narHash": "sha256-kAuep2h5ajznlPMD9rnQyffWG8EM/C73lejGofXvdM8=",
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "rev": "4022d587cbbfd70fe950c1e2083a02621806a725",
-        "type": "github"
-      },
-      "original": {
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "type": "github"
-      }
-    },
-    "nixpkgs": {
-      "locked": {
-        "lastModified": 1702312524,
-        "narHash": "sha256-gkZJRDBUCpTPBvQk25G0B7vfbpEYM5s5OZqghkjZsnE=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "a9bf124c46ef298113270b1f84a164865987a91c",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "root": {
-      "inputs": {
-        "flake-compat": "flake-compat",
-        "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs"
-      }
-    },
-    "systems": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
-      }
-    }
-  },
-  "root": "root",
-  "version": 7
-}

flake.nix

@@ -1,79 +0,0 @@
-{
-  description = "";
-
-  inputs = {
-    flake-compat.url = "https://flakehub.com/f/edolstra/flake-compat/1.tar.gz";
-    flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
-  };
-
-  outputs = { self, nixpkgs, flake-utils, ... }:
-    flake-utils.lib.eachDefaultSystem (system:
-      let
-        pkgs = nixpkgs.legacyPackages.${system};
-        manifest = import ./lake-manifest.nix { inherit pkgs; };
-        scheme-custom = with pkgs; (texlive.combine {
-          inherit (texlive) scheme-basic
-            bigfoot
-            comment
-            enumitem
-            environ
-            etoolbox
-            fontawesome5
-            jknapltx
-            mathabx
-            mathabx-type1
-            metafont
-            ncctools
-            pgf
-            rsfs
-            soul
-            stmaryrd
-            tcolorbox
-            xcolor;
-        });
-      in
-      {
-        packages = {
-          app = pkgs.stdenv.mkDerivation {
-            pname = "bookshelf";
-            version = "0.1.0";
-            src = ./.;
-            nativeBuildInputs = with pkgs; [
-              git
-              lean4
-              scheme-custom
-            ];
-            buildPhase = ''
-              mkdir -p .lake/packages
-              ${pkgs.lib.foldlAttrs (s: key: val: s + ''
-                cp -a ${val}/src .lake/packages/${key}
-                chmod 755 .lake/packages/${key}/{,.git}
-              '') "" manifest}
-
-              export GIT_ORIGIN_URL="https://github.com/jrpotter/bookshelf.git"
-              export GIT_REVISION="${self.rev or "dirty"}"
-              lake build Bookshelf:docs
-
-              find .lake/build/doc \
-                \( -name "*.html.trace" -o -name "*.html.hash" \) \
-                -exec rm {} +
-            '';
-            installPhase = ''
-              mkdir $out
-              cp -a .lake/build/doc/* $out
-            '';
-          };
-
-          default = self.packages.${system}.app;
-        };
-
-        devShells.default = pkgs.mkShell {
-          packages = with pkgs; [
-            lean4
-            python3
-            scheme-custom
-          ];
-        };
-      });
-}

lake-manifest.json

@@ -1,95 +1,76 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
+{"version": 6,
+ "packagesDir": "lake-packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "dc62b29a26fcc3da545472ab8ad2c98ef3433634",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/jrpotter/bookshelf-doc",
-   "type": "git",
-   "subDir": null,
-   "rev": "9bd217dc37ea79a3f118a313583f539cdbc762e6",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "bookshelf",
- "lakeDir": ".lake"}
+ [{"git":
+   {"url": "https://github.com/mhuisi/lean4-cli",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/xubaiw/CMark.lean",
+    "subDir?": null,
+    "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+    "opts": {},
+    "name": "CMark",
+    "inputRev?": "main",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+    "subDir?": null,
+    "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
+    "opts": {},
+    "name": "UnicodeBasic",
+    "inputRev?": "main",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/hargonix/LeanInk",
+    "subDir?": null,
+    "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
+    "opts": {},
+    "name": "leanInk",
+    "inputRev?": "doc-gen",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "c97b9b00802c2ed343d9ac73e59be287428dbcf0",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "master",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4.git",
+    "subDir?": null,
+    "rev": "87b0742b01e45c6cc53cd3043fe3c7cdbf87a56f",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/quote4",
+    "subDir?": null,
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}}],
+ "name": "bookshelf"}

lake-manifest.nix

@@ -1,119 +0,0 @@
-{ pkgs }:
-let
-  fetchGitPackage = { pname, version, owner, repo, rev, hash }:
-    pkgs.stdenv.mkDerivation {
-      inherit pname version;
-      src = pkgs.fetchgit {
-        inherit rev hash;
-        url = "https://github.com/${owner}/${repo}";
-        # We need to keep this attribute enabled to prevent Lake from trying to
-        # update the package. This attribute ensures the specified commit is
-        # accessible at HEAD:
-        # https://github.com/leanprover/lean4/blob/cddc8089bc736a1532d6092f69476bd2d205a9eb/src/lake/Lake/Load/Materialize.lean#L22
-        leaveDotGit = true;
-      };
-      nativeBuildInputs = with pkgs; [ git ];
-      # Lake will perform a compulsory check that `git remote get-url origin`
-      # returns the value we set here:
-      # https://github.com/leanprover/lean4/blob/cddc8089bc736a1532d6092f69476bd2d205a9eb/src/lake/Lake/Load/Materialize.lean#L54
-      buildPhase = ''
-        git remote add origin https://github.com/${owner}/${repo}
-      '';
-      installPhase = ''
-        shopt -s dotglob
-        mkdir -p $out/src
-        cp -a . $out/src
-      '';
-    };
-in
-{
-  CMark = fetchGitPackage {
-    pname = "CMark";
-    version = "main";
-    owner = "xubaiw";
-    repo = "CMark.lean";
-    rev = "0077cbbaa92abf855fc1c0413e158ffd8195ec77";
-    hash = "sha256-ge+9V4IsMdPwjhYu66zUUN6CK70K2BdMT98BzBV3a4c=";
-  };
-
-  Cli = fetchGitPackage {
-    pname = "Cli";
-    version = "main";
-    owner = "leanprover";
-    repo = "lean4-cli";
-    rev = "a751d21d4b68c999accb6fc5d960538af26ad5ec";
-    hash = "sha256-n+6x7ZhyKKiIMZ9cH9VV8zay3oTUlJojtxcLYsUwQPU=";
-  };
-
-  Qq = fetchGitPackage {
-    pname = "Qq";
-    version = "master";
-    owner = "leanprover-community";
-    repo = "quote4";
-    rev = "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755";
-    hash = "sha256-l+X+Mi4khC/xdwQmESz8Qzto6noYqhYN4UqC+TVt3cs=";
-  };
-
-  UnicodeBasic = fetchGitPackage {
-    pname = "UnicodeBasic";
-    version = "main";
-    owner = "fgdorais";
-    repo = "lean4-unicode-basic";
-    rev = "dc62b29a26fcc3da545472ab8ad2c98ef3433634";
-    hash = "sha256-EimohrYMr01CnGx8xCg4q4XX663QuxKfpTDNnDnosO4=";
-  };
-
-  aesop = fetchGitPackage {
-    pname = "aesop";
-    version = "master";
-    owner = "leanprover-community";
-    repo = "aesop";
-    rev = "c7cff4551258d31c0d2d453b3f9cbca757d445f1";
-    hash = "sha256-uzkxE9XJ4y3WMtmiNQn2Je1hNkQ2FgE1/0vqz8f98cw=";
-  };
-
-  doc-gen4 = fetchGitPackage {
-    pname = "doc-gen4";
-    version = "main";
-    owner = "jrpotter";
-    repo = "bookshelf-doc";
-    rev = "9bd217dc37ea79a3f118a313583f539cdbc762e6";
-    hash = "sha256-L7Uca5hJV19/WHYG+MkFWX6BwXDInfSYsOrnZdM9ejY=";
-  };
-
-  leanInk = fetchGitPackage {
-    pname = "leanInk";
-    version = "doc-gen";
-    owner = "hargonix";
-    repo = "LeanInk";
-    rev = "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1";
-    hash = "sha256-asHVaa1uOxpz5arCvfllIrJmMC9VDm1F+bufsu3XwN0=";
-  };
-
-  mathlib = fetchGitPackage {
-    pname = "mathlib";
-    version = "v4.3.0";
-    owner = "leanprover-community";
-    repo = "mathlib4.git";
-    rev = "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d";
-    hash = "sha256-B0pZ7HwJwOrEXTMMyJSzMLLyh66Bcs/CqNwC3EKZ60I=";
-  };
-
-  proofwidgets = fetchGitPackage {
-    pname = "proofwidgets";
-    version = "v0.0.23";
-    owner = "leanprover-community";
-    repo = "ProofWidgets4";
-    rev = "909febc72b4f64628f8d35cd0554f8a90b6e0749";
-    hash = "sha256-twXXKXXONQpfzG+YLoXYY+3kTU0F40Tsv2+SKfF2Qsc=";
-  };
-
-  std = fetchGitPackage {
-    pname = "std";
-    version = "v4.3.0";
-    owner = "leanprover";
-    repo = "std4";
-    rev = "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087";
-    hash = "sha256-agWcsRIEJbHSjIdiA6z/HQHLZkb72ASW9SPnIM0voeo=";
-  };
-}

lakefile.lean

@@ -4,17 +4,232 @@ open System Lake DSL
 
 package «bookshelf»
 
+-- ========================================
+-- Imports
+-- ========================================
+
+require Cli from git
+  "https://github.com/mhuisi/lean4-cli" @
+    "nightly"
+require CMark from git
+  "https://github.com/xubaiw/CMark.lean" @
+    "main"
+require UnicodeBasic from git
+  "https://github.com/fgdorais/lean4-unicode-basic" @
+    "main"
+require leanInk from git
+  "https://github.com/hargonix/LeanInk" @
+    "doc-gen"
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @
-    "v4.3.0"
+    "master"
 require std from git
   "https://github.com/leanprover/std4.git" @
-    "v4.3.0"
-require «doc-gen4» from git
-  "https://github.com/jrpotter/bookshelf-doc" @
     "main"
 
+-- ========================================
+-- Documentation Generator
+-- ========================================
+
+lean_lib DocGen4
+
+lean_exe «doc-gen4» {
+  root := `Main
+  supportInterpreter := true
+}
+
+/--
+Turns a Github git remote URL into an HTTPS Github URL.
+Three link types from git supported:
+- https://github.com/org/repo
+- https://github.com/org/repo.git
+- git@github.com:org/repo.git
+TODO: This function is quite brittle and very Github specific, we can
+probably do better.
+-/
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
+  let mut url := gitUrl
+  if url.startsWith "git@" then
+    url := url.drop 15
+    url := url.dropRight 4
+    return s!"https://github.com/{url}"
+  else if url.endsWith ".git" then
+    return url.dropRight 4
+  else
+    return url
+
+/--
+Obtain the Github URL of a project by parsing the origin remote.
+-/
+def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
+  let out ← IO.Process.output {
+    cmd := "git",
+    args := #["remote", "get-url", "origin"],
+    cwd := directory
+  }
+  if out.exitCode != 0 then
+    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
+  return out.stdout.trimRight
+
+/--
+Obtain the git commit hash of the project that is currently getting analyzed.
+-/
+def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
+  let out ← IO.Process.output {
+    cmd := "git",
+    args := #["rev-parse", "HEAD"]
+    cwd := directory
+  }
+  if out.exitCode != 0 then
+    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
+  return out.stdout.trimRight
+
+def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
+  let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir)
+  let commit ← getProjectCommit pkg.dir
+
+  let parts := mod.name.components.map toString
+  let path := String.intercalate "/" parts
+  let libPath := pkg.config.srcDir / lib.srcDir
+  let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
+  let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
+  return url
+
+module_facet docs (mod) : FilePath := do
+  let some docGen4 ← findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeJob ← docGen4.exe.fetch
+  let modJob ← mod.leanArts.fetch
+  let ws ← getWorkspace
+  let pkg ← ws.packages.find? (·.isLocalModule mod.name)
+  let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
+  -- Build all documentation imported modules
+  let imports ← mod.imports.fetch
+  let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
+  let gitUrl ← getGitUrl pkg libConfig mod
+  let buildDir := ws.root.buildDir
+  let docFile := mod.filePath (buildDir / "doc") "html"
+  depDocJobs.bindAsync fun _ depDocTrace => do
+  exeJob.bindAsync fun exeFile exeTrace => do
+  modJob.bindSync fun _ modTrace => do
+    let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
+    let trace ← buildFileUnlessUpToDate docFile depTrace do
+      logStep s!"Documenting module: {mod.name}"
+      proc {
+        cmd := exeFile.toString
+        args := #["single", mod.name.toString, gitUrl]
+        env := ← getAugmentedEnv
+      }
+    return (docFile, trace)
+
+-- TODO: technically speaking this facet does not show all file dependencies
+target coreDocs : FilePath := do
+  let some docGen4 ← findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeJob ← docGen4.exe.fetch
+  let basePath := (←getWorkspace).root.buildDir / "doc"
+  let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
+  exeJob.bindSync fun exeFile exeTrace => do
+    let trace ← buildFileUnlessUpToDate dataFile exeTrace do
+      logStep "Documenting Lean core: Init and Lean"
+      proc {
+        cmd := exeFile.toString
+        args := #["genCore"]
+        env := ← getAugmentedEnv
+      }
+    return (dataFile, trace)
+
+library_facet docs (lib) : FilePath := do
+  -- Ordering is important. The index file is generated by walking through the
+  -- filesystem directory. Files copied from the shell scripts need to exist
+  -- prior to this.
+  let mods ← lib.modules.fetch
+  let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
+  let coreJob : BuildJob FilePath ← coreDocs.fetch
+  let exeJob ← «doc-gen4».fetch
+  -- Shared with DocGen4.Output
+  let basePath := (←getWorkspace).root.buildDir / "doc"
+  let dataFile := basePath / "declarations" / "declaration-data.bmp"
+  let staticFiles := #[
+    basePath / "style.css",
+    basePath / "declaration-data.js",
+    basePath / "color-scheme.js",
+    basePath / "nav.js",
+    basePath / "jump-src.js",
+    basePath / "expand-nav.js",
+    basePath / "how-about.js",
+    basePath / "search.js",
+    basePath / "mathjax-config.js",
+    basePath / "instances.js",
+    basePath / "importedBy.js",
+    basePath / "index.html",
+    basePath / "404.html",
+    basePath / "navbar.html",
+    basePath / "search.html",
+    basePath / "find" / "index.html",
+    basePath / "find" / "find.js",
+    basePath / "src"  / "alectryon.css",
+    basePath / "src"  / "alectryon.js",
+    basePath / "src"  / "docutils_basic.css",
+    basePath / "src"  / "pygments.css"
+  ]
+  coreJob.bindAsync fun _ coreInputTrace => do
+    exeJob.bindAsync fun exeFile exeTrace => do
+      moduleJobs.bindSync fun _ inputTrace => do
+        let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
+        let trace ← buildFileUnlessUpToDate dataFile depTrace do
+          logInfo "Documentation indexing"
+          proc {
+            cmd := exeFile.toString
+            args := #["index"]
+          }
+        let traces ← staticFiles.mapM computeTrace
+        let indexTrace := mixTraceArray traces
+
+        return (dataFile, trace.mix indexTrace)
+
+-- ========================================
+-- Bookshelf
+-- ========================================
+
 @[default_target]
 lean_lib «Bookshelf» {
   roots := #[`Bookshelf, `Common]
 }
+
+/--
+The contents of our `.env` file.
+-/
+structure Config where
+  port : Nat := 5555
+
+/--
+Read in the `.env` file into an in-memory structure.
+-/
+private def readConfig : StateT Config ScriptM Unit := do
+  let env <- IO.FS.readFile ".env"
+  for line in env.trim.split (fun c => c == '\n') do
+    match line.split (fun c => c == '=') with
+    | ["PORT", port] => modify (fun c => { c with port := String.toNat! port })
+    | _ => error "Malformed `.env` file."
+  return ()
+
+/--
+Start an HTTP server for locally serving documentation. It is expected the
+documentation has already been generated prior via
+
+```bash
+> lake build Bookshelf:docs
+```
+
+USAGE:
+  lake run server
+-/
+script server (_args) do
+  let ((), config) <- StateT.run readConfig {}
+  IO.println s!"Running Lean on `http://localhost:{config.port}`"
+  _ <- IO.Process.run {
+    cmd := "python3",
+    args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
+  }
+  return 0

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.3.0-rc1

scripts/run_pdflatex.sh

@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+if ! command -v pdflatex > /dev/null; then
+  >&2 echo 'pdflatex was not found in the current $PATH.'
+  exit 1
+fi
+
+BUILD_DIR="$1"
+
+function process_file () {
+  REL_DIR=$(dirname "$1")
+  REL_BASE=$(basename -s ".tex" "$1")
+  mkdir -p "$BUILD_DIR/doc/$REL_DIR"
+  (cd "$REL_DIR" && pdflatex "$REL_BASE.tex")
+  cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/"
+}
+
+export BUILD_DIR
+export -f process_file
+
+# We run this command twice to allow any cross-references to resolve correctly.
+# https://tex.stackexchange.com/questions/41539/does-hyperref-work-between-two-files
+for _ in {1..2}; do
+  find ./* \( -path build -o -path lake-packages \) -prune -o -name "*.tex" -print0 \
+    | xargs -0 -I{} bash -c "process_file {}"
+done

static/alectryon/alectryon.css

@@ -0,0 +1,777 @@
+@charset "UTF-8";
+/*
+Copyright © 2019 Clément Pit-Claudel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+*/
+
+/*******************************/
+/* CSS reset for .alectryon-io */
+/*******************************/
+
+.alectryon-io blockquote {
+    line-height: inherit;
+}
+
+.alectryon-io blockquote:after {
+    display: none;
+}
+
+.alectryon-io label {
+    display: inline;
+    font-size: inherit;
+    margin: 0;
+}
+
+.alectryon-io a {
+    text-decoration: none !important;
+    font-style: oblique !important;
+    color: unset;
+}
+
+/* Undo <small> and <blockquote>, added to improve RSS rendering. */
+
+.alectryon-io small.alectryon-output,
+.alectryon-io small.alectryon-type-info {
+    font-size: inherit;
+}
+
+.alectryon-io blockquote.alectryon-goal,
+.alectryon-io blockquote.alectryon-message {
+    font-weight: normal;
+    font-size: inherit;
+}
+
+/***************/
+/* Main styles */
+/***************/
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .comment,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-mref,
+.alectryon-block, .alectryon-io,
+.alectryon-toggle-label, .alectryon-banner {
+    font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
+    font-size: 0.875em;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+    line-height: initial;
+}
+
+.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
+    overflow: visible;
+    overflow-wrap: break-word;
+    position: relative;
+    white-space: pre-wrap;
+}
+
+/*
+CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
+respects the user's `bidi-display-reordering` setting), so don't turn it off
+here either.  But beware unexpected results like `Definition test_אב := 0.`
+
+.alectryon-io span {
+    direction: ltr;
+    unicode-bidi: bidi-override;
+}
+
+In any case, make an exception for comments:
+
+.highlight .c {
+    direction: embed;
+    unicode-bidi: initial;
+}
+*/
+
+.alectryon-mref,
+.alectryon-mref-marker {
+    align-self: center;
+    box-sizing: border-box;
+    display: inline-block;
+    font-size: 80%;
+    font-weight: bold;
+    line-height: 1;
+    box-shadow: 0 0 0 1pt black;
+    padding: 1pt 0.3em;
+    text-decoration: none;
+}
+
+.alectryon-block .alectryon-mref-marker,
+.alectryon-io .alectryon-mref-marker {
+    user-select: none;
+    margin: -0.25em 0 -0.25em 0.5em;
+}
+
+.alectryon-inline .alectryon-mref-marker {
+    margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
+}
+
+.alectryon-mref {
+    color: inherit;
+    margin: -0.5em 0.25em;
+}
+
+.alectryon-goal:target .goal-separator .alectryon-mref-marker,
+:target > .alectryon-mref-marker {
+    animation: blink 0.2s step-start 0s 3 normal none;
+    background-color: #fcaf3e;
+    position: relative;
+}
+
+@keyframes blink {
+    50% {
+        box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
+        z-index: 10;
+    }
+}
+
+.alectryon-toggle,
+.alectryon-io .alectryon-extra-goal-toggle {
+    display: none;
+}
+
+.alectryon-bubble,
+.alectryon-io label,
+.alectryon-toggle-label {
+    cursor: pointer;
+}
+
+.alectryon-toggle-label {
+    display: block;
+    font-size: 0.8em;
+}
+
+.alectryon-io .alectryon-input {
+    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
+}
+
+.alectryon-io .alectryon-token {
+    white-space: pre-wrap;
+    display: inline;
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
+    /* FIXME if keywords were ‘bolder’ we wouldn't need !important */
+    font-weight: bold !important; /* Use !important to avoid a * selector */
+}
+
+.alectryon-bubble:before,
+.alectryon-toggle-label:before,
+.alectryon-io label.alectryon-input:after,
+.alectryon-io .alectryon-goal > label:before {
+    border: 1px solid #babdb6;
+    border-radius: 1em;
+    box-sizing: border-box;
+    content: '';
+    display: inline-block;
+    font-weight: bold;
+    height: 0.25em;
+    margin-bottom: 0.15em;
+    vertical-align: middle;
+    width: 0.75em;
+}
+
+.alectryon-toggle-label:before,
+.alectryon-io .alectryon-goal > label:before {
+    margin-right: 0.25em;
+}
+
+.alectryon-io .alectryon-goal > label:before {
+    margin-top: 0.125em;
+}
+
+.alectryon-io label.alectryon-input {
+    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
+}
+
+.alectryon-io label.alectryon-input:after {
+    margin-left: 0.25em;
+    margin-right: -1em; /* Compensate for the anti-wrapping space */
+}
+
+.alectryon-failed {
+    /* Underlines are broken in Chrome (they reset at each element boundary)… */
+    /* text-decoration: red wavy underline; */
+    /* … but it isn't too noticeable with dots */
+    text-decoration: red dotted underline;
+    text-decoration-skip-ink: none;
+    /* Chrome prints background images in low resolution, yielding a blurry underline */
+    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
+}
+
+/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
+   doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
+   hide its output causes it to remain visible (its :hover state gets triggered.
+   We only do it for the default style though, since other styles don't put the
+   output over the main text, so showing too much is not an issue. */
+@media (any-hover: hover) {
+    .alectryon-bubble:hover:before,
+    .alectryon-toggle-label:hover:before,
+    .alectryon-io label.alectryon-input:hover:after {
+        background: #eeeeec;
+    }
+
+    .alectryon-io label.alectryon-input:hover {
+        text-decoration: underline dotted #babdb6;
+	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
+    }
+
+    .alectryon-io .alectryon-sentence:hover .alectryon-output,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
+        z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
+    }
+}
+
+.alectryon-toggle:checked + .alectryon-toggle-label:before,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
+    background-color: #babdb6;
+    border-color: #babdb6;
+}
+
+/* Disable clicks on sentences when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
+    cursor: unset;
+    pointer-events: none;
+}
+
+/* Hide individual checkboxes when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
+    display: none;
+}
+
+/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
+.alectryon-io .alectryon-output {
+    box-sizing: border-box;
+    display: none;
+    left: 0;
+    right: 0;
+    position: absolute;
+    padding: 0.25em 0;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+}
+
+.alectryon-io .alectryon-type-info-wrapper {
+    position: absolute;
+    display: inline-block;
+    width: 100%;
+}
+
+.alectryon-io .alectryon-type-info-wrapper.full-width {
+    left: 0;
+    min-width: 100%;
+    max-width: 100%;
+}
+
+.alectryon-io .alectryon-type-info .goal-separator {
+    height: unset;
+    margin-top: 0em;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
+    box-sizing: border-box;
+    bottom: 100%;
+    position: absolute;
+    /*padding: 0.25em 0;*/
+    visibility: hidden;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+    white-space: pre-wrap !important;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
+    white-space: pre-wrap !important;
+}
+
+@media (any-hover: hover) { /* See note above about this @media query */
+    .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: block;
+    }
+
+    .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: none !important;
+    }
+
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        /*visibility: hidden !important;*/
+    }
+
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        visibility: visible;
+        transition-delay: 0.5s;
+    }
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
+    display: block;
+}
+
+/* Indicate active (hovered or targeted) goals with a shadow. */
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals,
+.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+    box-shadow: 2px 2px 2px gray;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
+    display: none;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
+    /* Dashes indicate that the hypotheses are hidden */
+    border-top-style: dashed;
+}
+
+
+/* Show just a small preview of the other goals; this is undone by the
+   "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
+    max-height: 5.2em;
+    overflow-y: auto;
+    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
+       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
+    vertical-align: middle;
+}
+
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-messages {
+    background: #f6f7f6;
+	/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
+    display: block;
+    padding: 0.25em;
+}
+
+.alectryon-message::before {
+    content: '';
+    float: right;
+    /* etc/svg/square-bubble-xl.svg */
+    background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
+    height: 14px;
+    width: 14px;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container {
+    width: unset;
+}
+
+/* Show goals when a toggle is set */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
+    display: block;
+    position: static;
+    width: unset;
+    background: unset; /* Override the backgrounds set in floating in windowed mode */
+    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
+}
+
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
+    /* Overridden back in windowed style */
+    flex-flow: row wrap;
+    justify-content: flex-start;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+    display: block;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
+    display: flex;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
+    display: none;
+}
+
+.alectryon-io .alectryon-messages,
+.alectryon-io .alectryon-message,
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-goal,
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    border-radius: 0.15em;
+}
+
+.alectryon-io .alectryon-goal,
+.alectryon-io .alectryon-message {
+    align-items: center;
+    background: #f6f7f6;
+    border: 0em;
+    display: block;
+    flex-direction: column;
+    margin: 0.25em;
+    padding: 0.5em;
+    position: relative;
+}
+
+.alectryon-io .goal-hyps {
+    align-content: space-around;
+    align-items: baseline;
+    display: flex;
+    flex-flow: column nowrap; /* re-stated in windowed mode */
+    justify-content: space-around;
+    /* LATER use a ‘gap’ property instead of margins once supported */
+    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
+    padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
+}
+
+.alectryon-io .goal-hyps > br {
+    display: none; /* Only for RSS readers */
+}
+
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    /*background: #eeeeec;*/
+    display: inline-block;
+    padding: 0.15em 0.35em;
+}
+
+.alectryon-io .goal-hyps > span {
+    align-items: baseline;
+    display: inline-flex;
+    margin: 0.15em 0.25em;
+}
+
+.alectryon-block var,
+.alectryon-inline var,
+.alectryon-io .goal-hyps > span > var {
+    font-weight: 600;
+    font-style: unset;
+}
+
+.alectryon-io .goal-hyps > span > var {
+    /* Shrink the list of names, but let it grow as long as space is available. */
+    flex-basis: min-content;
+    flex-grow: 1;
+}
+
+.alectryon-io .goal-hyps > span b {
+    font-weight: 600;
+    margin: 0 0 0 0.5em;
+    white-space: pre;
+}
+
+.alectryon-io .hyp-body,
+.alectryon-io .hyp-type {
+    display: flex;
+    align-items: baseline;
+}
+
+.alectryon-io .goal-separator {
+    align-items: center;
+    display: flex;
+    flex-direction: row;
+    height: 1em; /* Fixed height to ignore goal name and markers */
+    margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
+}
+
+.alectryon-io .goal-separator hr {
+    border: none;
+    border-top: thin solid #555753;
+    display: block;
+    flex-grow: 1;
+    margin: 0;
+}
+
+.alectryon-io .goal-separator .goal-name {
+    font-size: 0.75em;
+    margin-left: 0.5em;
+}
+
+/**********/
+/* Banner */
+/**********/
+
+.alectryon-banner {
+    background: #eeeeec;
+    border: 1px solid #babcbd;
+    font-size: 0.75em;
+    padding: 0.25em;
+    text-align: center;
+    margin: 1em 0;
+}
+
+.alectryon-banner a {
+    cursor: pointer;
+    text-decoration: underline;
+}
+
+.alectryon-banner kbd {
+    background: #d3d7cf;
+    border-radius: 0.15em;
+    border: 1px solid #babdb6;
+    box-sizing: border-box;
+    display: inline-block;
+    font-family: inherit;
+    font-size: 0.9em;
+    height: 1.3em;
+    line-height: 1.2em;
+    margin: -0.25em 0;
+    padding: 0 0.25em;
+    vertical-align: middle;
+}
+
+/**********/
+/* Toggle */
+/**********/
+
+.alectryon-toggle-label {
+    margin: 1rem 0;
+}
+
+/******************/
+/* Floating style */
+/******************/
+
+/* If there's space, display goals to the right of the code, not below it. */
+@media (min-width: 80rem) {
+    /* Unlike the windowed case, we don't want to move output blocks to the side
+       when they are both :checked and -targeted, since it gets confusing as
+       things jump around; hence the commented-output part of the selector,
+       which would otherwise increase specificity */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        top: 0;
+        left: 100%;
+        right: -100%;
+        padding: 0 0.5em;
+        position:  absolute;
+    }
+
+    .alectryon-floating .alectryon-output {
+        min-height: 100%;
+    }
+
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        background: white; /* Ensure that short goals hide long ones */
+    }
+
+    /* This odd margin-bottom property prevents the sticky div from bumping
+       against the bottom of its container (.alectryon-output).  The alternative
+       would be enlarging .alectryon-output, but that would cause overflows,
+       enlarging scrollbars and yielding scrolling towards the bottom of the
+       page.  Doing things this way instead makes it possible to restrict
+       .alectryon-output to a reasonable size (100%, through top = bottom = 0).
+       See also https://stackoverflow.com/questions/43909940/. */
+    /* See note on specificity above */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
+        margin-bottom: -200%;
+        position: sticky;
+        top: 0;
+    }
+
+    .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+    .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+        margin-bottom: unset; /* Undo the margin */
+    }
+
+    /* Float underneath the current fragment
+    @media (max-width: 80rem) {
+        .alectryon-floating .alectryon-output {
+            top: 100%;
+        }
+    } */
+}
+
+/********************/
+/* Multi-pane style */
+/********************/
+
+.alectryon-windowed {
+    border: 0 solid #2e3436;
+    box-sizing: border-box;
+}
+
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
+    background: white; /* Ensure that short goals hide long ones */
+}
+
+.alectryon-windowed .alectryon-output {
+    position: fixed; /* Overwritten by the ‘:checked’ rules */
+}
+
+/* See note about specificity below */
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    padding: 0.5em;
+    overflow-y: auto; /* Windowed contents may need to scroll */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals {
+    box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
+    /* Restated to override the :checked style */
+    flex-flow: column nowrap;
+    justify-content: space-around;
+}
+
+
+.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
+/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-windowed .alectryon-output > div {
+    display: flex; /* Put messages after goals */
+    flex-direction: column-reverse;
+}
+
+/*********************/
+/* Standalone styles */
+/*********************/
+
+.alectryon-standalone {
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+@media screen and (min-width: 50rem) {
+    html.alectryon-standalone {
+        /* Prevent flickering when hovering a block causes scrollbars to appear. */
+        margin-left: calc(100vw - 100%);
+        margin-right: 0;
+    }
+}
+
+/* Coqdoc */
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-coqdoc .doc .comment {
+    display: inline;
+}
+
+.alectryon-coqdoc .doc .comment {
+    color: #eeeeec;
+}
+
+.alectryon-coqdoc .doc .paragraph {
+    height: 0.75em;
+}
+
+/* Centered, Floating */
+
+.alectryon-standalone .alectryon-centered,
+.alectryon-standalone .alectryon-floating {
+    max-width: 50rem;
+    margin: auto;
+}
+
+@media (min-width: 80rem) {
+    .alectryon-standalone .alectryon-floating {
+        max-width: 80rem;
+    }
+
+    .alectryon-standalone .alectryon-floating > * {
+        width: 50%;
+        margin-left: 0;
+    }
+}
+
+/* Windowed */
+
+.alectryon-standalone .alectryon-windowed {
+    display: block;
+    margin: 0;
+    overflow-y: auto;
+    position: absolute;
+    padding: 0 1em;
+}
+
+.alectryon-standalone .alectryon-windowed > * {
+    /* Override properties of docutils_basic.css */
+    margin-left: 0;
+    max-width: unset;
+}
+
+.alectryon-standalone .alectryon-windowed .alectryon-io {
+    box-sizing: border-box;
+    width: 100%;
+}
+
+/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
+   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
+   ‘position’ to ‘static’ */
+
+
+/* Specificity: We want the output to stay inline when hovered while unfolded
+   (:checked), but we want it to move when it's targeted (i.e. when the user
+   is browsing goals one by one using the keyboard, in which case we want to
+   goals to appear in consistent locations).  The selectors below ensure
+   that :hover < :checked < -targeted in terms of specificity. */
+/* LATER: Reimplement this stuff with CSS variables */
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    position: fixed;
+}
+
+@media screen and (min-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-right-width: thin;
+        bottom: 0;
+        left: 0;
+        right: 50%;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 50%;
+        right: 0;
+        top: 0;
+    }
+}
+
+@media screen and (max-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-bottom-width: 1px;
+        bottom: 40%;
+        left: 0;
+        right: 0;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 0;
+        right: 0;
+        top: 60%;
+    }
+}

static/alectryon/alectryon.js

@@ -0,0 +1,172 @@
+var Alectryon;
+(function(Alectryon) {
+    (function (slideshow) {
+        function anchor(sentence) { return "#" + sentence.id; }
+
+        function current_sentence() { return slideshow.sentences[slideshow.pos]; }
+
+        function unhighlight() {
+            var sentence = current_sentence();
+            if (sentence) sentence.classList.remove("alectryon-target");
+            slideshow.pos = -1;
+        }
+
+        function highlight(sentence) {
+            sentence.classList.add("alectryon-target");
+        }
+
+        function scroll(sentence) {
+            // Put the top of the current fragment close to the top of the
+            // screen, but scroll it out of view if showing it requires pushing
+            // the sentence past half of the screen.  If sentence is already in
+            // a reasonable position, don't move.
+            var parent = sentence.parentElement;
+            /* We want to scroll the whole document, so start at root… */
+            while (parent && !parent.classList.contains("alectryon-root"))
+                parent = parent.parentElement;
+            /* … and work up from there to find a scrollable element.
+               parent.scrollHeight can be greater than parent.clientHeight
+               without showing scrollbars, so we add a 10px buffer. */
+            while (parent && parent.scrollHeight <= parent.clientHeight + 10)
+                parent = parent.parentElement;
+            /* <body> and <html> elements can have their client rect overflow
+             * the window if their height is unset, so scroll the window
+             * instead */
+            if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
+                parent = null;
+
+            var rect = function(e) { return e.getBoundingClientRect(); };
+            var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
+                sentence_y = rect(sentence).y - parent_box.y,
+                fragment_y = rect(sentence.parentElement).y - parent_box.y;
+
+            // The assertion below sometimes fails for the first element in a block.
+            // console.assert(sentence_y >= fragment_y);
+
+            if (sentence_y < 0.1 * parent_box.height ||
+                sentence_y > 0.7 * parent_box.height) {
+                (parent || window).scrollBy(
+                    0, Math.max(sentence_y - 0.5 * parent_box.height,
+                                fragment_y - 0.1 * parent_box.height));
+            }
+        }
+
+        function highlighted(pos) {
+            return slideshow.pos == pos;
+        }
+
+        function navigate(pos, inhibitScroll) {
+            unhighlight();
+            slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
+            var sentence = current_sentence();
+            highlight(sentence);
+            if (!inhibitScroll)
+                scroll(sentence);
+        }
+
+        var keys = {
+            PAGE_UP: 33,
+            PAGE_DOWN: 34,
+            ARROW_UP: 38,
+            ARROW_DOWN: 40,
+            h: 72, l: 76, p: 80, n: 78
+        };
+
+        function onkeydown(e) {
+            e = e || window.event;
+            if (e.ctrlKey || e.metaKey) {
+                if (e.keyCode == keys.ARROW_UP)
+                    slideshow.previous();
+                else if (e.keyCode == keys.ARROW_DOWN)
+                    slideshow.next();
+                else
+                    return;
+            } else {
+                // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
+                //     slideshow.previous();
+                // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
+                //     slideshow.next();
+                // else
+                return;
+            }
+            e.preventDefault();
+        }
+
+        function start() {
+            slideshow.navigate(0);
+        }
+
+        function toggleHighlight(idx) {
+            if (highlighted(idx))
+                unhighlight();
+            else
+                navigate(idx, true);
+        }
+
+        function handleClick(evt) {
+            if (evt.ctrlKey || evt.metaKey) {
+                var sentence = evt.currentTarget;
+
+                // Ensure that the goal is shown on the side, not inline
+                var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
+                if (checkbox)
+                    checkbox.checked = false;
+
+                toggleHighlight(sentence.alectryon_index);
+                evt.preventDefault();
+            }
+        }
+
+        function init() {
+            document.onkeydown = onkeydown;
+            slideshow.pos = -1;
+            slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
+            slideshow.sentences.forEach(function (s, idx) {
+                s.addEventListener('click', handleClick, false);
+                s.alectryon_index = idx;
+            });
+        }
+
+        slideshow.start = start;
+        slideshow.end = unhighlight;
+        slideshow.navigate = navigate;
+        slideshow.next = function() { navigate(slideshow.pos + 1); };
+        slideshow.previous = function() { navigate(slideshow.pos + -1); };
+        window.addEventListener('DOMContentLoaded', init);
+    })(Alectryon.slideshow || (Alectryon.slideshow = {}));
+
+    (function (styles) {
+        var styleNames = ["centered", "floating", "windowed"];
+
+        function className(style) {
+            return "alectryon-" + style;
+        }
+
+        function setStyle(style) {
+            var root = document.getElementsByClassName("alectryon-root")[0];
+            styleNames.forEach(function (s) {
+                root.classList.remove(className(s)); });
+            root.classList.add(className(style));
+        }
+
+        function init() {
+            var banner = document.getElementsByClassName("alectryon-banner")[0];
+            if (banner) {
+                banner.append(" Style: ");
+                styleNames.forEach(function (styleName, idx) {
+                    var s = styleName;
+                    var a = document.createElement("a");
+                    a.onclick = function() { setStyle(s); };
+                    a.append(styleName);
+                    if (idx > 0) banner.append("; ");
+                    banner.appendChild(a);
+                });
+                banner.append(".");
+            }
+        }
+
+        window.addEventListener('DOMContentLoaded', init);
+
+        styles.setStyle = setStyle;
+    })(Alectryon.styles || (Alectryon.styles = {}));
+})(Alectryon || (Alectryon = {}));

static/alectryon/docutils_basic.css

@@ -0,0 +1,593 @@
+/******************************************************************************
+The MIT License (MIT)
+
+Copyright (c) 2014 Matthias Eisen
+Further changes Copyright (c) 2020, 2021 Clément Pit-Claudel
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+******************************************************************************/
+
+kbd,
+pre,
+samp,
+tt,
+body code, /* Increase specificity to override IBM's stylesheet */
+body code.highlight,
+.docutils.literal {
+    font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+}
+
+body {
+    color: #111;
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+main, div.document {
+    margin: 0 auto;
+    max-width: 720px;
+}
+
+
+/* ========== Headings ========== */
+
+h1, h2, h3, h4, h5, h6 {
+    font-weight: normal;
+    margin-top: 1.5em;
+}
+
+h1.section-subtitle, 
+h2.section-subtitle, 
+h3.section-subtitle,
+h4.section-subtitle, 
+h5.section-subtitle, 
+h6.section-subtitle {
+    margin-top: 0.4em;
+}
+
+h1.title {
+    text-align: center;
+}
+
+h2.subtitle {
+    text-align: center;
+}
+
+span.section-subtitle {
+    font-size: 80%,
+}
+
+/* //-------- Headings ---------- */
+
+
+/* ========== Images ========== */
+
+img, 
+.figure, 
+object {
+    display:        block;
+    margin-left:    auto;
+    margin-right:   auto;
+}
+
+div.figure {
+    margin-left:    2em;
+    margin-right:   2em;
+}
+
+img.align-left, .figure.align-left, object.align-left {
+    clear:          left;
+    float:          left;
+    margin-right:   1em;
+}
+
+img.align-right, .figure.align-right, object.align-right {
+    clear:          right;
+    float:          right;
+    margin-left:    1em;
+}
+
+img.align-center, .figure.align-center, object.align-center {
+    display:        block;
+    margin-left:    auto;
+    margin-right:   auto;
+}
+
+/* reset inner alignment in figures */
+div.align-right {
+    text-align: inherit;
+}
+
+object[type="image/svg+xml"], 
+object[type="application/x-shockwave-flash"] {
+    overflow: hidden;
+}
+
+/* //-------- Images ---------- */
+
+
+
+/* ========== Literal Blocks ========== */
+
+.docutils.literal {
+    background-color: #eee;
+    padding: 0 0.2em;
+    border-radius: 0.1em;
+}
+
+pre.address {
+    margin-bottom: 0;
+    margin-top: 0;
+    font: inherit;
+}
+
+pre.literal-block {
+    border-left: solid 5px #ccc;
+    padding: 1em; 
+}
+
+pre.literal-block, pre.doctest-block, pre.math, pre.code {
+}
+
+span.interpreted {
+}
+
+span.pre {
+    white-space: pre;
+}
+
+pre.code .ln { 
+    color: grey; 
+}
+pre.code, code {
+    border-style: none;
+    /* ! padding: 1em 0; */ /* Removed because that large hitbox bleeds over links on other lines */
+}
+pre.code .comment, code .comment { 
+    color: #888;
+}
+pre.code .keyword, code .keyword {
+    font-weight: bold; 
+    color: #080;
+}
+pre.code .literal.string, code .literal.string { 
+    color: #d20;
+    background-color: #fff0f0;
+}
+pre.code .literal.number, code .literal.number { 
+    color: #00d;
+}
+pre.code .name.builtin, code .name.builtin {
+    color: #038;
+    color: #820;
+}
+pre.code .name.namespace, code .name.namespace {
+    color: #b06;
+}
+pre.code .deleted, code .deleted {
+    background-color: #fdd;
+}
+pre.code .inserted, code .inserted {
+    background-color: #dfd;
+}
+
+
+/* //-------- Literal Blocks --------- */
+
+
+/* ========== Tables ========== */
+
+table {
+    border-spacing:         0;
+    border-collapse:        collapse;
+    border-style:           none;
+    border-top:             solid thin #111;
+    border-bottom:          solid thin #111;
+}
+
+td, 
+th {
+    border: none;
+    padding:                0.5em;
+    vertical-align:         top;
+}
+
+th {
+    border-top:             solid thin #111;
+    border-bottom:          solid thin #111;
+    background-color:       #ddd;
+}
+
+
+table.field-list,
+table.footnote,
+table.citation,
+table.option-list {
+    border:                 none;
+}
+table.docinfo {
+    margin:                 2em 4em;
+}
+
+table.docutils {
+    margin:                 1em 0;
+}
+
+table.docutils th.field-name, 
+table.docinfo th.docinfo-name {
+    border:                 none;
+    background:             none;
+    font-weight:            bold ;
+    text-align:             left ;
+    white-space:            nowrap ;
+    padding-left:           0;
+    vertical-align:         middle; 
+}
+
+table.docutils.booktabs {
+    border:                 none;
+    border-top:             medium solid;
+    border-bottom:          medium solid;
+    border-collapse:        collapse;
+}
+
+table.docutils.booktabs * {
+    border:                 none;
+}
+table.docutils.booktabs th {
+    border-bottom:          thin solid;
+    text-align:             left;
+}
+
+span.option {
+    white-space: nowrap;
+}
+
+table caption {
+    margin-bottom: 2px;
+}
+
+/* //-------- Tables ---------- */
+
+
+/* ========== Lists ========== */
+
+ol.simple, ul.simple {
+    margin-bottom: 1em;
+}
+
+ol.arabic {
+    list-style: decimal;
+}
+
+ol.loweralpha {
+    list-style: lower-alpha;
+}
+
+ol.upperalpha {
+    list-style: upper-alpha;
+}
+
+ol.lowerroman {
+    list-style: lower-roman;
+}
+
+ol.upperroman {
+    list-style: upper-roman;
+}
+
+dl.docutils dd {
+    margin-bottom: 0.5em;
+}
+
+
+dl.docutils dt {
+    font-weight: bold;
+}
+
+/* //-------- Lists ---------- */
+
+
+/* ========== Sidebar ========== */
+
+div.sidebar {
+    margin: 0 0 0.5em 1em ;
+    border-left: solid medium #111;
+    padding: 1em ;
+    width: 40% ;
+    float: right ;
+    clear: right;
+}
+
+div.sidebar {
+    font-size: 0.9rem;
+}
+
+p.sidebar-title {
+    font-size: 1rem;
+    font-weight: bold ;
+}
+
+p.sidebar-subtitle {
+    font-weight: bold;
+}
+
+/* //-------- Sidebar ---------- */
+
+
+/* ========== Topic ========== */
+
+div.topic {
+    border-left: thin solid #111;
+    padding-left: 1em;
+}
+
+div.topic p {
+    padding: 0;
+}
+
+p.topic-title {
+    font-weight: bold;
+}
+
+/* //-------- Topic ---------- */
+
+
+/* ========== Header ========== */
+
+div.header {
+    font-family:        "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
+    font-size:          0.9rem;
+    margin:             2em auto 4em auto;
+    max-width:          960px;
+    clear:              both;
+}
+
+hr.header {
+    border:             0;
+    height:             1px;
+    margin-top:         1em;
+    background-color:   #111;
+}
+
+/* //-------- Header ---------- */
+
+
+/* ========== Footer ========== */
+
+div.footer {
+    font-family:        "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
+    font-size:          0.9rem;
+    margin:             6em auto 2em auto;
+    max-width:          960px;
+    clear:              both;
+    text-align:         center;
+}
+
+hr.footer {
+    border:             0;
+    height:             1px;
+    margin-bottom:      2em;
+    background-color:   #111;
+}
+
+/* //-------- Footer ---------- */
+
+
+/* ========== Admonitions ========== */
+
+div.admonition, 
+div.attention, 
+div.caution, 
+div.danger, 
+div.error,
+div.hint, 
+div.important, 
+div.note, 
+div.tip, 
+div.warning {
+    border: solid thin #111;
+    padding: 0 1em;
+}
+
+div.error,
+div.danger {
+    border-color: #a94442;
+    background-color: #f2dede;
+}
+
+div.hint,
+div.tip {
+    border-color: #31708f;
+    background-color: #d9edf7;
+}
+
+div.attention,
+div.caution,
+div.warning {
+    border-color: #8a6d3b;
+    background-color: #fcf8e3; 
+}
+
+div.hint p.admonition-title,
+div.tip p.admonition-title {
+    color: #31708f;
+    font-weight: bold ;
+}
+
+div.note p.admonition-title,
+div.admonition p.admonition-title, 
+div.important p.admonition-title {
+    font-weight: bold ;
+}
+
+div.attention p.admonition-title,
+div.caution p.admonition-title,
+div.warning p.admonition-title {
+    color: #8a6d3b;
+    font-weight: bold ;
+}
+
+div.danger p.admonition-title, 
+div.error p.admonition-title,
+.code .error {
+    color: #a94442;
+    font-weight: bold ;
+}
+
+/* //-------- Admonitions ---------- */
+
+
+/* ========== Table of Contents ========== */
+
+div.contents {
+    margin: 2em 0;
+    border: none;
+}
+
+ul.auto-toc {
+    list-style-type: none;
+}
+
+a.toc-backref {
+    text-decoration: none ;
+    color: #111;
+}
+
+/* //-------- Table of Contents ---------- */
+
+
+
+/* ========== Line Blocks========== */
+
+div.line-block {
+    display: block ;
+    margin-top: 1em ;
+    margin-bottom: 1em;
+}
+
+div.line-block div.line-block {
+    margin-top: 0 ;
+    margin-bottom: 0 ;
+    margin-left: 1.5em;
+}
+
+/* //-------- Line Blocks---------- */
+
+
+/* ========== System Messages ========== */
+
+div.system-messages {
+    margin: 5em;
+}
+
+div.system-messages h1 {
+    color: red;
+}
+
+div.system-message {
+    border: medium outset ;
+    padding: 1em;
+}
+
+div.system-message p.system-message-title {
+    color: red ;
+    font-weight: bold;
+}
+
+/* //-------- System Messages---------- */
+
+
+/* ========== Helpers ========== */
+
+.hidden {
+    display: none;
+}
+
+.align-left {
+    text-align: left;
+}
+
+.align-center {
+    clear: both ;
+    text-align: center;
+}
+
+.align-right {
+    text-align: right;
+}
+
+/* //-------- Helpers---------- */
+
+
+p.caption {
+    font-style: italic;
+    text-align: center;
+}
+
+p.credits {
+font-style: italic ;
+font-size: smaller }
+
+p.label {
+white-space: nowrap }
+
+p.rubric {
+font-weight: bold ;
+font-size: larger ;
+color: maroon ;
+text-align: center }
+
+p.attribution {
+text-align: right ;
+margin-left: 50% }
+
+blockquote.epigraph {
+    margin: 2em 5em;
+}
+
+div.abstract {
+margin: 2em 5em }
+
+div.abstract {
+font-weight: bold ;
+text-align: center }
+
+div.dedication {
+margin: 2em 5em ;
+text-align: center ;
+font-style: italic }
+
+div.dedication {
+font-weight: bold ;
+font-style: normal }
+
+
+span.classifier {
+font-style: oblique }
+
+span.classifier-delimiter {
+font-weight: bold }
+
+span.problematic {
+color: red }
+
+
+

static/alectryon/pygments.css

@@ -0,0 +1,82 @@
+/* Pygments stylesheet generated by Alectryon (style=None) */
+/* Most of the following are unused as of now */
+td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+.highlight .hll, .code .hll { background-color: #ffffcc }
+.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
+.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
+.highlight .g, .code .g { color: #000000 } /* Generic */
+.highlight .k, .code .k { color: #8f5902 } /* Keyword */
+.highlight .l, .code .l { color: #2e3436 } /* Literal */
+.highlight .n, .code .n { color: #000000 } /* Name */
+.highlight .o, .code .o { color: #000000 } /* Operator */
+.highlight .x, .code .x { color: #2e3436 } /* Other */
+.highlight .p, .code .p { color: #000000 } /* Punctuation */
+.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
+.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
+.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
+.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
+.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
+.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
+.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
+.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
+.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
+.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
+.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
+.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
+.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
+.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
+.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
+.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
+.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
+.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
+.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
+.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
+.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
+.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
+.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
+.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
+.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
+.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
+.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
+.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
+.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
+.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
+.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
+.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
+.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
+.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
+.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
+.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
+.highlight .py, .code .py { color: #000000 } /* Name.Property */
+.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
+.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
+.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
+.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
+.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
+.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
+.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
+.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
+.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
+.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
+.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
+.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
+.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
+.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
+.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
+.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
+.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
+.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
+.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
+.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
+.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
+.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
+.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
+.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
+.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
+.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
+.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
+.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
+.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */

static/color-scheme.js

@@ -0,0 +1,33 @@
+function getTheme() {
+    return localStorage.getItem("theme") || "system";
+}
+
+function setTheme(themeName) {
+    localStorage.setItem('theme', themeName);
+    if (themeName == "system") {
+        themeName = parent.matchMedia("(prefers-color-scheme: dark)").matches ? "dark" : "light";
+    }
+    // the navbar is in an iframe, so we need to set this variable in the parent document
+    for (const win of [window, parent]) {
+        win.document.documentElement.setAttribute('data-theme', themeName);
+    }
+}
+
+setTheme(getTheme())
+
+document.addEventListener("DOMContentLoaded", function() {
+    document.querySelectorAll("#color-theme-switcher input").forEach((input) => {
+        if (input.value == getTheme()) {
+            input.checked = true;
+        }
+        input.addEventListener('change', e => setTheme(e.target.value));
+    });
+
+    // also check to see if the user changes their theme settings while the page is loaded.
+    parent.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
+        setTheme(getTheme());
+    })
+});
+
+// un-hide the colorscheme picker
+document.querySelector("#settings").removeAttribute('hidden');

static/declaration-data.js

@@ -0,0 +1,272 @@
+/**
+ * This module is a wrapper that facilitates manipulating the declaration data.
+ *
+ * Please see {@link DeclarationDataCenter} for more information.
+ */
+
+const CACHE_DB_NAME = "declaration-data";
+const CACHE_DB_VERSION = 1;
+const CACHE_DB_KEY = "DECLARATIONS_KEY";
+
+/**
+ * The DeclarationDataCenter is used for declaration searching.
+ *
+ * For usage, see the {@link init} and {@link search} methods.
+ */
+export class DeclarationDataCenter {
+  /**
+   * The declaration data. Users should not interact directly with this field.
+   *
+   * *NOTE:* This is not made private to support legacy browsers.
+   */
+  declarationData = null;
+
+  /**
+   * Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
+   */
+  static requestSingleton = null;
+
+  /**
+   * Construct a DeclarationDataCenter with given data.
+   *
+   * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process.
+   * @param {*} declarationData
+   */
+  constructor(declarationData) {
+    this.declarationData = declarationData;
+  }
+
+  /**
+   * The actual constructor of DeclarationDataCenter
+   * @returns {Promise<DeclarationDataCenter>}
+   */
+  static async init() {
+    if (DeclarationDataCenter.requestSingleton === null) {
+      DeclarationDataCenter.requestSingleton = DeclarationDataCenter.getData();
+    }
+    return await DeclarationDataCenter.requestSingleton;
+  }
+
+  static async getData() {
+    const dataListUrl = new URL(
+      `${SITE_ROOT}/declarations/declaration-data.bmp`,
+      window.location
+    );
+
+    // try to use cache first
+    // TODO: This API is not thought 100% through. If we have a DB cached
+    // already it will not even ask the remote for a new one so we end up
+    // with outdated declaration-data. This has to have some form of cache
+    // invalidation: https://github.com/leanprover/doc-gen4/issues/133
+    // const data = await fetchCachedDeclarationData().catch(_e => null);
+    const data = null;
+    if (data) {
+      // if data is defined, use the cached one.
+      return new DeclarationDataCenter(data);
+    } else {
+      // undefined. then fetch the data from the server.
+      const dataListRes = await fetch(dataListUrl);
+      const data = await dataListRes.json();
+      // TODO https://github.com/leanprover/doc-gen4/issues/133
+      // await cacheDeclarationData(data);
+      return new DeclarationDataCenter(data);
+    }
+  }
+
+  /**
+   * Search for a declaration.
+   * @returns {Array<any>}
+   */
+  search(pattern, strict = true, allowedKinds = undefined, maxResults = undefined) {
+    if (!pattern) {
+      return [];
+    }
+    if (strict) {
+      let decl = this.declarationData.declarations[pattern];
+      return decl ? [decl] : [];
+    } else {
+      return getMatches(this.declarationData.declarations, pattern, allowedKinds, maxResults);
+    }
+  }
+
+  /**
+   * Search for all instances of a certain typeclass
+   * @returns {Array<String>}
+   */
+  instancesForClass(className) {
+    const instances = this.declarationData.instances[className];
+    if (!instances) {
+      return [];
+    } else {
+      return instances;
+    }
+  }
+
+  /**
+   * Search for all instances that involve a certain type
+   * @returns {Array<String>}
+   */
+  instancesForType(typeName) {
+    const instances = this.declarationData.instancesFor[typeName];
+    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<String>}
+   */
+  moduleImportedBy(moduleName) {
+    return this.declarationData.importedBy[moduleName];
+  }
+
+  /**
+   * Analogous to Lean moduleNameToLink
+   * @returns {String}
+   */
+  moduleNameToLink(moduleName) {
+    return this.declarationData.modules[moduleName];
+  }
+}
+
+function isSeparator(char) {
+  return char === "." || char === "_";
+}
+
+// HACK: the fuzzy matching is quite hacky
+
+function matchCaseSensitive(declName, lowerDeclName, pattern) {
+  let i = 0,
+    j = 0,
+    err = 0,
+    lastMatch = 0;
+  while (i < declName.length && j < pattern.length) {
+    if (pattern[j] === declName[i] || pattern[j] === lowerDeclName[i]) {
+      err += (isSeparator(pattern[j]) ? 0.125 : 1) * (i - lastMatch);
+      if (pattern[j] !== declName[i]) err += 0.5;
+      lastMatch = i + 1;
+      j++;
+    } else if (isSeparator(declName[i])) {
+      err += 0.125 * (i + 1 - lastMatch);
+      lastMatch = i + 1;
+    }
+    i++;
+  }
+  err += 0.125 * (declName.length - lastMatch);
+  if (j === pattern.length) {
+    return err;
+  }
+}
+
+function getMatches(declarations, pattern, allowedKinds = undefined, maxResults = undefined) {
+  const lowerPats = pattern.toLowerCase().split(/\s/g);
+  const patNoSpaces = pattern.replace(/\s/g, "");
+  const results = [];
+  for (const [name, {
+    kind,
+    docLink,
+  }] of Object.entries(declarations)) {
+    // Apply "kind" filter
+    if (allowedKinds !== undefined) {
+      if (!allowedKinds.has(kind)) {
+        continue;
+      }
+    }
+    const lowerName = name.toLowerCase();
+    let err = matchCaseSensitive(name, lowerName, patNoSpaces);
+    if (err !== undefined) {
+      results.push({
+        name,
+        kind,
+        err,
+        lowerName,
+        docLink,
+      });
+    }
+  }
+  return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
+}
+
+// TODO: refactor the indexedDB part to be more robust
+
+/**
+ * Get the indexedDB database, automatically initialized.
+ * @returns {Promise<IDBDatabase>}
+ */
+async function getDeclarationDatabase() {
+  return new Promise((resolve, reject) => {
+    const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION);
+
+    request.onerror = function (event) {
+      reject(
+        new Error(
+          `fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}`
+        )
+      );
+    };
+    request.onupgradeneeded = function (event) {
+      let db = event.target.result;
+      // We only need to store one object, so no key path or increment is needed.
+      db.createObjectStore("declaration");
+    };
+    request.onsuccess = function (event) {
+      resolve(event.target.result);
+    };
+  });
+}
+
+/**
+ * Store data in indexedDB object store.
+ * @param {Map<string, any>} data
+ */
+async function cacheDeclarationData(data) {
+  let db = await getDeclarationDatabase();
+  let store = db
+    .transaction("declaration", "readwrite")
+    .objectStore("declaration");
+  return new Promise((resolve, reject) => {
+    let clearRequest = store.clear();
+    let addRequest = store.add(data, CACHE_DB_KEY);
+
+    addRequest.onsuccess = function (event) {
+      resolve();
+    };
+    addRequest.onerror = function (event) {
+      reject(new Error(`fail to store declaration data`));
+    };
+    clearRequest.onerror = function (event) {
+      reject(new Error("fail to clear object store"));
+    };
+  });
+}
+
+/**
+ * Retrieve data from indexedDB database.
+ * @returns {Promise<Map<string, any>|undefined>}
+ */
+async function fetchCachedDeclarationData() {
+  let db = await getDeclarationDatabase();
+  let store = db
+    .transaction("declaration", "readonly")
+    .objectStore("declaration");
+  return new Promise((resolve, reject) => {
+    let transactionRequest = store.get(CACHE_DB_KEY);
+    transactionRequest.onsuccess = function (event) {
+      resolve(event.target.result);
+    };
+    transactionRequest.onerror = function (event) {
+      reject(new Error(`fail to store declaration data`));
+    };
+  });
+}

static/expand-nav.js

@@ -0,0 +1,24 @@
+document.querySelector('.navframe').addEventListener('load', function() {
+    // Get the current page URL without the suffix after #
+    var currentPageURL = window.location.href.split('#')[0];
+
+    // Get all anchor tags
+    var as = document.querySelector('.navframe').contentWindow.document.body.querySelectorAll('a');
+    for (const a of as) {
+        if (a.href) {
+            var href = a.href.split('#')[0];
+            // find the one with the current url
+            if (href === currentPageURL) {
+                a.style.fontStyle = 'italic';
+                // open all detail tags above the current
+                var el = a.parentNode.closest('details');
+                while (el) {
+                    el.open = true;
+                    el = el.parentNode.closest('details');
+                }
+            }
+            // seeing as we found the link we were looking for, stop
+            break;
+        }
+    }
+});

static/find/find.js

@@ -0,0 +1,94 @@
+/**
+ * This module is used for the `/find` endpoint.
+ *
+ * Two basic kinds of search syntax are supported:
+ *
+ * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
+ * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
+ *
+ * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
+ *
+ * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
+ * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
+ * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
+ * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
+ * fallback to the `#doc` view.
+ */
+
+import { DeclarationDataCenter } from "../declaration-data.js";
+
+function leanFriendlyRegExp(c) {
+  try {
+    return new RegExp("(?<!«[^»]*)" + c);
+  } catch (e) {
+    if (e instanceof SyntaxError) {
+      // Lookbehind is not implemented yet in WebKit: https://bugs.webkit.org/show_bug.cgi?id=174931
+      // Fall back to less friendly regex.
+      return new RegExp(c);
+    }
+    throw e;
+  }
+}
+
+/**
+ * We don't use browser's default hash and searchParams in case Lean declaration name
+ * can be like `«#»`, rather we manually handle the `window.location.href` with regex.
+ */
+const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/;
+const LEAN_FRIENDLY_AND_SEPARATOR = leanFriendlyRegExp("&");
+const LEAN_FRIENDLY_EQUAL_SEPARATOR = leanFriendlyRegExp("=");
+const LEAN_FRIENDLY_SLASH_SEPARATOR = leanFriendlyRegExp("/");
+
+const [_, query, fragment] = LEAN_FRIENDLY_URL_REGEX.exec(window.location.href);
+const queryParams = new Map(
+  query
+    ?.split(LEAN_FRIENDLY_AND_SEPARATOR)
+    ?.map((p) => p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
+    ?.filter((l) => l.length == 2 && l[0].length > 0)
+);
+const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
+
+const encodedPattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
+const pattern = encodedPattern && decodeURIComponent(encodedPattern);
+const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
+const view = fragmentPaths[0];
+
+findAndRedirect(pattern, strict, view);
+
+/**
+ * Find the result and redirect to the result page.
+ * @param {string} pattern the pattern to search for
+ * @param {string} view the view of the find result (`"doc"` or `"src"` for now)
+ */
+async function findAndRedirect(pattern, strict, view) {
+  // if no pattern provided, directly redirect to the 404 page
+  if (!pattern) {
+    window.location.replace(`${SITE_ROOT}404.html`);
+  }
+  // search for result
+  try {
+    const dataCenter = await DeclarationDataCenter.init();
+    let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
+    // if no result found, redirect to the 404 page
+    if (!result) {
+      // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found.
+      window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
+    } else {
+      result.docLink = SITE_ROOT + result.docLink;
+      // success, redirect to doc or source page, or to the semantic rdf.
+      if (!view) {
+        window.location.replace(result.link);
+      } else if (view == "doc") {
+        window.location.replace(result.docLink);
+      } else if (view == "src") {
+        const [module, decl] = result.docLink.split("#", 2);
+        window.location.replace(`${module}?jump=src#${decl}`);
+      } else {
+        // fallback to doc page
+        window.location.replace(result.docLink);
+      }
+    }
+  } catch (e) {
+    document.write(`Cannot fetch data, please check your network connection.\n${e}`);
+  }
+}

static/how-about.js

@@ -0,0 +1,39 @@
+/**
+ * This module implements the `howabout` functionality in the 404 page.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+const HOW_ABOUT = document.querySelector("#howabout");
+
+// Show url of the missing page
+if (HOW_ABOUT) {
+  HOW_ABOUT.parentNode
+    .insertBefore(document.createElement("pre"), HOW_ABOUT)
+    .appendChild(document.createElement("code")).innerText =
+    window.location.href.replace(/[/]/g, "/\u200b");
+
+  // TODO: add how about functionality for similar page as well.
+  const pattern = window.location.hash.replace("#", "");
+
+  // try to search for similar declarations
+  if (pattern) {
+    HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
+    DeclarationDataCenter.init().then((dataCenter) => {
+      let results = dataCenter.search(pattern, false);
+      if (results.length > 0) {
+        HOW_ABOUT.innerText = "How about one of these instead:";
+        const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
+        for (const { name, docLink } of results) {
+          const li = ul.appendChild(document.createElement("li"));
+          const a = li.appendChild(document.createElement("a"));
+          a.href = docLink;
+          a.appendChild(document.createElement("code")).innerText = name;
+        }
+      } else {
+        HOW_ABOUT.innerText =
+          "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
+      }
+    });
+  }
+}

static/importedBy.js

@@ -0,0 +1,19 @@
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+fillImportedBy();
+
+async function fillImportedBy() {
+  if (typeof(MODULE_NAME) == "undefined") {
+    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 += `<li><a href="${SITE_ROOT}${moduleLink}">${module}</a></li>`
+  }
+  importedByList.innerHTML = innerHTML;
+}

static/instances.js

@@ -0,0 +1,36 @@
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+annotateInstances();
+annotateInstancesFor()
+
+async function annotateInstances() {
+  const dataCenter = await DeclarationDataCenter.init();
+  const instanceForLists = [...(document.querySelectorAll(".instances-list"))];
+
+  for (const instanceForList of instanceForLists) {
+    const className = instanceForList.id.slice("instances-list-".length);
+    const instances = dataCenter.instancesForClass(className);
+    var innerHTML = "";
+    for(var instance of instances) {
+      const instanceLink = dataCenter.declNameToLink(instance);
+      innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
+    }
+    instanceForList.innerHTML = innerHTML;
+  }
+}
+
+async function annotateInstancesFor() {
+  const dataCenter = await DeclarationDataCenter.init();
+  const instanceForLists = [...(document.querySelectorAll(".instances-for-list"))];
+
+  for (const instanceForList of instanceForLists) {
+    const typeName = instanceForList.id.slice("instances-for-list-".length);
+    const instances = dataCenter.instancesForType(typeName);
+    var innerHTML = "";
+    for(var instance of instances) {
+      const instanceLink = dataCenter.declNameToLink(instance);
+      innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
+    }
+    instanceForList.innerHTML = innerHTML;
+  }
+}

static/jump-src.js

@@ -0,0 +1,10 @@
+document.addEventListener("DOMContentLoaded", () => {
+    const hash = document.location.hash.substring(1);
+    const tgt = new URLSearchParams(document.location.search).get("jump");
+    if (tgt === "src" && hash) {
+      const target = document.getElementById(hash)
+        ?.querySelector(".gh_link a")
+        ?.getAttribute("href");
+      if (target) window.location.replace(target);
+    }
+})

static/mathjax-config.js

@@ -0,0 +1,41 @@
+/*
+ * This file is for configing MathJax behavior.
+ * See https://docs.mathjax.org/en/latest/web/configuration.html
+ * 
+ * This configuration is copied from old doc-gen3
+ * https://github.com/leanprover-community/doc-gen
+ */
+MathJax = {
+  tex: {
+    inlineMath: [["$", "$"]],
+    displayMath: [["$$", "$$"]],
+  },
+  options: {
+    skipHtmlTags: [
+      "script",
+      "noscript",
+      "style",
+      "textarea",
+      "pre",
+      "code",
+      "annotation",
+      "annotation-xml",
+      "decl",
+      "decl_meta",
+      "attributes",
+      "decl_args",
+      "decl_header",
+      "decl_name",
+      "decl_type",
+      "equation",
+      "equations",
+      "structure_field",
+      "structure_fields",
+      "constructor",
+      "constructors",
+      "instances",
+    ],
+    ignoreHtmlClass: "tex2jax_ignore",
+    processHtmlClass: "tex2jax_process",
+  },
+};

static/nav.js

@@ -0,0 +1,43 @@
+/**
+ * This module is used to implement persistent navbar expansion.
+ */
+
+// The variable to store the expansion information.
+let expanded = {};
+
+// Load expansion information from sessionStorage.
+for (const e of (sessionStorage.getItem("expanded") || "").split(",")) {
+  if (e !== "") {
+    expanded[e] = true;
+  }
+}
+
+/**
+ * Save expansion information to sessionStorage.
+ */
+function saveExpanded() {
+  sessionStorage.setItem(
+    "expanded",
+    Object.getOwnPropertyNames(expanded)
+      .filter((e) => expanded[e])
+      .join(",")
+  );
+}
+
+// save expansion information when user change the expansion.
+for (const elem of document.getElementsByClassName("nav_sect")) {
+  const id = elem.getAttribute("data-path");
+  if (!id) continue;
+  if (expanded[id]) {
+    elem.open = true;
+  }
+  elem.addEventListener("toggle", () => {
+    expanded[id] = elem.open;
+    saveExpanded();
+  });
+}
+
+// Scroll to center.
+for (const currentFileLink of document.getElementsByClassName("visible")) {
+  currentFileLink.scrollIntoView({ block: "center" });
+}

static/search.js

@@ -0,0 +1,164 @@
+/**
+ * This module is used to handle user's interaction with the search form.
+ */
+
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+// Search form and input in the upper right toolbar
+const SEARCH_FORM = document.querySelector("#search_form");
+const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
+
+// Search form on the /search.html_page.  These may be null.
+const SEARCH_PAGE_INPUT = document.querySelector("#search_page_query")
+const SEARCH_RESULTS = document.querySelector("#search_results")
+
+// Max results to show for autocomplete or /search.html page.
+const AC_MAX_RESULTS = 30
+const SEARCH_PAGE_MAX_RESULTS = undefined
+
+// Create an `div#autocomplete_results` to hold all autocomplete results.
+let ac_results = document.createElement("div");
+ac_results.id = "autocomplete_results";
+SEARCH_FORM.appendChild(ac_results);
+
+/**
+ * Attach `selected` class to the the selected autocomplete result.
+ */
+function handleSearchCursorUpDown(down) {
+  const sel = ac_results.querySelector(`.selected`);
+  if (sel) {
+    sel.classList.remove("selected");
+    const toSelect = down
+      ? sel.nextSibling 
+      : sel.previousSibling;
+    toSelect && toSelect.classList.add("selected");
+  } else {
+    const toSelect = down ? ac_results.firstChild : ac_results.lastChild;
+    toSelect && toSelect.classList.add("selected");
+  }
+}
+
+/**
+ * Perform search (when enter is pressed).
+ */
+function handleSearchEnter() {
+  const sel = ac_results.querySelector(`.selected .result_link a`) || document.querySelector(`#search_button`);
+  sel.click();
+}
+
+/**
+ * Allow user to navigate autocomplete results with up/down arrow keys, and choose with enter.
+ */
+SEARCH_INPUT.addEventListener("keydown", (ev) => {
+  switch (ev.key) {
+    case "Down":
+    case "ArrowDown":
+      ev.preventDefault();
+      handleSearchCursorUpDown(true);
+      break;
+    case "Up":
+    case "ArrowUp":
+      ev.preventDefault();
+      handleSearchCursorUpDown(false);
+      break;
+    case "Enter":
+      ev.preventDefault();
+      handleSearchEnter();
+      break;
+  }
+});
+
+/**
+ * Remove all children of a DOM node.
+ */
+function removeAllChildren(node) {
+  while (node.firstChild) {
+    node.removeChild(node.lastChild);
+  }
+}
+
+/**
+ * Handle user input and perform search.
+ */
+function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
+  const text = ev.target.value;
+
+  // If no input clear all.
+  if (!text) {
+    sr.removeAttribute("state");
+    removeAllChildren(sr);
+    return;
+  }
+
+  // searching
+  sr.setAttribute("state", "loading");
+
+  if (dataCenter) {
+    var allowedKinds;
+    if (!autocomplete) {
+      allowedKinds = new Set();
+      document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
+        {
+          if (checkbox.checked) {
+            allowedKinds.add(checkbox.value);
+          }
+        } 
+      );
+    }
+    const result = dataCenter.search(text, false, allowedKinds, maxResults);
+
+    // in case user has updated the input.
+    if (ev.target.value != text) return;
+  
+    // update autocomplete results
+    removeAllChildren(sr);
+    for (const { name, kind, docLink } of result) {
+      const row = sr.appendChild(document.createElement("div"));
+      row.classList.add("search_result")
+      const linkdiv = row.appendChild(document.createElement("div"))
+      linkdiv.classList.add("result_link")
+      const link = linkdiv.appendChild(document.createElement("a"));
+      link.innerText = name;
+      link.title = name;
+      link.href = SITE_ROOT + docLink;
+    }
+  }
+  // handle error
+  else {
+    removeAllChildren(sr);
+    const d = sr.appendChild(document.createElement("a"));
+    d.innerText = `Cannot fetch data, please check your network connection.\n${err}`;
+  }
+  sr.setAttribute("state", "done");
+}
+
+// https://www.joshwcomeau.com/snippets/javascript/debounce/
+const debounce = (callback, wait) => {
+  let timeoutId = null;
+  return (...args) => {
+    window.clearTimeout(timeoutId);
+    timeoutId = window.setTimeout(() => {
+      callback.apply(null, args);
+    }, wait);
+  };
+}
+
+DeclarationDataCenter.init()
+  .then((dataCenter) => {
+    // Search autocompletion.
+    SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true), 300));
+    if(SEARCH_PAGE_INPUT) {
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false))
+      document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
+        checkbox.addEventListener("input", ev => SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")))
+      );
+      SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
+    };
+    SEARCH_INPUT.dispatchEvent(new Event("input"))
+  })
+  .catch(e => {
+    SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS, true), 300));
+    if(SEARCH_PAGE_INPUT) {
+      SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false));
+    }
+  });

static/site-root.js

@@ -0,0 +1,4 @@
+/**
+ * Get the site root, {siteRoot} is to be replaced by doc-gen4.
+ */
+export const SITE_ROOT = "{siteRoot}";

static/style.css

@@ -0,0 +1,815 @@
+@import url('https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro&family=Source+Code+Pro:wght@600&display=swap');
+
+* {
+    box-sizing: border-box;
+}
+
+body {
+    font-family: 'Open Sans', sans-serif;
+    color: var(--text-color);
+    background: var(--body-bg);
+}
+
+a {
+   color: var(--link-color);
+}
+
+a.pdf {
+   color: var(--link-pdf-color);
+}
+
+h1, h2, h3, h4, h5, h6 {
+    font-family: 'Merriweather', serif;
+}
+
+body { line-height: 1.5; }
+nav { line-height: normal; }
+
+:root {
+    --header-height: 3em;
+    --fragment-offset: calc(var(--header-height) + 1em);
+    --content-width: 55vw;
+
+    --header-bg: #f8f8f8;
+    --body-bg: white;
+    --code-bg: #f3f3f3;
+    --text-color: black;
+    --link-color: hsl(210, 100%, 30%);
+    --link-pdf-color: hsl(272, 61%, 34%);
+
+    --implicit-arg-text-color: var(--text-color);
+
+    --def-color: #92dce5;
+    --def-color-hsl-angle: 187;
+    --theorem-color: #8fe388;
+    --theorem-color-hsl-angle: 115;
+    --axiom-and-constant-color: #f44708;
+    --axiom-and-constant-color-hsl-angle: 16;
+    --structure-and-inductive-color: #f0a202;
+    --structure-and-inductive-color-hsl-angle: 40;
+    --starting-percentage: 100;
+
+    --hamburger-bg-color: #eee;
+    --hamburger-active-color: white;
+    --hamburger-border-color: #ccc;
+
+    --tags-border-color: #555;
+
+    --fragment-offset: calc(var(--header-height) + 1em);
+    --content-width: 55vw;
+}
+/* automatic dark theme if no javascript */
+@media (prefers-color-scheme: dark) {
+    :root {
+        --header-bg: #111010;
+        --body-bg: #171717;
+        --code-bg: #363333;
+        --text-color: #eee;
+        --link-color: #58a6ff;
+        --link-pdf-color: #9d58fd;
+
+        --implicit-arg-text-color: var(--text-color);
+
+        --def-color: #1F497F;
+        --def-color-hsl-angle: 214;
+        --theorem-color: #134E2D;
+        --theorem-color-hsl-angle: 146;
+        --axiom-and-constant-color: #6B1B1A;
+        --axiom-and-constant-color-hsl-angle: 1;
+        --structure-and-inductive-color: #73461C;
+        --structure-and-inductive-color-hsl-angle: 29;
+        --starting-percentage: 30;
+
+        --hamburger-bg-color: #2d2c2c;
+        --hamburger-active-color: black;
+        --hamburger-border-color: #717171;
+
+        --tags-border-color: #AAA;
+    }
+}
+
+[data-theme="light"] {
+    color-scheme: light;
+
+    --header-height: 3em;
+    --fragment-offset: calc(var(--header-height) + 1em);
+    --content-width: 55vw;
+
+    --header-bg: #f8f8f8;
+    --body-bg: white;
+    --code-bg: #f3f3f3;
+    --text-color: black;
+    --link-color: hsl(210, 100%, 30%);
+    --link-pdf-color: hsl(272, 61%, 34%);
+
+    --implicit-arg-text-color: var(--text-color);
+
+    --def-color: #92dce5;
+    --def-color-hsl-angle: 187;
+    --theorem-color: #8fe388;
+    --theorem-color-hsl-angle: 115;
+    --axiom-and-constant-color: #f44708;
+    --axiom-and-constant-color-hsl-angle: 16;
+    --structure-and-inductive-color: #f0a202;
+    --structure-and-inductive-color-hsl-angle: 40;
+    --starting-percentage: 100;
+
+    --hamburger-bg-color: #eee;
+    --hamburger-active-color: white;
+    --hamburger-border-color: #ccc;
+
+    --tags-border-color: #555;
+
+    --fragment-offset: calc(var(--header-height) + 1em);
+    --content-width: 55vw;
+}
+
+[data-theme="dark"] {
+    color-scheme: dark;
+
+    --header-bg: #111010;
+    --body-bg: #171717;
+    --code-bg: #363333;
+    --text-color: #eee;
+    --link-color: #58a6ff;
+    --link-pdf-color: #9d58fd;
+
+    --implicit-arg-text-color: var(--text-color);
+
+    --def-color: #1F497F;
+    --def-color-hsl-angle: 214;
+    --theorem-color: #134E2D;
+    --theorem-color-hsl-angle: 146;
+    --axiom-and-constant-color: #6B1B1A;
+    --axiom-and-constant-color-hsl-angle: 1;
+    --structure-and-inductive-color: #73461C;
+    --structure-and-inductive-color-hsl-angle: 29;
+    --starting-percentage: 30;
+
+    --hamburger-bg-color: #2d2c2c;
+    --hamburger-active-color: black;
+    --hamburger-border-color: #717171;
+
+    --tags-border-color: #AAA;
+}
+
+@supports (width: min(10px, 5vw)) {
+    :root {
+        --content-width: clamp(20em, 55vw, 60em);
+    }
+}
+
+#nav_toggle {
+    display: none;
+}
+label[for="nav_toggle"] {
+    display: none;
+}
+
+header {
+    height: var(--header-height);
+    float: left;
+    position: fixed;
+    width: 100vw;
+    max-width: 100%;
+    left: 0;
+    right: 0;
+    top: 0;
+    --header-side-padding: 2em;
+    padding: 0 var(--header-side-padding);
+    background: var(--header-bg);
+    z-index: 1;
+    display: flex;
+    align-items: center;
+    justify-content: space-between;
+}
+@supports (width: min(10px, 5vw)) {
+    header {
+        --header-side-padding: calc(max(2em, (100vw - var(--content-width) - 30em) / 2));
+    }
+}
+@media screen and (max-width: 1000px) {
+    :root {
+        --content-width: 100vw;
+    }
+
+    .internal_nav {
+        display: none;
+    }
+
+    body .nav {
+        width: 100vw;
+        max-width: 100vw;
+        margin-left: 1em;
+        z-index: 1;
+    }
+
+    body main {
+        width: unset;
+        max-width: unset;
+        margin-left: unset;
+        margin-right: unset;
+    }
+    body .decl > div {
+        overflow-x: unset;
+    }
+
+    #nav_toggle:not(:checked) ~ .nav {
+        display: none;
+    }
+    #nav_toggle:checked ~ main {
+        visibility: hidden;
+    }
+
+    label[for="nav_toggle"]::before {
+        content: '≡';
+    }
+    label[for="nav_toggle"] {
+        display: inline-block;
+        margin-right: 1em;
+        border: 1px solid var(--hamburger-border-color);
+        padding: 0.5ex 1ex;
+        cursor: pointer;
+        background: var(--hamburger-bg-color);
+    }
+    #nav_toggle:checked ~ * label[for="nav_toggle"] {
+        background: var(--hamburger-active-color);
+    }
+
+    body header h1 {
+        font-size: 100%;
+    }
+
+    header {
+        --header-side-padding: 1ex;
+    }
+}
+@media screen and (max-width: 700px) {
+    header h1 span { display: none; }
+    :root { --header-side-padding: 1ex; }
+    #search_form button { display: none; }
+    #search_form input { width: 100%; }
+    header #autocomplete_results {
+        left: 1ex;
+        right: 1ex;
+        width: inherit;
+    }
+    body header > * { margin: 0; }
+}
+
+header > * {
+    display: inline-block;
+    padding: 0;
+    margin: 0 1em;
+    vertical-align: middle;
+}
+
+header h1 {
+    font-weight: normal;
+    font-size: 160%;
+}
+
+header header_filename {
+    font-size: 150%;
+}
+@media (max-width: 80em) {
+    .header .header_filename {
+        display: none;
+    }
+}
+
+/* inserted by nav.js */
+#autocomplete_results {
+    position: absolute;
+    top: var(--header-height);
+    right: calc(var(--header-side-padding));
+    width: calc(20em + 4em);
+    z-index: 1;
+    background: var(--header-bg);
+    border: 1px solid #aaa;
+    border-top: none;
+    overflow-x: hidden;
+    overflow-y: auto;
+    max-height: calc(100vh - var(--header-height));
+}
+
+#autocomplete_results:empty {
+    display: none;
+}
+
+#autocomplete_results[state="loading"]:empty {
+    display: block;
+    cursor: progress;
+}
+#autocomplete_results[state="loading"]:empty::before {
+    display: block;
+    content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
+    padding: 1ex;
+    animation: marquee 10s linear infinite;
+}
+@keyframes marquee {
+    0% { transform: translate(100%, 0); }
+    100% { transform: translate(-100%, 0); }
+}
+
+#autocomplete_results[state="done"]:empty {
+    display: block;
+    text-align: center;
+    padding: 1ex;
+}
+#autocomplete_results[state="done"]:empty::before {
+    content: '(no results)';
+    font-style: italic;
+}
+
+#autocomplete_results a {
+    display: block;
+    color: inherit;
+    padding: 1ex;
+    border-left: 0.5ex solid transparent;
+    padding-left: 0.5ex;
+    cursor: pointer;
+}
+
+#autocomplete_results .selected .result_link a {
+    background: var(--body-bg);
+    border-color: var(--structure-and-inductive-color);
+}
+
+
+#search_results {
+    display: table;
+    width: 100%;
+}
+#search_results[state="done"]:empty::before {
+    content: '(no results)';
+    font-style: italic;
+}
+
+#search_results .result_link, #search_results .result_doc {
+    border-bottom: 1px solid rgba(0, 0, 0, 0.8);
+}
+
+.search_result {
+    display: table-row;
+}
+
+.result_link, .result_doc {
+    display: table-cell;
+    overflow: hidden;
+    word-break: break-word;
+}
+
+main, nav {
+    margin-top: calc(var(--header-height) + 1em);
+}
+
+/* extra space for scrolling things to the top */
+main {
+    margin-bottom: 90vh;
+}
+
+main {
+    max-width: var(--content-width);
+    /* center it: */
+    margin-left: auto;
+    margin-right: auto;
+}
+
+nav {
+    float: left;
+    height: calc(100vh - var(--header-height) - 1em);
+    position: fixed;
+    top: 0;
+    overflow: auto;
+    scrollbar-width: thin;
+    scrollbar-color: transparent transparent;
+}
+
+nav:hover {
+    scrollbar-color: gray transparent;
+}
+
+nav {
+    --column-available-space: calc((100vw - var(--content-width) - 5em)/2);
+    --column-width: calc(var(--column-available-space) - 1ex);
+    --dist-to-edge: 1ex;
+    width: var(--content-width);
+    max-width: var(--column-width);
+}
+@supports (width: min(10px, 5vw)) {
+    .nav { --desired-column-width: 20em; }
+    .internal_nav { --desired-column-width: 30em; }
+    nav {
+        --column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2));
+        --column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width)));
+        --dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width)));
+    }
+}
+
+.nav { left: var(--dist-to-edge); }
+.internal_nav { right: var(--dist-to-edge); }
+
+.internal_nav .nav_link, .taclink {
+    /* indent everything but first line by 2ex */
+    text-indent: -2ex; padding-left: 2ex;
+}
+
+.navframe {
+    height: 100%;
+    width: 100%;
+}
+
+.navframe .nav {
+    position: absolute;
+    left: 0;
+    margin-left: 0;
+}
+
+.internal_nav .imports {
+    margin-bottom: 1rem;
+}
+
+.tagfilter-div {
+    margin-bottom: 1em;
+}
+.tagfilter-div > summary {
+    margin-bottom: 1ex;
+}
+
+/* top-level modules in left navbar */
+.nav .module_list > details {
+    margin-top: 1ex;
+}
+
+.nav details > * {
+    padding-left: 2ex;
+}
+
+.nav summary {
+    cursor: pointer;
+    padding-left: 0;
+}
+
+.nav summary::marker {
+    font-size: 85%;
+}
+
+.nav .nav_file {
+    display: inline-block;
+}
+
+.nav h3 {
+    margin-block-end: 4px;
+}
+
+/* People use way too long declaration names. */
+.internal_nav, .decl_name {
+    overflow-wrap: break-word;
+}
+
+/* Add a linebreak after a declaration name. */
+.decl_name::after {
+    content: "\A";
+    white-space: pre;
+}
+
+.nav_link {
+    overflow-wrap: break-word;
+}
+
+.navframe {
+    --header-height: 0;
+}
+
+#settings {
+    margin-top: 5em;
+}
+#settings h3 {
+    font-size: inherit;
+}
+
+#color-theme-switcher {
+    display: flex;
+    justify-content: space-between;
+    padding: 0 2ex;
+    flex-flow: row wrap;
+}
+
+/* custom radio buttons for dark/light switch */
+#color-theme-switcher input {
+    -webkit-appearance: none;
+    -moz-appearance: none;
+    appearance: none;
+    display: inline-block;
+    box-sizing: content-box;
+    height: 1em;
+    width: 1em;
+    background-clip: content-box;
+    padding: 2px;
+    border: 2px solid transparent;
+    margin-bottom: -4px;
+    border-radius: 50%;
+}
+#color-theme-dark { background-color: #444; }
+#color-theme-light { background-color: #ccc; }
+#color-theme-system {
+    background-image: linear-gradient(60deg, #444, #444 50%, #CCC 50%, #CCC);
+}
+#color-theme-switcher input:checked {
+    border-color: var(--text-color);
+}
+
+.decl > div, .mod_doc {
+    padding-left: 8px;
+    padding-right: 8px;
+}
+
+.decl {
+    margin-top: 20px;
+    margin-bottom: 20px;
+}
+
+.decl > div {
+    /* sometimes declarations arguments are way too long
+       and would continue into the right column,
+       so put a scroll bar there: */
+    overflow-x: auto;
+}
+
+/* Make `#id` links appear below header. */
+.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] {
+    scroll-margin-top: var(--fragment-offset);
+}
+/* don't need as much vertical space for these
+inline elements */
+a[id], li[id] {
+    scroll-margin-top: var(--header-height);
+}
+
+/* HACK: Safari doesn't support scroll-margin-top for
+fragment links (yet?)
+https://caniuse.com/mdn-css_properties_scroll-margin-top
+https://bugs.webkit.org/show_bug.cgi?id=189265
+*/
+@supports not (scroll-margin-top: var(--fragment-offset)) {
+    .decl::before, h1[id]::before, h2[id]::before, h3[id]::before,
+    h4[id]::before, h5[id]::before, h6[id]::before,
+    a[id]::before, li[id]::before {
+        content: "";
+        display: block;
+        height:      var(--fragment-offset);
+        margin-top:  calc(-1 * var(--fragment-offset));
+        box-sizing: inherit;
+        visibility: hidden;
+        width: 1px;
+    }
+}
+
+
+/* hide # after markdown headings except on hover */
+.markdown-heading:not(:hover) > .hover-link {
+    visibility: hidden;
+}
+
+main h2, main h3, main h4, main h5, main h6 {
+    margin-top: 2rem;
+}
+.decl + .mod_doc > h2,
+        .decl + .mod_doc > h3,
+        .decl + .mod_doc > h4,
+        .decl + .mod_doc > h5,
+        .decl + .mod_doc > h6 {
+    margin-top: 4rem;
+}
+
+.def, .instance {
+    border-left: 10px solid var(--text-color);
+    border-top: 2px solid var(--text-color);
+}
+
+.theorem {
+    border-left: 10px solid var(--theorem-color);
+    border-top: 2px solid var(--theorem-color);
+}
+
+.axiom, .opaque {
+    border-left: 10px solid var(--axiom-and-constant-color);
+    border-top: 2px solid var(--axiom-and-constant-color);
+}
+
+.structure, .inductive, .class {
+    border-left: 10px solid var(--structure-and-inductive-color);
+    border-top: 2px solid var(--structure-and-inductive-color);
+}
+
+.fn {
+    display: inline-block;
+    /* border: 1px dashed red; */
+    text-indent: -1ex;
+    padding-left: 1ex;
+    white-space: pre-wrap;
+    vertical-align: top;
+}
+
+.fn { --fn: 1; }
+.fn .fn { --fn: 2; }
+.fn .fn .fn { --fn: 3; }
+.fn .fn .fn .fn { --fn: 4; }
+.fn .fn .fn .fn .fn { --fn: 5; }
+.fn .fn .fn .fn .fn .fn { --fn: 6; }
+.fn .fn .fn .fn .fn .fn .fn { --fn: 7; }
+.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; }
+.fn {
+    transition: background-color 100ms ease-in-out;
+}
+
+.def .fn:hover, .instance .fn:hover {
+    background-color: hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*var(--fn)));
+    box-shadow: 0 0 0 1px hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
+    border-radius: 5px;
+}
+.theorem .fn:hover {
+    background-color: hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*var(--fn)));
+    box-shadow: 0 0 0 1px hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
+    border-radius: 5px;
+}
+.axiom .fn:hover, .opaque .fn:hover {
+    background-color: hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*var(--fn)));
+    box-shadow: 0 0 0 1px hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
+    border-radius: 5px;
+}
+.structure .fn:hover, .inductive .fn:hover, .class .fn:hover {
+    background-color: hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*var(--fn)));
+    box-shadow: 0 0 0 1px hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
+    border-radius: 5px;
+}
+
+.decl_args, .decl_type .decl_parent {
+    font-weight: normal;
+}
+
+.implicits, .impl_arg {
+    color: var(--text-color);
+    white-space: normal;
+}
+
+.decl_kind, .decl_name, .decl_extends {
+    font-weight: bold;
+}
+
+/* break long declaration names at periods where possible */
+.break_within {
+    word-break: break-all;
+}
+
+.break_within .name {
+    word-break: normal;
+}
+
+.decl_header {
+    /* indent everything but first line twice as much as decl_type */
+    text-indent: -8ex; padding-left: 8ex;
+}
+
+.decl_type {
+    margin-top: 2px;
+    margin-left: 4ex; /* extra indentation */
+}
+
+.imports li, code, .decl_header, .attributes, .structure_field_info,
+        .constructor, .instances li, .equation, .result_link, .structure_ext_ctor {
+    font-family: 'Source Code Pro', monospace;
+}
+
+pre {
+    white-space: break-spaces;
+}
+
+code, pre { background: var(--code-bg); }
+code, pre { border-radius: 5px; }
+code { padding: 1px 3px; }
+pre { padding: 1ex; }
+pre code { padding: 0 0; }
+
+#howabout code { background: inherit; }
+#howabout li { margin-bottom: 0.5ex; }
+
+.structure_fields, .constructors {
+    display: block;
+    padding-inline-start: 0;
+    margin-top: 1ex;
+    text-indent: -2ex; padding-left: 2ex;
+}
+
+.structure_field {
+    display: block;
+    margin-left: 2ex;
+}
+
+.inductive_ctor_doc  {
+    text-indent: 2ex;
+    font-family: 'Open Sans', sans-serif;
+}
+
+.structure_field_doc {
+    text-indent: 0;
+    font-family: 'Open Sans', sans-serif;
+}
+
+.structure_ext_fields {
+    display: block;
+    padding-inline-start: 0;
+    margin-top: 1ex;
+    text-indent: -2ex; padding-left: 2ex;
+}
+
+.structure_ext_fields .structure_field {
+    margin-left: -1ex !important;
+}
+
+.structure_ext_ctor {
+    display: block;
+    text-indent: -3ex;
+}
+
+.constructor {
+    display: block;
+}
+.constructor:before {
+    content: '| ';
+    color: gray;
+}
+
+/** Don't show underline on types, to prevent the ≤ vs < confusion. **/
+a:link, a:visited, a:active {
+    color:var(--link-color);
+    text-decoration: none;
+}
+
+a.pdf:link, a.pdf:visited, a.pdf:active {
+    color:var(--link-pdf-color);
+}
+
+/** Show it on hover though. **/
+a:hover {
+    text-decoration: underline;
+}
+
+.impl_arg {
+    font-style: italic;
+    transition: opacity 300ms ease-in;
+}
+
+.decl_header:not(:hover) .impl_arg {
+    opacity: 30%;
+    transition: opacity 1000ms ease-out;
+}
+
+.gh_link {
+    float: right;
+    margin-left: 10px;
+}
+
+.ink_link {
+    float: right;
+    margin-left: 20px;
+}
+
+
+.docfile h2, .note h2 {
+    margin-block-start: 3px;
+    margin-block-end: 0px;
+}
+
+.docfile h2 a {
+    color: var(--text-color);
+}
+
+.tags {
+    margin-bottom: 1ex;
+}
+
+.tags ul {
+    display: inline;
+    padding: 0;
+}
+
+.tags li {
+    border: 1px solid var(--tags-border-color);
+    border-radius: 4px;
+    list-style-type: none;
+    padding: 1px 3px;
+    margin-left: 1ex;
+    display: inline-block;
+}
+
+/* used by nav.js */
+.hide { display: none; }
+
+.tactic, .note {
+    border-top: 3px solid #0479c7;
+    padding-top: 2em;
+    margin-top: 2em;
+    margin-bottom: 2em;
+}

static/tactic.js

@@ -0,0 +1,61 @@
+// TODO: The tactic part seem to be unimplemented now.
+
+function filterSelectionClass(tagNames, classname) {
+  if (tagNames.length == 0) {
+    for (const elem of document.getElementsByClassName(classname)) {
+      elem.classList.remove("hide");
+    }
+  } else {
+    // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
+    for (const elem of document.getElementsByClassName(classname)) {
+      elem.classList.add("hide");
+      for (const tagName of tagNames) {
+        if (elem.classList.contains(tagName)) {
+          elem.classList.remove("hide");
+        }
+      }
+    }
+  }
+}
+
+function filterSelection(c) {
+  filterSelectionClass(c, "tactic");
+  filterSelectionClass(c, "taclink");
+}
+
+var filterBoxes = document.getElementsByClassName("tagfilter");
+
+function updateDisplay() {
+  filterSelection(getSelectValues());
+}
+
+function getSelectValues() {
+  var result = [];
+
+  for (const opt of filterBoxes) {
+    if (opt.checked) {
+      result.push(opt.value);
+    }
+  }
+  return result;
+}
+
+function setSelectVal(val) {
+  for (const opt of filterBoxes) {
+    opt.checked = val;
+  }
+}
+
+updateDisplay();
+
+for (const opt of filterBoxes) {
+  opt.addEventListener("change", updateDisplay);
+}
+
+const tse = document.getElementById("tagfilter-selectall");
+if (tse != null) {
+  tse.addEventListener("change", function () {
+    setSelectVal(this.checked);
+    updateDisplay();
+  });
+}