From 82303dd2176de096d1b11dd99a8a0501869af180 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 9 Sep 2026 23:54:02 -0700 Subject: [PATCH] exposition: LOC per project + main/dependency metrics in decls viewer Landing page: a "Lines of Lean" tile and a LOC column on the project table (raw line count of LeanPool/.lean plus LeanPool//**). Declarations viewer: each row now carries whether the declaration is one of the project's main results (starred, sorted first by default), its direct dependency and dependent counts, and the sizes of its transitive dependency and dependent cones within the project. Cones are computed over the SCC condensation with integer bitsets (0.3 s for the whole pool). Co-Authored-By: Claude Fable 5.1 --- python/lean_pool/exposition/SCHEMA.md | 28 ++++-- python/lean_pool/exposition/cones.py | 86 +++++++++++++++++++ python/lean_pool/exposition/generate.py | 44 +++++++++- python/lean_pool/exposition/layout.py | 4 +- .../exposition/static/assets/landing.js | 3 + .../exposition/static/assets/viewer.css | 37 +++++++- .../exposition/static/assets/viewer.js | 63 +++++++++++++- .../exposition/static/decls/index.html | 10 +++ python/tests/test_exposition_cones.py | 34 ++++++++ python/tests/test_exposition_generate.py | 25 ++++-- 10 files changed, 304 insertions(+), 30 deletions(-) create mode 100644 python/lean_pool/exposition/cones.py create mode 100644 python/tests/test_exposition_cones.py diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md index 0481903575..5e81b01986 100644 --- a/python/lean_pool/exposition/SCHEMA.md +++ b/python/lean_pool/exposition/SCHEMA.md @@ -61,7 +61,7 @@ GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/.lean` plus every `.lean` file under +`LeanPool//`, 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//index.html#d`. +`p//index.html#d`. 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 diff --git a/python/lean_pool/exposition/cones.py b/python/lean_pool/exposition/cones.py new file mode 100644 index 0000000000..a0b306194f --- /dev/null +++ b/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) + ], + ) diff --git a/python/lean_pool/exposition/generate.py b/python/lean_pool/exposition/generate.py index 4bb42e00ab..5660c79bcb 100644 --- a/python/lean_pool/exposition/generate.py +++ b/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/.lean`` and ``LeanPool//``. + + 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} diff --git a/python/lean_pool/exposition/layout.py b/python/lean_pool/exposition/layout.py index 433290956c..706d733cbd 100644 --- a/python/lean_pool/exposition/layout.py +++ b/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: diff --git a/python/lean_pool/exposition/static/assets/landing.js b/python/lean_pool/exposition/static/assets/landing.js index 6f25ae85e1..d9e7ed8520 100644 --- a/python/lean_pool/exposition/static/assets/landing.js +++ b/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))); diff --git a/python/lean_pool/exposition/static/assets/viewer.css b/python/lean_pool/exposition/static/assets/viewer.css index 26a40c25ae..7e4c5ec4c5 100644 --- a/python/lean_pool/exposition/static/assets/viewer.css +++ b/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; + } } diff --git a/python/lean_pool/exposition/static/assets/viewer.js b/python/lean_pool/exposition/static/assets/viewer.js index 3a663576ed..4ef2932e0c 100644 --- a/python/lean_pool/exposition/static/assets/viewer.js +++ b/python/lean_pool/exposition/static/assets/viewer.js @@ -37,7 +37,13 @@ let kindOf = null; // Uint8Array let projectOf = null; // Uint16Array let declIdOf = null; // Uint32Array + let mainOf = null; // Uint8Array: 1 when listed as a project main result + let depsOf = null; // Uint32Array: direct intra-project dependencies + let dependentsOf = null; // Uint32Array: direct intra-project dependents + let depConeOf = null; // Uint32Array: transitive dependency cone size + let dependentConeOf = null; // Uint32Array: transitive dependent cone size let kindRank = null; // Uint8Array: kind index -> canonical display rank + const NUMERIC_COLUMNS = new Set(["deps", "dependents", "depCone", "dependentCone"]); const sortedOrders = new Map(); // column name -> ascending Uint32Array let filtered = null; // Uint32Array scratch; first filteredCount valid @@ -45,9 +51,11 @@ let kindFacetCounts = null; // Uint32Array: per-kind counts under project+search let chipCountEls = []; // kind index -> chip count element + // Default sort: main results first (descending on the 0/1 flag), then by + // name within each group. const state = { - column: "name", - descending: false, + column: "main", + descending: true, query: "", project: -1, // -1 = all projects kindActive: [], // boolean per kind index @@ -84,12 +92,30 @@ compare = (a, b) => kindRank[kindOf[a]] - kindRank[kindOf[b]] || nameCompare(a, b); } else if (column === "project") { compare = (a, b) => projectOf[a] - projectOf[b] || nameCompare(a, b); + } else if (column === "main") { + // Ascending order puts non-main first; the default (descending) walk + // of this array is then main-first, still alphabetical within groups. + compare = (a, b) => mainOf[a] - mainOf[b] || nameCompare(b, a); + } else if (NUMERIC_COLUMNS.has(column)) { + const values = numericColumn(column); + // Same trick: descending is the natural reading of a count column, so + // the ascending array reverses the name tie-break. + compare = (a, b) => values[a] - values[b] || nameCompare(b, a); } order.sort(compare); sortedOrders.set(column, order); return order; } + function numericColumn(column) { + switch (column) { + case "deps": return depsOf; + case "dependents": return dependentsOf; + case "depCone": return depConeOf; + default: return dependentConeOf; + } + } + // ---------- filtering ---------- function applyFilter() { @@ -133,16 +159,26 @@ const row = document.createElement("div"); row.className = "vrow"; // A real link gives keyboard focus, Enter activation, and open-in-new-tab. + const main = document.createElement("span"); + main.className = "vcell-main"; const name = document.createElement("a"); name.className = "vcell-name"; const kind = document.createElement("span"); kind.className = "kchip"; const project = document.createElement("a"); project.className = "vcell-project"; - row.append(name, kind, project); + row.append(main, name, kind, project); + row._main = main; row._name = name; row._kind = kind; row._project = project; + row._nums = []; + for (let c = 0; c < 4; c++) { + const cell = document.createElement("span"); + cell.className = "vcell-num"; + row.appendChild(cell); + row._nums.push(cell); + } return row; } @@ -156,6 +192,10 @@ function fillRow(row, i) { row.dataset.index = i; + const isMain = mainOf[i] === 1; + row._main.textContent = isMain ? "★" : ""; + row._main.title = isMain ? "Main result" : ""; + row.classList.toggle("vrow-main", isMain); row._name.textContent = names[i]; const slug = projects[projectOf[i]]; row._name.href = `../p/${encodeURIComponent(slug)}/index.html#d${declIdOf[i]}`; @@ -164,6 +204,10 @@ row._kind.className = `kchip ${kindClass(kindName)}`; row._project.textContent = slug; row._project.href = `../p/${encodeURIComponent(slug)}/`; + row._nums[0].textContent = formatCount(depsOf[i]); + row._nums[1].textContent = formatCount(dependentsOf[i]); + row._nums[2].textContent = formatCount(depConeOf[i]); + row._nums[3].textContent = formatCount(dependentConeOf[i]); } function renderWindow() { @@ -289,7 +333,8 @@ state.descending = !state.descending; } else { state.column = column; - state.descending = false; + // Flag and count columns read naturally largest/starred first. + state.descending = column === "main" || NUMERIC_COLUMNS.has(column); } updateSortIndicators(); refresh(true); @@ -309,6 +354,11 @@ kindOf = new Uint8Array(total); projectOf = new Uint16Array(total); declIdOf = new Uint32Array(total); + mainOf = new Uint8Array(total); + depsOf = new Uint32Array(total); + dependentsOf = new Uint32Array(total); + depConeOf = new Uint32Array(total); + dependentConeOf = new Uint32Array(total); const kindCounts = new Array(kinds.length).fill(0); for (let i = 0; i < total; i++) { const row = raw[i]; @@ -317,6 +367,11 @@ kindOf[i] = row[1]; projectOf[i] = row[2]; declIdOf[i] = row[3]; + mainOf[i] = row[4] || 0; + depsOf[i] = row[5] || 0; + dependentsOf[i] = row[6] || 0; + depConeOf[i] = row[7] || 0; + dependentConeOf[i] = row[8] || 0; kindCounts[row[1]] += 1; } diff --git a/python/lean_pool/exposition/static/decls/index.html b/python/lean_pool/exposition/static/decls/index.html index 8dc11ffab5..3600c40ec9 100644 --- a/python/lean_pool/exposition/static/decls/index.html +++ b/python/lean_pool/exposition/static/decls/index.html @@ -34,9 +34,19 @@
+ + + + +
diff --git a/python/tests/test_exposition_cones.py b/python/tests/test_exposition_cones.py new file mode 100644 index 0000000000..22f4e850a9 --- /dev/null +++ b/python/tests/test_exposition_cones.py @@ -0,0 +1,34 @@ +"""Tests for per-declaration dependency cone metrics.""" + +from __future__ import annotations + +from lean_pool.exposition.cones import compute_cone_metrics + + +def test_chain_and_diamond() -> None: + """Cones are transitive and exclude the node itself; counts are direct.""" + # 0 <- 1 <- 3, 0 <- 2 <- 3 (3 depends on 1 and 2, both depend on 0), + # 4 depends on 3, 5 is isolated. + dependencies = [[], [0], [0], [1, 2], [3], []] + metrics = compute_cone_metrics(dependencies) + assert metrics.dependent_counts == [2, 1, 1, 1, 0, 0] + assert metrics.dependency_cone_sizes == [0, 1, 1, 3, 4, 0] + assert metrics.dependent_cone_sizes == [4, 2, 2, 1, 0, 0] + + +def test_cycle_members_count_each_other() -> None: + """Members of a cycle appear in each other's cones exactly once.""" + # 0 <-> 1 (mutual recursion), 2 depends on 1. + dependencies = [[1], [0], [1]] + metrics = compute_cone_metrics(dependencies) + assert metrics.dependent_counts == [1, 2, 0] + assert metrics.dependency_cone_sizes == [1, 1, 2] + assert metrics.dependent_cone_sizes == [2, 2, 0] + + +def test_empty_graph() -> None: + """No nodes yields empty metric lists.""" + metrics = compute_cone_metrics([]) + assert metrics.dependent_counts == [] + assert metrics.dependency_cone_sizes == [] + assert metrics.dependent_cone_sizes == [] diff --git a/python/tests/test_exposition_generate.py b/python/tests/test_exposition_generate.py index 74f88719c6..89c915a8f6 100644 --- a/python/tests/test_exposition_generate.py +++ b/python/tests/test_exposition_generate.py @@ -247,6 +247,7 @@ def test_project_shard_schema_and_stats(site: tuple[Path, SiteSummary]) -> None: assert shard["provenance"] == "AI" assert shard["stats"] == { "nodes": 4, + "loc": 9, # One.lean (7 lines) + Two.lean (2 lines) "edges": 2, "maxDepth": 2, "avgDepth": 0.75, @@ -377,6 +378,7 @@ def test_index_json(site: tuple[Path, SiteSummary]) -> None: assert index["totals"] == { "projects": 2, "decls": 7, + "loc": 14, "edges": 3, "maxDepth": 2, "kinds": {"theorem": 3, "def": 2, "lemma": 2}, @@ -387,6 +389,7 @@ def test_index_json(site: tuple[Path, SiteSummary]) -> None: "title": "Alpha & Co", "provenance": "AI", "nodes": 4, + "loc": 9, "edges": 2, "maxDepth": 2, "avgDepth": 0.75, @@ -399,26 +402,32 @@ def test_index_json(site: tuple[Path, SiteSummary]) -> None: assert beta_row["title"] is None # pseudo-project: no registry card assert beta_row["provenance"] is None assert beta_row["avgDepth"] == 0.33 + assert beta_row["loc"] == 5 assert beta_row["authors"] is None assert beta_row["license"] is None assert beta_row["mainResults"] == 0 def test_decls_json(site: tuple[Path, SiteSummary]) -> None: - """decls.json rows are [name, kindIdx, projectIdx, declId].""" + """decls.json rows carry the viewer columns and per-node graph metrics. + + Row layout: [name, kindIdx, projectIdx, declId, main, deps, dependents, + depCone, dependentCone]. In Alpha the chain is a4 -> a2 -> a1, so a1 has + two transitive dependents and a4 a two-node dependency cone. + """ out, _ = site declarations = _load(out, "data/decls.json") assert declarations["schema"] == 1 assert declarations["kinds"] == ["theorem", "def", "lemma"] assert declarations["projects"] == ["Alpha", "Beta"] assert declarations["decls"] == [ - ["a1", 2, 0, 0], - ["a2", 0, 0, 1], - ["a3", 1, 0, 2], - ["a4", 0, 0, 3], - ["b1", 1, 1, 0], - ["b2", 2, 1, 1], - ["b3", 0, 1, 2], + ["a1", 2, 0, 0, 0, 0, 1, 0, 2], + ["a2", 0, 0, 1, 1, 1, 1, 1, 1], + ["a3", 1, 0, 2, 1, 0, 0, 0, 0], + ["a4", 0, 0, 3, 0, 1, 0, 2, 0], + ["b1", 1, 1, 0, 0, 0, 1, 0, 1], + ["b2", 2, 1, 1, 0, 1, 0, 1, 0], + ["b3", 0, 1, 2, 0, 0, 0, 0, 0], ]