[Vilin97]

A static companion site to the API docs, published at <pages-root>/exposition/ on the existing Pages deployment. Inspired by LML's exposition but rebuilt from scratch for the pool's scale: 58,431 declarations, 392,352 dependency edges, 130 projects.

What it does

• Per-project dependency graphs — every project gets a left-to-right layered graph (dependencies flow left → results right, longest-path layering with SCC collapse + barycenter crossing reduction, precomputed at build time). Header shows #nodes / #edges / max depth / avg depth and a kind legend. Since pool projects never import each other, there is deliberately no whole-pool hairball — the landing page's project table is the global view.
• Registry-card metadata — each graph page surfaces the projects.yml card: authors, math area, license, summary, source paper (DOI/arXiv) and upstream-repo links; main_declarations/main_results render as ★-ringed nodes and a click-to-select headline list with the card's informal statements.
• Declaration panel + dependency cones — clicking a node shows its statement (sliced from source), docstring, GitHub/API-docs links, uses/used-by lists, and a one-click dependency cone: ancestors + descendants re-layered client-side (e.g. Gödel I's cone: 2,966 ancestors). Deep-linkable via #d<id> / #cone=<id>.
• All-declarations viewer — all 58K declarations in one virtual-scrolled table, sortable and filterable by kind, project, and name substring; rows link into the graphs.
• Landing page — pool-wide stats, kind breakdown, and a sortable project table (area, provenance, license, decls, edges, depths).

How it's built

1. scripts/exposition/Extract.lean (via lake env lean --run — no lakefile changes, so no build-cache invalidation) walks the compiled environment and dumps human-written declarations with kernel-closure dependency edges (equation lemmas, match_* auxiliaries, projections, constructors tunnelled through to their parents; private declarations kept, demangled for display). 6.5 min / 7.9 GB peak locally.
2. python -m lean_pool.exposition computes layouts + stats and emits per-project JSON shards plus the static frontend (vanilla JS, zero external dependencies, dark/light theming). 11 s for the whole pool.
3. CI: a new exposition job in docs.yml runs in parallel with the doc-gen4 build, restores the same Docs-Lake cache (read-only), and uploads a ~30 MB artifact that the docs job merges into the Pages tree before deploy. Fail-soft: if the exposition job fails or times out, the docs deploy proceeds without it.

Verification

• 180 pytest tests green (layout, statement slicing, end-to-end generation), ruff + actionlint clean.
• Full-pool data audit: zero dangling/self/cross-project dependency references; shard layouts satisfy layer(node) > layer(dep) outside SCCs; stats/index/viewer cross-checks pass; byte-identical output across runs.
• A 21-agent adversarial review (data integrity, graph frontend, generator/extractor, CI, UX) produced 14 confirmed findings — all fixed here except five stale main_declarations names in projects.yml, which need a separate content-only PR (exact replacements identified).
• Browser-tested on the real pool including the largest project (Incompleteness: 8,225 nodes / 132K edges), light + dark, down to 800 px.

The five projects.yml main_declarations typos currently render as unlinked headline entries on their project pages; they self-heal once the content fix lands and the site rebuilds.

🤖 Generated with Claude Code

[github-actions]

🤖 LLM review (gpt-5.5)

Reviewed head: d4e0cb22621382d38b90e7b83bf3ae86aacf7632

Verdict: 🛑 request_changes

This PR adds a non-mathematical exposition site pipeline: a Lean extractor for declaration/dependency metadata, a Python static-site generator, frontend pages for project graphs and declaration search, tests, and a docs workflow job that publishes the generated site next to doc-gen4 output. It does not add or formalize a mathematical result, so under the Lean Pool project-intake criteria it is repository infrastructure rather than a mergeable formal-mathematics project.

Aspect	Value
Fit	🛑 not_a_fit
Level	undergraduate
Branch	repository tooling
Mode	mixed
Obscure problem	no
Code quality	4 / 5

The contribution is documentation and visualization infrastructure, not a theorem or theory-building formalization.

Findings (1)

• no-mathematical-project — PR-wide
  There is no headline mathematical theorem, source-anchored formalization, or project card because this is a docs/tooling PR; if the maintainer wants infrastructure changes reviewed under a different standard, this should be routed separately from Lean Pool project intake.

---

Tokens: 54,016 in / 1,322 out · Tier: flex · Cost: $0.1549
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

CI timing from this PR's run (all checks green):

job	time	notes
Build exposition site	26m59s	cache restore + pool delta build + extraction (~17 min of it) + generation + 30 MB artifact upload
Build doc-gen4 site	1m36s	near-no-op here (no pool modules changed); on content merges this typically runs 15–40 min
Lean Action CI (pool build)	8m32s	unchanged

Verdict on the every-commit vs daily question: every commit works. The exposition job runs in parallel with the docs build, so on real content merges (where docs itself takes 15–40 min) it adds little to nothing to the critical path; on docs-quiet runs the deploy waits at most ~25 extra minutes, bounded by the 30-min fail-soft poll. On a cold cache the job exceeds the poll window and the site deploys docs-only, healing on the next warm run.

One note: the artifact-merge step is gated to main pushes, so its first live execution happens on the merge commit — it's adversarially reviewed and fail-soft in every failure path, so the worst case is a docs-only deploy plus a warning annotation.

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.