[Vilin97]

Summary

Landing page (exposition/): adds a Lines of Lean stat tile and a sortable LOC column to the project table. LOC is the raw line count of LeanPool/<Project>.lean plus everything under LeanPool/<Project>/ (wc -l semantics; the pool total matches wc -l exactly).

Declarations viewer (exposition/decls/): each row now shows

• Main — ★ when the declaration is one of the project card's main results; this is the default sort (main first, alphabetical within),
• Deps / Dependents — direct intra-project counts,
• Dep cone / Dependent cone — transitive cone sizes within the project (excluding the declaration itself).

Count columns sort largest-first on first click; the two cone columns collapse on narrow screens.

Implementation

• cones.py: cone sizes over the SCC condensation using Python int bitsets (Tarjan emits components dependencies-first, so one forward and one backward pass suffice). 0.3 s for all 84K declarations of the live site.
• decls.json rows extend to [name, kind, project, declId, main, deps, dependents, depCone, dependentCone]; index.json and shard stats gain loc. Documented in SCHEMA.md (schema 1.2, additive).
• No extractor or CI changes; the generator CLI is unchanged.

Test plan

• uv run --group test pytest (320 passed), ruff check, ruff format --check
• Rebuilt index.json/decls.json from the live site's 174 shards and served the site locally: both pages render, default sort is main-first, per-column sorts verified (largest dep cone = topological_classification_of_surfaces, 5,905; largest dependent cone = Incompleteness LO.Arrow, 6,122)

🤖 Generated with Claude Code

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

The PR appears safe to merge with the changed exposition generation and rendering paths remaining internally consistent.

Summary

• Computes dependency cones over the SCC condensation and emits compact declaration metrics.
• Adds LOC totals, sortable landing-page data, declaration sorting, and responsive metric columns.
• Documents the additive payload fields and covers graph, shard, index, and declaration-index generation with tests.

_{Reviews (1) · Last reviewed commit: "exposition: LOC per project + main/depen..."}