detailed declaration pages

Author: RemyDegenne

LeanExposition/Collect.lean

@@ -123,6 +123,7 @@ structure DeclInfo where
   deps : Array Name
   typeDeps : Array Name := #[]
   usedBy : Array Name := #[]
+  transDeps : Array Name := #[]
   docstringBlock? : Option (Block Manual) := none
 deriving Repr
 
@@ -338,9 +339,10 @@ def codeListParagraph (label : String) (items : Array String) : Option (Block Ma
       joinInlines entries #[.text " · "]
 
 /-- Helper for mkLinkParagraph. -/
-def mkLinkParagraph (sourceUrl? issueUrl? : Option String) : Option (Block Manual) :=
+def mkLinkParagraph (sourceUrl? issueUrl? detailsUrl? : Option String) : Option (Block Manual) :=
   let items :=
-    ([sourceUrl?.map fun url => .link #[.text "Source"] url,
+    ([detailsUrl?.map fun url => .link #[.text "Details"] url,
+      sourceUrl?.map fun url => .link #[.text "Source"] url,
       issueUrl?.map fun url => .link #[.text "Open Issue"] url].filterMap id)
   if items.isEmpty then
     none
@@ -921,6 +923,16 @@ def declHrefMap (decls : Array DeclInfo) : Std.HashMap Name String :=
     (fun acc decl => acc.insert decl.name (pathForPart decl.groupKey decl.modulePath decl.name))
     {}
 
+/-- Computes path ForDeclPage. -/
+def pathForDeclPage (groupKey modulePath : String) (declName : Name) : String :=
+  s!"{groupHrefOf groupKey}{moduleHrefOf modulePath}decl-{anchorIdOf declName}/"
+
+/-- Maps each declaration name to its dedicated detail page. -/
+def declPageHrefMap (decls : Array DeclInfo) : Std.HashMap Name String :=
+  decls.foldl
+    (fun acc decl => acc.insert decl.name (pathForDeclPage decl.groupKey decl.modulePath decl.name))
+    {}
+
 /-- Helper for runCoreIO. -/
 def runCoreIO {α : Type} (env : Environment) (x : CoreM α) : IO α := do
   x.toIO'
@@ -1050,6 +1062,28 @@ def attachReverseDeps (decls : Array DeclInfo) : Array DeclInfo :=
     {}
   decls.map fun decl => { decl with usedBy := (rev.getD decl.name #[]).qsort Name.lt }
 
+/-- Computes the set of declarations reachable from `start` via `depsMap`. -/
+partial def transitiveClosure (depsMap : Std.HashMap Name (Array Name)) (start : Array Name) :
+    Std.HashSet Name :=
+  go {} start.toList
+where
+  go (visited : Std.HashSet Name) : List Name → Std.HashSet Name
+    | [] => visited
+    | n :: rest =>
+      if visited.contains n then
+        go visited rest
+      else
+        go (visited.insert n) ((depsMap.getD n #[]).toList ++ rest)
+
+/-- Adds the transitive closure of `deps` (all declarations reachable, recursively) to each
+declaration as `transDeps`. -/
+def attachTransitiveDeps (decls : Array DeclInfo) : Array DeclInfo :=
+  let depsMap : Std.HashMap Name (Array Name) :=
+    decls.foldl (fun acc decl => acc.insert decl.name decl.deps) {}
+  decls.map fun decl =>
+    let closure := transitiveClosure depsMap decl.deps
+    { decl with transDeps := (closure.toArray.filter (· != decl.name)).qsort Name.lt }
+
 /-- Marks declarations that transitively depend on any `sorry`. -/
 def attachDependsOnSorry (decls : Array DeclInfo) : Array DeclInfo :=
   Id.run do

LeanExposition/Site.lean

@@ -200,7 +200,7 @@ private def renderConfig (hasTfb : Bool) : RenderConfig :=
     emitTeX := false
     emitHtmlSingle := .no
     emitHtmlMulti := .immediately
-    htmlDepth := 2
+    htmlDepth := 3
     rootTocDepth := some 1
     sectionTocDepth := some 1
     extraCss := [customCss]
@@ -318,10 +318,11 @@ private def mkTrustedBaseIndexBlocks (groups : Array GroupInfo) : Array (Block M
 
 /-- Renders one declaration card with docs, statement, links, and dependencies. -/
 private def mkDeclBlock (decl : DeclInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) : Block Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) : Block Manual :=
   Id.run do
     let issueUrl := issueUrlOf repoUrl? decl.name decl.moduleName decl.source? decl.hasSorry
     let sourceUrl := sourceUrlOf repoUrl? decl.source?
+    let detailsUrl := declPageHrefs.get? decl.name
     let mkLinks (deps : Array Name) := deps.filterMap fun dep =>
       declHrefs.get? dep |>.map fun href => { label := dep.getString!, href? := some href }
     let typeDepLinks := mkLinks decl.typeDeps
@@ -342,7 +343,7 @@ private def mkDeclBlock (decl : DeclInfo) (repoUrl? : Option String)
       blocks := blocks.push <| .other (Block.details { summary := s!"Body uses ({proofDepLinks.size})" }) #[block]
     if let some block := depListBlock usedByLinks then
       blocks := blocks.push <| .other (Block.details { summary := s!"Used by ({usedByLinks.size})" }) #[block]
-    if let some block := mkLinkParagraph sourceUrl issueUrl then
+    if let some block := mkLinkParagraph sourceUrl issueUrl detailsUrl then
       blocks := blocks.push block
     if let some proof := decl.proofText? then
       blocks := blocks.push <| .other (Block.details { summary := "Proof" }) #[.code proof]
@@ -358,9 +359,44 @@ private def mkDeclBlock (decl : DeclInfo) (repoUrl? : Option String)
     }
     .other (Block.declCard cardData) blocks
 
+/-- Builds a dedicated detail page for one declaration, listing its direct and transitive
+dependencies. -/
+private def mkDeclPart (decl : DeclInfo) (declPageHrefs : Std.HashMap Name String) : Part Manual :=
+  Id.run do
+  let mkLinks (deps : Array Name) := deps.filterMap fun dep =>
+    declPageHrefs.get? dep |>.map fun href => { label := dep.getString!, href? := some href }
+  let typeDepLinks := mkLinks decl.typeDeps
+  let proofDepLinks := mkLinks <| decl.deps.filter (!decl.typeDeps.contains ·)
+  let usedByLinks := mkLinks decl.usedBy
+  let transDepLinks := mkLinks decl.transDeps
+  let mut blocks : Array (Block Manual) := #[]
+  if let some docstringBlock := decl.docstringBlock? then
+    blocks := blocks.push docstringBlock
+  blocks := blocks.push (.para #[.bold #[.text "Code"]])
+  blocks := blocks.push (.code decl.displaySignature)
+  if let some block := depListBlock typeDepLinks then
+    blocks := blocks.push <| .other (Block.details { summary := s!"Type uses ({typeDepLinks.size})" }) #[block]
+  if let some block := depListBlock proofDepLinks then
+    blocks := blocks.push <| .other (Block.details { summary := s!"Body uses ({proofDepLinks.size})" }) #[block]
+  if let some block := depListBlock usedByLinks then
+    blocks := blocks.push <| .other (Block.details { summary := s!"Used by ({usedByLinks.size})" }) #[block]
+  if let some block := depListBlock transDepLinks then
+    blocks := blocks.push <| .other (Block.details { summary := s!"All dependencies, transitively ({transDepLinks.size})" }) #[block]
+  return {
+    title := #[.code decl.name.toString]
+    titleString := decl.name.toString
+    metadata := some {
+      file := some s!"decl-{anchorIdOf decl.name}"
+      shortTitle := some decl.name.getString!
+      number := false
+    }
+    content := blocks
+    subParts := #[]
+  }
+
 /-- Builds a module page from its declarations. -/
 private def mkModulePart (moduleInfo : ModuleInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) : Part Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) : Part Manual :=
   {
     title := #[.text moduleInfo.path]
     titleString := moduleInfo.path
@@ -375,13 +411,13 @@ private def mkModulePart (moduleInfo : ModuleInfo) (repoUrl? : Option String)
         .code moduleInfo.name.toString,
         .text s!" contains {moduleInfo.decls.size} exposed declarations."
       ]
-    ] ++ moduleInfo.decls.map (fun decl => mkDeclBlock decl repoUrl? declHrefs)
-    subParts := #[]
+    ] ++ moduleInfo.decls.map (fun decl => mkDeclBlock decl repoUrl? declHrefs declPageHrefs)
+    subParts := moduleInfo.decls.map (fun decl => mkDeclPart decl declPageHrefs)
   }
 
 /-- Builds a trusted-base module page from declarations in that module. -/
 private def mkTrustedBaseModulePart (moduleInfo : ModuleInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) : Part Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) : Part Manual :=
   {
     title := #[.text moduleInfo.path]
     titleString := moduleInfo.path
@@ -396,13 +432,13 @@ private def mkTrustedBaseModulePart (moduleInfo : ModuleInfo) (repoUrl? : Option
         .code moduleInfo.name.toString,
         .text s!" contributes {moduleInfo.decls.size} declarations to the trusted formalization base."
       ]
-    ] ++ moduleInfo.decls.map (fun decl => mkDeclBlock decl repoUrl? declHrefs)
+    ] ++ moduleInfo.decls.map (fun decl => mkDeclBlock decl repoUrl? declHrefs declPageHrefs)
     subParts := #[]
   }
 
 /-- Builds a chapter page that contains regular module pages. -/
 private def mkGroupPart (group : GroupInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) : Part Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) : Part Manual :=
   let title := humanizeWord group.key
   {
     title := #[.text title]
@@ -415,12 +451,12 @@ private def mkGroupPart (group : GroupInfo) (repoUrl? : Option String)
     content := #[
       .para #[.text s!"Modules in the {title} slice are grouped from the first path component after the project root."]
     ]
-    subParts := group.modules.map fun moduleInfo => mkModulePart moduleInfo repoUrl? declHrefs
+    subParts := group.modules.map fun moduleInfo => mkModulePart moduleInfo repoUrl? declHrefs declPageHrefs
   }
 
 /-- Builds a chapter page for the trusted-base view. -/
 private def mkTrustedBaseGroupPart (group : GroupInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) : Part Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) : Part Manual :=
   let title := humanizeWord group.key
   {
     title := #[.text title]
@@ -433,12 +469,12 @@ private def mkTrustedBaseGroupPart (group : GroupInfo) (repoUrl? : Option String
     content := #[
       .para #[.text s!"Modules in the {title} slice that contribute declarations to the trusted formalization base."]
     ]
-    subParts := group.modules.map fun moduleInfo => mkTrustedBaseModulePart moduleInfo repoUrl? declHrefs
+    subParts := group.modules.map fun moduleInfo => mkTrustedBaseModulePart moduleInfo repoUrl? declHrefs declPageHrefs
   }
 
 /-- Builds the top-level trusted-base section and its chapter subpages. -/
 private def mkTrustedBasePart (groups : Array GroupInfo) (repoUrl? : Option String)
-    (declHrefs : Std.HashMap Name String) (targetBlocks : Array (Block Manual)) : Part Manual :=
+    (declHrefs declPageHrefs : Std.HashMap Name String) (targetBlocks : Array (Block Manual)) : Part Manual :=
   let declCount := countDecls groups
   let moduleCount := groups.foldl (fun n group => n + group.modules.size) 0
   let intro :=
@@ -462,7 +498,7 @@ private def mkTrustedBasePart (groups : Array GroupInfo) (repoUrl? : Option Stri
       ++ intro
       ++ mkTrustedBaseIndexBlocks groups
       ++ mkDashboardBlocks groups
-    subParts := groups.map fun group => mkTrustedBaseGroupPart group repoUrl? declHrefs
+    subParts := groups.map fun group => mkTrustedBaseGroupPart group repoUrl? declHrefs declPageHrefs
   }
 
 /-- Builds the interactive dependency graph page and graph payload. -/
@@ -500,7 +536,7 @@ private def mkGraphPart (decls : Array DeclInfo) (declHrefs : Std.HashMap Name S
 
 /-- Builds the root site part with chapter pages and utility sections. -/
 private def mkRootPart (cfg : Cli) (rootPrefix : Name) (groups : Array GroupInfo)
-    (decls : Array DeclInfo) (declHrefs : Std.HashMap Name String)
+    (decls : Array DeclInfo) (declHrefs declPageHrefs : Std.HashMap Name String)
     (introBlocks : Array (Block Manual)) (readerGuideBlocks : Array (Block Manual))
     (extraParts : Array (Part Manual)) : Part Manual :=
   let title := cfg.siteTitle.getD s!"{rootPrefix} exposition"
@@ -516,7 +552,7 @@ private def mkRootPart (cfg : Cli) (rootPrefix : Name) (groups : Array GroupInfo
       ++ introBlocks
       ++ readerGuideBlocks
       ++ mkDashboardBlocks groups
-    subParts := (groups.map fun group => mkGroupPart group cfg.repoUrl declHrefs)
+    subParts := (groups.map fun group => mkGroupPart group cfg.repoUrl declHrefs declPageHrefs)
       ++ extraParts
       ++ #[mkGraphPart decls declHrefs]
   }
@@ -585,22 +621,23 @@ unsafe def mainImpl (args : List String) : IO UInt32 := do
   else
     IO.println s!"Collected {decls.size} declarations under {rootPrefix}"
   let tfbInfo ← loadTrustedBaseInfo cfg rootPrefix
-  let decls := decls |> attachReverseDeps |> attachDependsOnSorry |> attachTrustedBaseFlags tfbInfo.names
+  let decls := decls |> attachReverseDeps |> attachTransitiveDeps |> attachDependsOnSorry |> attachTrustedBaseFlags tfbInfo.names
   let order ← moduleOrderMap cfg.projectDir rootPrefix
   let modules := buildModules rootPrefix order decls
   let groups := buildGroups order modules
   let declHrefs := declHrefMap decls
+  let declPageHrefs := declPageHrefMap decls
   let (introBlocks, extraParts) ← loadProjectContextParts cfg.projectDir cfg.repoUrl
   let tfbGroups := buildGroups order <| buildModules rootPrefix order <| decls.filter (·.inTfb)
   let targetBlocks ← loadTrustedBaseTargetBlocks cfg.projectDir cfg.repoUrl tfbInfo
   let hasContext := extraParts.any fun part => part.metadata.bind PartMetadata.file == some "context"
   let extraParts :=
     if tfbInfo.comparator?.isSome then
-      extraParts.push <| mkTrustedBasePart tfbGroups cfg.repoUrl declHrefs targetBlocks
+      extraParts.push <| mkTrustedBasePart tfbGroups cfg.repoUrl declHrefs declPageHrefs targetBlocks
     else
       extraParts
   let readerGuideBlocks := mkReaderGuideBlocks hasContext tfbInfo.comparator?.isSome
-  let root := mkRootPart cfg rootPrefix groups decls declHrefs introBlocks readerGuideBlocks extraParts
+  let root := mkRootPart cfg rootPrefix groups decls declHrefs declPageHrefs introBlocks readerGuideBlocks extraParts
   let versoArgs :=
     match cfg.outputDir with
     | some out => ["--output", out]

SITE_STRUCTURE.md

@@ -4,21 +4,22 @@ The exposition site logic is split across five files:
 
 | File | Lines | Purpose |
 |---|---|---|
-| `LeanExposition/Theme.lean` | 352 | Site CSS (`customCss`) |
+| `LeanExposition/Theme.lean` | 374 | Site CSS (`customCss`) |
 | `LeanExposition/GraphJs.lean` | 326 | Graph page JavaScript (`graphJs`) |
-| `LeanExposition/TocJs.lean` | 111 | TOC/utility-nav JavaScript (`tocJs`) |
-| `LeanExposition/Collect.lean` | 929 | Declaration collection and analysis pipeline |
-| `LeanExposition/Site.lean` | 576 | Rendering, page assembly, and CLI entrypoint wiring |
+| `LeanExposition/TocJs.lean` | 153 | TOC/utility-nav JavaScript (`tocJs`) |
+| `LeanExposition/Collect.lean` | 1109 | Declaration collection and analysis pipeline |
+| `LeanExposition/Site.lean` | 647 | Rendering, page assembly, and CLI entrypoint wiring |
 
 ---
 
 ## `LeanExposition/Theme.lean`
 
-### 1 · CSS (lines 1–352)
+### 1 · CSS (lines 1–374)
 
 `customCss` — the full site stylesheet as a Lean string literal. Covers CSS
-custom properties, layout, `.decl-card` variants, `.graph-*` components, TOC
-collapse, and responsive breakpoints.
+custom properties, layout, `.decl-card` variants, utility nav/buttons
+(including the "Hide Theorems" toggle), `.graph-*` components, TOC collapse,
+and responsive breakpoints.
 
 ---
 
@@ -38,44 +39,55 @@ collapse, and responsive breakpoints.
 
 ## `LeanExposition/TocJs.lean`
 
-### 1 · TOC behavior script (lines 1–111)
+### 1 · TOC behavior script (lines 1–153)
 
-`tocJs` — table-of-contents and utility-nav behavior:
+`tocJs (hasTfb : Bool)` — table-of-contents and utility-nav behavior:
 
-- injects the Overview / TFB / Graph utility links
+- injects the Overview / TFB (when present) / Graph utility links
 - removes duplicate utility entries from the generated TOC
 - adds a persistent TOC collapse/expand button via `localStorage`
+- adds a persistent "Hide Theorems" / "Show Theorems" toggle via `localStorage`
 
 ---
 
 ## `LeanExposition/Collect.lean`
 
-### 1 · Data model and CLI config (lines 18–153)
+### 1 · Data model and CLI config (lines 18–~155)
 
 Defines core structures and enums used by the exposition pipeline:
 `Cli`, `DeclKind`, `SourceInfo`, `LinkInfo`, `DeclCardData`, `DetailsData`,
 `GraphNode`, `GraphEdge`, `GraphData`, `DeclInfo`, `ModuleInfo`, `GroupInfo`,
 `MarkdownSection`, `ComparatorConfigInfo`, `TrustedBaseInfo`,
 `TargetStatementInfo`.
 
-### 2 · CLI parsing and naming helpers (lines 154–364)
+`DeclInfo` carries, among other fields, `deps` (all type+body dependencies),
+`typeDeps` (type-only dependencies), `usedBy` (reverse dependencies),
+`transDeps` (full transitive closure of `deps`), and `docstringBlock?` (a
+Verso `Block.docstring` rendered for the declaration).
+
+### 2 · CLI parsing and naming helpers (lines ~155–~365)
 
 `usage`, `parseArgs`, name/path helpers, slugging, inline/doc helpers, and
 README markdown section parsing.
 
-### 3 · Trusted-base and config loading (lines 365–523)
+### 3 · Trusted-base and config loading (lines ~365–~525)
 
 Filesystem/config readers, comparator config parsing, trusted-base target block
 loading, and trusted closure computation via `lake exe extractDeps`.
 
-### 4 · Declaration introspection pipeline (lines 524–894)
+### 4 · Declaration introspection pipeline (lines ~525–975)
 
 Signature extraction, source-range resolution, exposure filtering, module import
-traversal, and declaration collection into `DeclInfo` records.
+traversal, `mkDocstringBlock?` (builds the `{docstring ...}`-equivalent block
+via `MetaM`), href-map builders (`declHrefMap`, `declPageHrefMap`), and
+declaration collection into `DeclInfo` records (including type/body dependency
+splitting for defs, theorems, structures, and classes).
 
-### 5 · Post-processing passes (lines 895–925)
+### 5 · Post-processing passes (lines ~1050–1109)
 
-`attachReverseDeps`, `attachDependsOnSorry`, and `attachTrustedBaseFlags`.
+`attachReverseDeps` (computes `usedBy`), `attachTransitiveDeps` (computes
+`transDeps` via `transitiveClosure`), `attachDependsOnSorry`, and
+`attachTrustedBaseFlags`.
 
 ---
 
@@ -89,16 +101,20 @@ traversal, and declaration collection into `DeclInfo` records.
 
 `mkSourceParagraph`, `mkMarkdownPart`, `loadProjectContextParts`.
 
-### 3 · Verso block extensions and render config (lines 121–201)
+### 3 · Verso block extensions and render config (lines 121–212)
 
-`Block.declCard`, `Block.details`, `Block.graph`, and `renderConfig`.
+`Block.declCard`, `Block.details`, `Block.graph`, and `renderConfig`
+(`htmlDepth := 3`, so each declaration gets its own split page).
 
-### 4 · Page/document assembly (lines 203–494)
+### 4 · Page/document assembly (lines 213–559)
 
-Dashboard blocks, reader guides, declaration cards, chapter/module pages,
+Dashboard blocks, reader guides, declaration cards (`mkDeclBlock`, including a
+"Details" link to the declaration's dedicated page), dedicated per-declaration
+pages (`mkDeclPart`, listing direct "Type uses" / "Body uses" / "Used by" and
+the full "All dependencies, transitively" list), chapter/module pages,
 trusted-base pages, graph page, and root part construction.
 
-### 5 · Workspace loading and entrypoint (lines 496–576)
+### 5 · Workspace loading and entrypoint (lines 560–647)
 
 `withCurrentDir`, `loadWorkspaceAt`, `importRoots`, `firstRootPrefix`,
 `loadEnv`, and `mainImpl`.