exposition: LOC per project + main-result/dependency metrics in decls viewer

python/lean_pool/exposition/SCHEMA.md

@@ -61,7 +61,7 @@ GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/<LeanPool/A/B.lea
  "project": "ABCExceptions",
  "title": "…",                 // from projects.yml; null for pseudo-projects
  "provenance": "human",        // "human" | "AI" | "mix" | null
- "stats": {"nodes": 235, "edges": 817, "maxDepth": 14, "avgDepth": 3.71,
+ "stats": {"nodes": 235, "loc": 4120, "edges": 817, "maxDepth": 14, "avgDepth": 3.71,
            "kinds": {"lemma": 120, "theorem": 75, "def": 37, "structure": 3}},
  "modules": ["LeanPool.ABCExceptions.Section2", …],
  "layers": [40, 31, …],        // node count per layer, index = layer
@@ -88,7 +88,9 @@ GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/<LeanPool/A/B.lea
 Depth definitions: `layer(n) = 0` if `n` has no intra-project deps, else
 `1 + max(layer(dep))` (cycles collapsed via SCC condensation — every member of
 an SCC shares the layer). `maxDepth = max layer`, `avgDepth = mean layer`
-(2 decimals). `edges = Σ len(deps)`.
+(2 decimals). `edges = Σ len(deps)`. `loc` (schema 1.2) is the raw line
+count of `LeanPool/<Project>.lean` plus every `.lean` file under
+`LeanPool/<Project>/`, exposed or not (`wc -l` semantics).
 
 ### Card metadata (schema 1.1, additive)
 
@@ -164,17 +166,18 @@ it needs module sources not yet fetched; callers fetch and retry.
 
 ```json
 {"schema": 1, "commit": "abc123", "generated": "2026-07-21T12:00:00Z",
- "totals": {"projects": 126, "decls": 55600, "edges": 210000,
+ "totals": {"projects": 126, "decls": 55600, "loc": 1200000, "edges": 210000,
             "maxDepth": 41, "kinds": {"lemma": …}},
  "projects": [{"slug": "ABCExceptions", "title": "…", "provenance": "human",
-               "nodes": 235, "edges": 817, "maxDepth": 14, "avgDepth": 3.71,
+               "nodes": 235, "loc": 4120, "edges": 817, "maxDepth": 14, "avgDepth": 3.71,
                "authors": ["…"], "license": "Apache-2.0",
                "branch": "analytic number theory", "mainResults": 3}, …]}
 ```
 
-Sorted by slug. `totals.maxDepth` is the max over projects. The last four
-fields are schema 1.1 additions (null / 0 for pseudo-projects); the landing
-table shows branch and license columns and an authors line under the title.
+Sorted by slug. `totals.maxDepth` is the max over projects; `totals.loc`
+is the sum. The last four fields are schema 1.1 additions (null / 0 for
+pseudo-projects); the landing table shows branch and license columns and an
+authors line under the title. `loc` (schema 1.2) is the project's line count.
 
 ## `data/decls.json` (all-declarations viewer index)
 
@@ -184,11 +187,18 @@ Compact arrays to keep the file small (~55K rows):
 {"schema": 1,
  "kinds": ["lemma", "theorem", …],
  "projects": ["ABCExceptions", …],       // slugs, same order as index.json
- "decls": [["Foo.aux", 0, 0, 12], …]}    // [name, kindIdx, projectIdx, declId]
+ "decls": [["Foo.aux", 0, 0, 12, 1, 3, 7, 5, 41], …]}
+ // [name, kindIdx, projectIdx, declId, main, deps, dependents, depCone, dependentCone]
 ```
 
 `declId` indexes into that project's shard `decls`; the viewer links a row to
-`p/<slug>/index.html#d<declId>`.
+`p/<slug>/index.html#d<declId>`. The remaining five columns (schema 1.2) are
+graph metrics within the project: `main` is 1 when the declaration is one of
+the card's main results, `deps`/`dependents` are the direct intra-project
+in/out counts, and `depCone`/`dependentCone` are the sizes of the transitive
+dependency and dependent cones (excluding the declaration itself; members of
+a dependency cycle count each other). The viewer sorts main results first by
+default.
 
 ## Page shells
 

python/lean_pool/exposition/cones.py

@@ -0,0 +1,86 @@
+"""Per-declaration dependency metrics for the all-declarations viewer.
+
+Given the intra-project dependency lists of one shard, computes for every
+node its direct dependent count and the sizes of its two transitive cones:
+the *dependency cone* (everything it transitively uses) and the *dependent
+cone* (everything that transitively uses it). Both exclude the node itself.
+
+Cones are accumulated over the SCC condensation as Python integer bitsets:
+components come out of Tarjan dependencies-first, so one forward pass unions
+each component's members with the cones of the components it depends on,
+and one backward pass does the same for dependents. Cycles (mutual
+recursion) therefore count every other member of the cycle in both cones.
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+
+from lean_pool.exposition.layout import strongly_connected_components
+
+
+@dataclass
+class ConeMetrics:
+    """Per-node metrics, indexed by shard-local node id."""
+
+    dependent_counts: list[int]
+    dependency_cone_sizes: list[int]
+    dependent_cone_sizes: list[int]
+
+
+def _component_cones(
+    components: list[list[int]],
+    component_of: list[int],
+    neighbors: list[list[int]],
+    order: range,
+) -> list[int]:
+    """Union member bits with neighbor-component cones, visiting ``order``.
+
+    ``order`` must list every component after all components reachable from
+    it through ``neighbors``.
+    """
+    cones = [0] * len(components)
+    for component_index in order:
+        bits = 0
+        for node in components[component_index]:
+            bits |= 1 << node
+        for node in components[component_index]:
+            for neighbor in neighbors[node]:
+                neighbor_component = component_of[neighbor]
+                if neighbor_component != component_index:
+                    bits |= cones[neighbor_component]
+        cones[component_index] = bits
+    return cones
+
+
+def compute_cone_metrics(dependencies: list[list[int]]) -> ConeMetrics:
+    """Return dependent counts and transitive cone sizes for every node.
+
+    ``dependencies[n]`` lists the node ids that node ``n`` depends on
+    (self references already removed).
+    """
+    node_count = len(dependencies)
+    dependents: list[list[int]] = [[] for _ in range(node_count)]
+    for node, node_dependencies in enumerate(dependencies):
+        for dependency in node_dependencies:
+            dependents[dependency].append(node)
+    components = strongly_connected_components(dependencies)
+    component_of = [0] * node_count
+    for component_index, members in enumerate(components):
+        for node in members:
+            component_of[node] = component_index
+    forward = range(len(components))
+    backward = range(len(components) - 1, -1, -1)
+    dependency_cones = _component_cones(components, component_of, dependencies, forward)
+    dependent_cones = _component_cones(components, component_of, dependents, backward)
+    return ConeMetrics(
+        dependent_counts=[len(nodes) for nodes in dependents],
+        dependency_cone_sizes=[
+            (dependency_cones[component_of[node]] & ~(1 << node)).bit_count()
+            for node in range(node_count)
+        ],
+        dependent_cone_sizes=[
+            (dependent_cones[component_of[node]] & ~(1 << node)).bit_count()
+            for node in range(node_count)
+        ],
+    )

python/lean_pool/exposition/generate.py

@@ -22,6 +22,7 @@
 
 import yaml
 
+from lean_pool.exposition.cones import compute_cone_metrics
 from lean_pool.exposition.layout import compute_layout
 from lean_pool.exposition.source_text import (
     ModuleSkeleton,
@@ -65,13 +66,13 @@ class SourceCache:
 
     def __init__(self, repo_root: Path) -> None:
         """Remember the repository root that module paths resolve against."""
-        self._repo_root = repo_root
+        self.repo_root = repo_root
         self._files: dict[str, SourceFile | None] = {}
 
     def get(self, module: str) -> SourceFile | None:
         """Return the parsed source for ``module``, or ``None`` if missing."""
         if module not in self._files:
-            path = self._repo_root.joinpath(*module.split(".")).with_suffix(".lean")
+            path = self.repo_root.joinpath(*module.split(".")).with_suffix(".lean")
             if path.is_file():
                 text = path.read_text(encoding="utf-8")
                 self._files[module] = SourceFile.from_text(text)
@@ -335,6 +336,25 @@ def _build_node(
     return node
 
 
+def _count_lines(path: Path) -> int:
+    """Count raw newline-delimited lines in one file (``wc -l`` semantics)."""
+    with path.open("rb") as handle:
+        return sum(1 for _ in handle)
+
+
+def count_project_loc(repo_root: Path, slug: str) -> int:
+    """Total lines of Lean in ``LeanPool/<slug>.lean`` and ``LeanPool/<slug>/``.
+
+    Counts every ``.lean`` file under the project directory, whether or not
+    the extractor exposed declarations from it, so the figure matches what
+    ``wc -l`` reports for the project tree.
+    """
+    pool_directory = Path(repo_root) / "LeanPool"
+    paths = [pool_directory / f"{slug}.lean"]
+    paths.extend(sorted((pool_directory / slug).rglob("*.lean")))
+    return sum(_count_lines(path) for path in paths if path.is_file())
+
+
 def _kind_counts(kinds: list[str]) -> dict[str, int]:
     """Count kinds, ordered by descending count then name for determinism."""
     counts = Counter(kinds)
@@ -441,6 +461,7 @@ def build_project_shard(
     average = sum(layout.node_layers) / node_count if node_count else 0.0
     stats = {
         "nodes": node_count,
+        "loc": count_project_loc(source_cache.repo_root, slug),
         "edges": sum(len(dependencies) for dependencies in dependency_lists),
         "maxDepth": max(layout.node_layers, default=0),
         "avgDepth": round(average, 2),
@@ -498,6 +519,7 @@ def build_index(shards: dict[str, dict], commit: str) -> dict:
                 "title": shard["title"],
                 "provenance": shard["provenance"],
                 "nodes": stats["nodes"],
+                "loc": stats["loc"],
                 "edges": stats["edges"],
                 "maxDepth": stats["maxDepth"],
                 "avgDepth": stats["avgDepth"],
@@ -510,6 +532,7 @@ def build_index(shards: dict[str, dict], commit: str) -> dict:
     totals = {
         "projects": len(project_rows),
         "decls": sum(row["nodes"] for row in project_rows),
+        "loc": sum(row["loc"] for row in project_rows),
         "edges": sum(row["edges"] for row in project_rows),
         "maxDepth": max((row["maxDepth"] for row in project_rows), default=0),
         "kinds": dict(
@@ -527,19 +550,32 @@ def build_index(shards: dict[str, dict], commit: str) -> dict:
 
 
 def build_declaration_index(shards: dict[str, dict], index: dict) -> dict:
-    """Build the compact ``data/decls.json`` payload for the viewer."""
+    """Build the compact ``data/decls.json`` payload for the viewer.
+
+    Each row is ``[name, kindIdx, projectIdx, declId, main, deps,
+    dependents, depCone, dependentCone]`` (schema 1.2): the main-result
+    flag (0/1), direct dependency and dependent counts, and the sizes of
+    the transitive dependency and dependent cones within the project.
+    """
     kinds = list(index["totals"]["kinds"])
     kind_indices = {kind: position for position, kind in enumerate(kinds)}
     slugs = [row["slug"] for row in index["projects"]]
     rows = []
     for project_position, slug in enumerate(slugs):
-        for declaration_id, node in enumerate(shards[slug]["decls"]):
+        nodes = shards[slug]["decls"]
+        metrics = compute_cone_metrics([node["deps"] for node in nodes])
+        for declaration_id, node in enumerate(nodes):
             rows.append(
                 [
                     node["name"],
                     kind_indices[node["kind"]],
                     project_position,
                     declaration_id,
+                    1 if node.get("main") else 0,
+                    len(node["deps"]),
+                    metrics.dependent_counts[declaration_id],
+                    metrics.dependency_cone_sizes[declaration_id],
+                    metrics.dependent_cone_sizes[declaration_id],
                 ]
             )
     return {"schema": 1, "kinds": kinds, "projects": slugs, "decls": rows}

python/lean_pool/exposition/layout.py

@@ -44,7 +44,7 @@ def compute_layout(dependencies: list[list[int]]) -> Layout:
     )
 
 
-def _strongly_connected_components(adjacency: list[list[int]]) -> list[list[int]]:
+def strongly_connected_components(adjacency: list[list[int]]) -> list[list[int]]:
     """Return SCCs via iterative Tarjan, dependencies-first.
 
     With edges pointing node -> dependency, Tarjan emits each component
@@ -99,7 +99,7 @@ def _strongly_connected_components(adjacency: list[list[int]]) -> list[list[int]
 
 def _longest_path_layers(dependencies: list[list[int]]) -> list[int]:
     """Return the longest-path layer of every node (SCCs share a layer)."""
-    components = _strongly_connected_components(dependencies)
+    components = strongly_connected_components(dependencies)
     component_of = [0] * len(dependencies)
     for component_index, members in enumerate(components):
         for node in members:

python/lean_pool/exposition/static/assets/landing.js

@@ -20,6 +20,7 @@
     { key: "provenance", label: "Provenance", numeric: false },
     { key: "license", label: "License", numeric: false },
     { key: "nodes", label: "Decls", numeric: true },
+    { key: "loc", label: "LOC", numeric: true },
     { key: "edges", label: "Edges", numeric: true },
     { key: "maxDepth", label: "Max depth", numeric: true },
     { key: "avgDepth", label: "Avg depth", numeric: true },
@@ -47,6 +48,7 @@
     const tiles = [
       ["Projects", totals.projects],
       ["Declarations", totals.decls],
+      ["Lines of Lean", totals.loc || 0],
       ["Dependency edges", totals.edges],
       ["Deepest chain", totals.maxDepth],
     ];
@@ -204,6 +206,7 @@
     tr.appendChild(licenseCell);
 
     tr.appendChild(numericCell(formatCount(project.nodes)));
+    tr.appendChild(numericCell(formatCount(project.loc || 0)));
     tr.appendChild(numericCell(formatCount(project.edges)));
     tr.appendChild(numericCell(formatCount(project.maxDepth)));
     tr.appendChild(numericCell(Number(project.avgDepth || 0).toFixed(2)));

python/lean_pool/exposition/static/assets/viewer.css

@@ -348,7 +348,7 @@
   flex-direction: column;
   height: calc(100vh - var(--header-h, 49px));
   height: calc(100dvh - var(--header-h, 49px));
-  max-width: 1200px;
+  max-width: 1440px;
   margin: 0 auto;
   padding: 16px 24px 16px;
   box-sizing: border-box;
@@ -435,7 +435,8 @@
 .vhead,
 .vrow {
   display: grid;
-  grid-template-columns: minmax(0, 1fr) 110px 200px;
+  /* main ★ | name | kind | project | deps | dependents | dep cone | dependent cone */
+  grid-template-columns: 28px minmax(0, 1fr) 100px 180px 56px 88px 76px 112px;
   gap: 12px;
   align-items: center;
   padding: 0 14px;
@@ -475,6 +476,29 @@
   content: " ↓";
 }
 
+.vsort.num,
+.vcell-num {
+  text-align: right;
+}
+
+.vcell-num {
+  font-variant-numeric: tabular-nums;
+  color: var(--muted);
+  font-size: 12.5px;
+  white-space: nowrap;
+}
+
+.vcell-main {
+  color: var(--star);
+  text-align: center;
+  font-size: 14px;
+  line-height: 1;
+}
+
+.vrow-main .vcell-name {
+  font-weight: 600;
+}
+
 .vspacer {
   position: relative;
 }
@@ -557,7 +581,14 @@ a.vcell-name:focus-visible {
 
   .vhead,
   .vrow {
-    grid-template-columns: minmax(0, 1fr) 92px 150px;
+    grid-template-columns: 24px minmax(0, 1fr) 92px 130px 52px 84px;
     gap: 8px;
   }
+
+  /* drop the two cone columns; the direct counts stay */
+  .vsort[data-col="depCone"],
+  .vsort[data-col="dependentCone"],
+  .vcell-num:nth-last-child(-n + 2) {
+    display: none;
+  }
 }