Add exposition site: per-project dependency graphs + declaration index

.github/workflows/docs.yml

@@ -11,6 +11,7 @@ on:
       - 'lake-manifest.json'
       - 'lean-toolchain'
       - 'docbuild/**'
+      - 'python/lean_pool/exposition/**'
       - '.github/workflows/docs.yml'
   pull_request:
     branches:
@@ -22,6 +23,7 @@ on:
       - 'lake-manifest.json'
       - 'lean-toolchain'
       - 'docbuild/**'
+      - 'python/lean_pool/exposition/**'
       - '.github/workflows/docs.yml'
   workflow_dispatch:
 
@@ -33,8 +35,75 @@ permissions:
   contents: read
   pages: write
   id-token: write
+  actions: read
 
 jobs:
+  # Runs in parallel with the doc-gen4 build; its (small) artifact is merged
+  # into the Pages tree by the `build` job just before deployment. Restores
+  # the same cache as `build` but never saves it — `build` owns cache writes.
+  exposition:
+    runs-on: ubuntu-latest
+    name: Build exposition site
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+
+      - name: Restore caches
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: |
+            ~/.elan
+            .lake/packages
+            .lake/build
+            docbuild/.lake/build
+          key: Docs-Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'docbuild/lake-manifest.json', 'LeanPool.lean') }}-${{ github.sha }}
+          restore-keys: |
+            Docs-Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'docbuild/lake-manifest.json', 'LeanPool.lean') }}-
+            Docs-Lake-${{ runner.os }}-
+
+      - name: Install Lean
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
+        with:
+          auto-config: false
+          use-github-cache: false
+          use-mathlib-cache: false
+
+      - name: Install Mathlib cache
+        run: |
+          if [ ! -d ".lake/packages/mathlib" ]; then
+            ~/.elan/bin/lake exe cache get
+          else
+            echo "Mathlib already present from cache"
+          fi
+
+      - name: Build pool
+        run: ~/.elan/bin/lake build LeanPool
+
+      - name: Extract declarations
+        run: ~/.elan/bin/lake env ~/.elan/bin/lean --run scripts/exposition/Extract.lean exposition-dump.jsonl
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
+      - name: Generate site
+        run: |
+          cd python
+          uv sync --locked
+          uv run python -m lean_pool.exposition \
+            --dump ../exposition-dump.jsonl \
+            --repo-root .. \
+            --out ../exposition-site \
+            --commit ${{ github.sha }}
+
+      - name: Upload exposition artifact
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: exposition-site
+          path: exposition-site
+          retention-days: 3
+
   build:
     runs-on: ubuntu-latest
     name: Build doc-gen4 site
@@ -80,6 +149,41 @@ jobs:
         id: build
         run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs
 
+      - name: Add exposition site
+        # Wait for the parallel `exposition` job's artifact and merge it into
+        # the Pages tree. Fail-soft: if that job failed or timed out, deploy
+        # the docs without the exposition rather than blocking the site.
+        if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          # Drop any exposition tree restored from the Docs-Lake cache so the
+          # deploy matches the fresh artifact exactly (or omits the exposition
+          # entirely on the fail-soft paths) — never a stale mixture.
+          rm -rf docbuild/.lake/build/doc/exposition
+          deadline=$((SECONDS + 1800))
+          while [ "$SECONDS" -lt "$deadline" ]; do
+            found=$(gh api "repos/${{ github.repository }}/actions/runs/${{ github.run_id }}/artifacts" \
+              --jq '[.artifacts[] | select(.name == "exposition-site" and .expired == false)] | length' || echo 0)
+            if [ "$found" -ge 1 ]; then
+              if gh run download "${{ github.run_id }}" --repo "${{ github.repository }}" \
+                  --name exposition-site --dir docbuild/.lake/build/doc/exposition; then
+                echo "Exposition site merged into Pages tree."
+              else
+                echo "::warning::Exposition artifact download failed; deploying docs without it."
+              fi
+              exit 0
+            fi
+            conclusion=$(gh api "repos/${{ github.repository }}/actions/runs/${{ github.run_id }}/jobs" \
+              --jq '.jobs[] | select(.name == "Build exposition site") | .conclusion' || echo "")
+            if [ "$conclusion" = "failure" ] || [ "$conclusion" = "cancelled" ]; then
+              echo "::warning::Exposition job concluded with '$conclusion'; deploying docs without it."
+              exit 0
+            fi
+            sleep 20
+          done
+          echo "::warning::Timed out waiting for the exposition artifact; deploying docs without it."
+
       - name: Configure Pages
         if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'
         uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b

.gitignore

@@ -2,6 +2,10 @@
 /docbuild/.lake
 .env
 
+# Exposition build outputs (see python/lean_pool/exposition/)
+/exposition-dump.jsonl
+/exposition-site/
+
 # Python
 __pycache__/
 *.pyc

python/lean_pool/exposition/SCHEMA.md

@@ -0,0 +1,154 @@
+# Exposition site: data formats and layout contract
+
+The exposition is a static site published at `<pages-root>/exposition/` next to
+the doc-gen4 API docs (which live at `<pages-root>/`). It is produced in two
+steps:
+
+1. **Extractor** (`scripts/exposition/Extract.lean`, run via
+   `lake env lean --run`): dumps one JSON object per human-written declaration
+   (JSONL). Kernel-level dependency edges are pre-resolved to human-written
+   declarations; compiler-generated auxiliaries are tunnelled through.
+2. **Generator** (`python -m lean_pool.exposition`): reads the dump, the
+   project registry (`LeanPool/projects.yml`) and the Lean sources; computes
+   per-project layered layouts and stats; emits the static site.
+
+## Extractor dump (JSONL, one line per declaration)
+
+```json
+{"id": "_private.LeanPool.X.0.Foo.aux",   // full (possibly mangled) name — unique
+ "n": "Foo.aux",                           // display name (private names demangled)
+ "m": "LeanPool.ABCExceptions.Section2",   // defining module
+ "k": "theorem",                           // coarse kind: theorem|def|instance|structure|class|inductive|axiom|opaque
+ "r": [435, 0, 446, 23],                   // range: start line, start col, end line, end col (1-based lines)
+ "s": [435, 6],                            // selection (name token) line/col
+ "d": "docstring",                         // optional
+ "p": true,                                // optional: private
+ "deps": ["<id>", ...],                    // intra-pool dependency ids (other dump lines)
+ "ext": 127}                               // count of distinct external (Mathlib/core) constants used
+```
+
+The generator refines `k` from source text (`lemma` vs `theorem`, `abbrev` vs
+`def`) and slices the statement text (keyword up to the top-level `:=` /
+`where` / `|` boundary — same approach as `scripts/proof-profile/statements.py`).
+
+## Site tree
+
+```
+exposition/
+  index.html              # landing: pool totals + sortable project table
+  decls/index.html        # all-declarations viewer
+  p/<Project>/index.html  # per-project graph page (one per project)
+  assets/…                # shared JS/CSS (copied verbatim from static/)
+  data/index.json
+  data/decls.json
+  data/projects/<Project>.json
+```
+
+`<Project>` is the second component of the module name
+(`LeanPool.ABCExceptions.Section2` → `ABCExceptions`). Modules sitting directly
+under `LeanPool/` (e.g. `LeanPool.Basic`) form a pseudo-project named after the
+module ("Basic") with no registry card.
+
+Relative bases from `p/<Project>/index.html`: exposition root `../..`,
+doc-gen4 root `../../..`. doc-gen4 page for a non-private declaration
+`Foo.bar` in module `LeanPool.A.B`: `<docs-root>/LeanPool/A/B.html#Foo.bar`.
+GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/<LeanPool/A/B.lean>#L<line>-L<endLine>`.
+
+## `data/projects/<Project>.json` (shard)
+
+```json
+{"schema": 1,
+ "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,
+           "kinds": {"lemma": 120, "theorem": 75, "def": 37, "structure": 3}},
+ "modules": ["LeanPool.ABCExceptions.Section2", …],
+ "layers": [40, 31, …],        // node count per layer, index = layer
+ "decls": [ … ]}
+```
+
+`decls[i]` — the node with id `i` (ids are shard-local array indices):
+
+```json
+{"name": "Foo.aux",
+ "full": "_private.…",         // only when it differs from name (⇒ no doc-gen page)
+ "kind": "lemma",              // refined source keyword
+ "module": 0,                  // index into modules
+ "line": 435, "endLine": 446,
+ "doc": "…",                   // optional
+ "statement": "lemma aux (h : …) : …",  // ≤ 1200 chars, trimmed
+ "private": true,              // optional
+ "deps": [3, 17],              // node ids this declaration uses
+ "ext": 127,
+ "layer": 5,                   // x: longest-path layer, 0 = no intra-project deps
+ "order": 12}                  // y: position within layer after crossing reduction
+```
+
+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)`.
+
+### Card metadata (schema 1.1, additive)
+
+Each shard additionally carries the project's registry card (from
+`LeanPool/projects.yml`, matched via `entry_module`'s last component;
+`card` is `null` for pseudo-projects):
+
+```json
+"card": {"authors": ["…"], "license": "Apache-2.0", "branch": "extremal combinatorics",
+         "summary": "…", "tags": ["…"], "msc": ["05D05"], "status": "verified",
+         "source": {"title": "…", "authors": ["…"],
+                    "doi": "…" | "arxiv": "…" | "url": "…",   // one or more; link priority doi > arxiv > url
+                    "github_repo": "owner/repo"}},             // optional
+"mainResults": [{"id": 12, "name": "BooleanIsoperimetry.harper_theorem",
+                 "informal": "…"}]                             // id null if unresolved
+```
+
+`mainResults` is the union of the card's `main_declarations` and
+`main_results` (informal text when available), resolved to node ids by
+display name. Every resolved id's decl entry also gets `"main": true` —
+frontends render these as visually distinguished ("starred") nodes.
+Link recipes: `doi` → `https://doi.org/<doi>`, `arxiv` →
+`https://arxiv.org/abs/<arxiv>`, `url` as-is, `github_repo` →
+`https://github.com/<github_repo>`.
+
+## `data/index.json`
+
+```json
+{"schema": 1, "commit": "abc123", "generated": "2026-07-21T12:00:00Z",
+ "totals": {"projects": 126, "decls": 55600, "edges": 210000,
+            "maxDepth": 41, "kinds": {"lemma": …}},
+ "projects": [{"slug": "ABCExceptions", "title": "…", "provenance": "human",
+               "nodes": 235, "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.
+
+## `data/decls.json` (all-declarations viewer index)
+
+Compact arrays to keep the file small (~55K rows):
+
+```json
+{"schema": 1,
+ "kinds": ["lemma", "theorem", …],
+ "projects": ["ABCExceptions", …],       // slugs, same order as index.json
+ "decls": [["Foo.aux", 0, 0, 12], …]}    // [name, kindIdx, projectIdx, declId]
+```
+
+`declId` indexes into that project's shard `decls`; the viewer links a row to
+`p/<slug>/index.html#d<declId>`.
+
+## Page shells
+
+`templates/project.html` is a template with literal `${SLUG}` and `${TITLE}`
+placeholders (Python `string.Template`); the generator instantiates it once
+per project. `index.html`, `decls/index.html` and everything under `assets/`
+are copied verbatim from `static/` and fetch their JSON at runtime.
+URL fragments on project pages: `#d<id>` (select declaration `id`),
+`#cone=<id>` (dependency-cone mode for declaration `id`).

python/lean_pool/exposition/__init__.py

@@ -0,0 +1,7 @@
+"""Static exposition-site generator for the Lean Pool.
+
+Turns the extractor dump (JSONL, one line per human-written declaration)
+into the static site described in ``SCHEMA.md``: per-project data shards
+with layered dependency layouts, a pool-wide index, an all-declarations
+index, and instantiated per-project pages.
+"""

python/lean_pool/exposition/__main__.py

@@ -0,0 +1,56 @@
+"""CLI entry point for the exposition site generator.
+
+Run with ``uv run python -m lean_pool.exposition --dump <jsonl>
+--repo-root <path> --out <dir> [--commit <sha>]`` from ``python/``.
+"""
+
+import logging
+from pathlib import Path
+
+import click
+
+from lean_pool.exposition.generate import generate_site
+
+
+@click.command()
+@click.option(
+    "--dump",
+    "dump_path",
+    type=click.Path(exists=True, dir_okay=False, path_type=Path),
+    required=True,
+    help="Extractor JSONL dump (one JSON object per declaration).",
+)
+@click.option(
+    "--repo-root",
+    "repo_root",
+    type=click.Path(exists=True, file_okay=False, path_type=Path),
+    required=True,
+    help="Repository root containing LeanPool/ sources and projects.yml.",
+)
+@click.option(
+    "--out",
+    "out_dir",
+    type=click.Path(file_okay=False, path_type=Path),
+    required=True,
+    help="Output directory for the generated static site.",
+)
+@click.option(
+    "--commit",
+    default="main",
+    show_default=True,
+    help="Commit SHA recorded in index.json and used for GitHub link metadata.",
+)
+def cli(dump_path: Path, repo_root: Path, out_dir: Path, commit: str) -> None:
+    """Generate the static exposition site from an extractor dump."""
+    logging.basicConfig(level=logging.INFO, format="%(levelname)s %(message)s")
+    summary = generate_site(
+        dump_path=dump_path, repo_root=repo_root, out_dir=out_dir, commit=commit
+    )
+    click.echo(
+        f"Wrote {summary.projects} projects ({summary.decls} declarations, "
+        f"{summary.edges} edges) to {out_dir}"
+    )
+
+
+if __name__ == "__main__":
+    cli()