From d4e0cb22621382d38b90e7b83bf3ae86aacf7632 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 22 Jul 2026 01:20:30 -0700 Subject: [PATCH] Add exposition site: per-project dependency graphs + declaration index MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A static companion site to the API docs, published at /exposition/ on the existing Pages deployment (inspired by leanmachinelearning.org's exposition, rebuilt from scratch for the pool's scale: 58K declarations, 392K edges, 130 projects). - scripts/exposition/Extract.lean (run via `lake env lean --run`, no lakefile changes): walks the compiled pool environment and dumps every human-written declaration with kernel-closure dependency edges (compiler-generated auxiliaries tunnelled through), docstrings, and source ranges as JSONL. - python/lean_pool/exposition: generator computing per-project layered layouts (iterative Tarjan SCC + longest-path layering + barycenter crossing reduction), stats (#nodes, #edges, max/avg depth), statement slices from source, and registry-card metadata (authors, license, area, summary, source links, starred main results with informal statements); emits per-project JSON shards + a static frontend. - Frontend (vanilla JS, no dependencies): canvas graph with left-to-right dependency layers, pan/zoom, search, declaration panel (statement, docstring, source/API-docs links, uses/used-by), per-declaration dependency cones re-layered client-side, hash deep links; an all-declarations viewer (virtual scrolling, sort/filter by kind and project); a landing page with pool-wide stats and a sortable project table. Full run: extraction 6.5 min + generation 11 s locally. - docs.yml: new `exposition` job runs in parallel with the doc-gen4 build, restores the same cache (never writes it), and uploads a ~30 MB artifact the docs job merges into the Pages tree before deploy — fail-soft, so a broken exposition never blocks the docs. Co-Authored-By: Claude Fable 5 --- .github/workflows/docs.yml | 104 ++ .gitignore | 4 + python/lean_pool/exposition/SCHEMA.md | 154 ++ python/lean_pool/exposition/__init__.py | 7 + python/lean_pool/exposition/__main__.py | 56 + python/lean_pool/exposition/generate.py | 441 +++++ python/lean_pool/exposition/layout.py | 163 ++ python/lean_pool/exposition/source_text.py | 335 ++++ .../exposition/static/assets/graph.js | 1423 +++++++++++++++++ .../exposition/static/assets/landing.js | 288 ++++ .../exposition/static/assets/style.css | 637 ++++++++ .../exposition/static/assets/viewer.css | 563 +++++++ .../exposition/static/assets/viewer.js | 335 ++++ .../exposition/static/decls/index.html | 54 + python/lean_pool/exposition/static/index.html | 60 + .../exposition/templates/project.html | 49 + python/tests/test_exposition_generate.py | 391 +++++ python/tests/test_exposition_layout.py | 90 ++ python/tests/test_exposition_source_text.py | 98 ++ scripts/exposition/Extract.lean | 185 +++ 20 files changed, 5437 insertions(+) create mode 100644 python/lean_pool/exposition/SCHEMA.md create mode 100644 python/lean_pool/exposition/__init__.py create mode 100644 python/lean_pool/exposition/__main__.py create mode 100644 python/lean_pool/exposition/generate.py create mode 100644 python/lean_pool/exposition/layout.py create mode 100644 python/lean_pool/exposition/source_text.py create mode 100644 python/lean_pool/exposition/static/assets/graph.js create mode 100644 python/lean_pool/exposition/static/assets/landing.js create mode 100644 python/lean_pool/exposition/static/assets/style.css create mode 100644 python/lean_pool/exposition/static/assets/viewer.css create mode 100644 python/lean_pool/exposition/static/assets/viewer.js create mode 100644 python/lean_pool/exposition/static/decls/index.html create mode 100644 python/lean_pool/exposition/static/index.html create mode 100644 python/lean_pool/exposition/templates/project.html create mode 100644 python/tests/test_exposition_generate.py create mode 100644 python/tests/test_exposition_layout.py create mode 100644 python/tests/test_exposition_source_text.py create mode 100644 scripts/exposition/Extract.lean diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 04114b8cdd..7c1dc4537c 100644 --- a/.github/workflows/docs.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index 8780bc76f1..ade4808901 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,10 @@ /docbuild/.lake .env +# Exposition build outputs (see python/lean_pool/exposition/) +/exposition-dump.jsonl +/exposition-site/ + # Python __pycache__/ *.pyc diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md new file mode 100644 index 0000000000..e96b29a200 --- /dev/null +++ b/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 `/exposition/` next to +the doc-gen4 API docs (which live at `/`). 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": ["", ...], // 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//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/.json +``` + +`` 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//index.html`: exposition root `../..`, +doc-gen4 root `../../..`. doc-gen4 page for a non-private declaration +`Foo.bar` in module `LeanPool.A.B`: `/LeanPool/A/B.html#Foo.bar`. +GitHub source: `https://github.com/Vilin97/lean-pool/blob/main/#L-L`. + +## `data/projects/.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/`, `arxiv` → +`https://arxiv.org/abs/`, `url` as-is, `github_repo` → +`https://github.com/`. + +## `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//index.html#d`. + +## 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` (select declaration `id`), +`#cone=` (dependency-cone mode for declaration `id`). diff --git a/python/lean_pool/exposition/__init__.py b/python/lean_pool/exposition/__init__.py new file mode 100644 index 0000000000..027f4e6da2 --- /dev/null +++ b/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. +""" diff --git a/python/lean_pool/exposition/__main__.py b/python/lean_pool/exposition/__main__.py new file mode 100644 index 0000000000..dd4c835c77 --- /dev/null +++ b/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 +--repo-root --out [--commit ]`` 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() diff --git a/python/lean_pool/exposition/generate.py b/python/lean_pool/exposition/generate.py new file mode 100644 index 0000000000..935e49cf6a --- /dev/null +++ b/python/lean_pool/exposition/generate.py @@ -0,0 +1,441 @@ +"""Orchestrate generation of the static exposition site. + +Reads the extractor JSONL dump, the project registry +(``LeanPool/projects.yml``) and the Lean sources under the repository root, +computes per-project layered layouts and statistics, and writes the site +described in ``SCHEMA.md``: ``data/projects/.json`` shards, +``data/index.json``, ``data/decls.json``, static assets copied verbatim from +``static/``, and one instantiated ``p//index.html`` per project. +""" + +from __future__ import annotations + +import html +import json +import logging +import shutil +import string +from collections import Counter +from dataclasses import dataclass +from datetime import UTC, datetime +from pathlib import Path + +import yaml + +from lean_pool.exposition.layout import compute_layout +from lean_pool.exposition.source_text import SourceFile, statement_slice + +logger = logging.getLogger(__name__) + +PACKAGE_DIRECTORY = Path(__file__).resolve().parent +DEFAULT_STATIC_DIRECTORY = PACKAGE_DIRECTORY / "static" +DEFAULT_TEMPLATES_DIRECTORY = PACKAGE_DIRECTORY / "templates" + + +CARD_SOURCE_FIELDS = ("title", "authors", "doi", "arxiv", "url", "github_repo") + + +@dataclass +class ProjectCard: + """Registry metadata for one project (from ``LeanPool/projects.yml``).""" + + title: str | None + provenance: str | None + card: dict | None = None + main_declarations: list[str] | None = None + main_results: list[dict] | None = None + + +@dataclass +class SiteSummary: + """Totals reported after a site generation run.""" + + projects: int + decls: int + edges: int + + +class SourceCache: + """Read and cache Lean source files by module name (one read per file).""" + + def __init__(self, repo_root: Path) -> None: + """Remember the repository root that module paths resolve against.""" + 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") + if path.is_file(): + text = path.read_text(encoding="utf-8") + self._files[module] = SourceFile.from_text(text) + else: + logger.warning("source file missing for module %s: %s", module, path) + self._files[module] = None + return self._files[module] + + +def read_dump(dump_path: Path) -> list[dict]: + """Parse the extractor JSONL dump into a list of record dicts. + + Records are deduplicated by ``id`` (first occurrence wins): a constant + declared textually in two modules would otherwise become two nodes. + """ + records: list[dict] = [] + seen_ids: set[str] = set() + with Path(dump_path).open(encoding="utf-8") as dump_file: + for line in dump_file: + stripped = line.strip() + if not stripped: + continue + record = json.loads(stripped) + if record["id"] in seen_ids: + logger.warning("duplicate dump record dropped: %s", record["id"]) + continue + seen_ids.add(record["id"]) + records.append(record) + return records + + +def project_for_module(module: str) -> str: + """Return the project slug a module belongs to (second name component).""" + parts = module.split(".") + return parts[1] if len(parts) > 1 else parts[0] + + +def group_records_by_project(records: list[dict]) -> dict[str, list[dict]]: + """Group dump records into per-project lists keyed by slug.""" + grouped: dict[str, list[dict]] = {} + for record in records: + grouped.setdefault(project_for_module(record["m"]), []).append(record) + return grouped + + +def _card_payload(entry: dict) -> dict: + """Build the shard ``card`` object (schema 1.1) from a registry entry.""" + card: dict = {} + for field in ("authors", "license", "branch", "summary", "tags", "msc", "status"): + value = entry.get(field) + if value: + card[field] = value + source = entry.get("source") or {} + source_payload = { + field: source[field] for field in CARD_SOURCE_FIELDS if source.get(field) + } + if source_payload: + card["source"] = source_payload + return card + + +def load_project_cards(projects_yml_path: Path) -> dict[str, ProjectCard]: + """Load registry metadata per project, keyed by entry-module last component.""" + if not projects_yml_path.is_file(): + logger.warning("project registry not found: %s", projects_yml_path) + return {} + data = yaml.safe_load(projects_yml_path.read_text(encoding="utf-8")) or {} + cards: dict[str, ProjectCard] = {} + for entry in data.get("projects", []): + entry_module = entry.get("entry_module") or "" + if not entry_module: + continue + slug = entry_module.split(".")[-1] + main_results = [ + { + "declaration": result.get("declaration"), + "informal": result.get("informal"), + } + for result in entry.get("main_results") or [] + if result.get("declaration") + ] + cards[slug] = ProjectCard( + title=entry.get("title"), + provenance=entry.get("provenance"), + card=_card_payload(entry), + main_declarations=list(entry.get("main_declarations") or []), + main_results=main_results, + ) + return cards + + +def _resolve_main_results(card: ProjectCard | None, nodes: list[dict]) -> list[dict]: + """Resolve card main declarations/results to node ids (schema 1.1). + + Returns one entry per declaration in the union of ``main_declarations`` + and ``main_results``, keeping the informal statement when the card has + one. Resolved ids also flag their node with ``main: true``. + """ + if card is None: + return [] + informal_by_name = { + result["declaration"]: result.get("informal") + for result in card.main_results or [] + } + names: list[str] = list(informal_by_name) + for name in card.main_declarations or []: + if name not in informal_by_name: + names.append(name) + id_by_name: dict[str, int] = {} + for node_id, node in enumerate(nodes): + id_by_name.setdefault(node.get("full", node["name"]), node_id) + id_by_name.setdefault(node["name"], node_id) + resolved = [] + for name in names: + node_id = id_by_name.get(name) + if node_id is None: + logger.warning("main declaration not found in shard: %s", name) + else: + nodes[node_id]["main"] = True + entry: dict = {"id": node_id, "name": name} + informal = informal_by_name.get(name) + if informal: + entry["informal"] = informal + resolved.append(entry) + return resolved + + +def _sorted_records(records: list[dict]) -> list[dict]: + """Order records by (module, start line, name) — the shard id order.""" + return sorted( + records, key=lambda record: (record["m"], record["r"][0], record["n"]) + ) + + +def _remap_dependencies(records: list[dict]) -> list[list[int]]: + """Map dependency ids to shard-local indices, dropping dangling/self refs.""" + index_of = {record["id"]: index for index, record in enumerate(records)} + dependency_lists: list[list[int]] = [] + for index, record in enumerate(records): + indices = { + index_of[dependency] + for dependency in record.get("deps", []) + if dependency in index_of + } + indices.discard(index) + dependency_lists.append(sorted(indices)) + return dependency_lists + + +def _refined_kind_and_statement( + record: dict, source: SourceFile | None +) -> tuple[str, str]: + """Refine the extractor kind and slice the statement from the source.""" + if source is None: + return record["k"], "" + return statement_slice(source, record["r"], record["s"], record["k"]) + + +def _build_node( + record: dict, + kind: str, + statement: str, + module_index: int, + dependencies: list[int], + layer: int, + order: int, +) -> dict: + """Build one shard ``decls`` entry with the schema's key order.""" + node: dict = {"name": record["n"]} + if record["id"] != record["n"]: + node["full"] = record["id"] + node["kind"] = kind + node["module"] = module_index + node["line"] = record["r"][0] + node["endLine"] = record["r"][2] + if "d" in record: + node["doc"] = record["d"] + node["statement"] = statement + if record.get("p"): + node["private"] = True + node["deps"] = dependencies + node["ext"] = record.get("ext", 0) + node["layer"] = layer + node["order"] = order + return node + + +def _kind_counts(kinds: list[str]) -> dict[str, int]: + """Count kinds, ordered by descending count then name for determinism.""" + counts = Counter(kinds) + return dict(sorted(counts.items(), key=lambda item: (-item[1], item[0]))) + + +def build_project_shard( + slug: str, + records: list[dict], + card: ProjectCard | None, + source_cache: SourceCache, +) -> dict: + """Build one ``data/projects/.json`` payload per SCHEMA.md.""" + ordered = _sorted_records(records) + modules = sorted({record["m"] for record in ordered}) + module_indices = {module: index for index, module in enumerate(modules)} + dependency_lists = _remap_dependencies(ordered) + layout = compute_layout(dependency_lists) + nodes = [] + for index, record in enumerate(ordered): + source = source_cache.get(record["m"]) + kind, statement = _refined_kind_and_statement(record, source) + nodes.append( + _build_node( + record, + kind, + statement, + module_indices[record["m"]], + dependency_lists[index], + layout.node_layers[index], + layout.node_orders[index], + ) + ) + node_count = len(nodes) + average = sum(layout.node_layers) / node_count if node_count else 0.0 + stats = { + "nodes": node_count, + "edges": sum(len(dependencies) for dependencies in dependency_lists), + "maxDepth": max(layout.node_layers, default=0), + "avgDepth": round(average, 2), + "kinds": _kind_counts([node["kind"] for node in nodes]), + } + main_results = _resolve_main_results(card, nodes) + return { + "schema": 1, + "project": slug, + "title": card.title if card else None, + "provenance": card.provenance if card else None, + "card": card.card if card and card.card else None, + "mainResults": main_results, + "stats": stats, + "modules": modules, + "layers": layout.layer_sizes, + "decls": nodes, + } + + +def build_index(shards: dict[str, dict], commit: str) -> dict: + """Build the ``data/index.json`` payload (projects sorted by slug).""" + project_rows = [] + total_kinds: Counter[str] = Counter() + for slug in sorted(shards): + shard = shards[slug] + stats = shard["stats"] + total_kinds.update(stats["kinds"]) + card = shard.get("card") or {} + project_rows.append( + { + "slug": slug, + "title": shard["title"], + "provenance": shard["provenance"], + "nodes": stats["nodes"], + "edges": stats["edges"], + "maxDepth": stats["maxDepth"], + "avgDepth": stats["avgDepth"], + "authors": card.get("authors"), + "license": card.get("license"), + "branch": card.get("branch"), + "mainResults": len(shard.get("mainResults") or []), + } + ) + totals = { + "projects": len(project_rows), + "decls": sum(row["nodes"] 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( + sorted(total_kinds.items(), key=lambda item: (-item[1], item[0])) + ), + } + generated = datetime.now(UTC).strftime("%Y-%m-%dT%H:%M:%SZ") + return { + "schema": 1, + "commit": commit, + "generated": generated, + "totals": totals, + "projects": project_rows, + } + + +def build_declaration_index(shards: dict[str, dict], index: dict) -> dict: + """Build the compact ``data/decls.json`` payload for the viewer.""" + 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"]): + rows.append( + [ + node["name"], + kind_indices[node["kind"]], + project_position, + declaration_id, + ] + ) + return {"schema": 1, "kinds": kinds, "projects": slugs, "decls": rows} + + +def _write_json(path: Path, payload: dict) -> None: + """Write compact JSON (preserving insertion key order) to ``path``.""" + path.parent.mkdir(parents=True, exist_ok=True) + text = json.dumps(payload, separators=(",", ":"), ensure_ascii=False) + path.write_text(text, encoding="utf-8") + + +def _write_project_pages( + out_dir: Path, shards: dict[str, dict], template_path: Path +) -> None: + """Instantiate ``templates/project.html`` once per project.""" + template = string.Template(template_path.read_text(encoding="utf-8")) + for slug, shard in shards.items(): + title = shard["title"] or slug + page = template.safe_substitute(SLUG=slug, TITLE=html.escape(title)) + page_directory = out_dir / "p" / slug + page_directory.mkdir(parents=True, exist_ok=True) + (page_directory / "index.html").write_text(page, encoding="utf-8") + + +def generate_site( + dump_path: Path, + repo_root: Path, + out_dir: Path, + commit: str = "main", + static_dir: Path | None = None, + templates_dir: Path | None = None, +) -> SiteSummary: + """Generate the whole static site; return the run's totals. + + ``static_dir`` and ``templates_dir`` default to the package's ``static/`` + and ``templates/`` directories; tests inject fakes through them. + """ + static_directory = Path(static_dir) if static_dir else DEFAULT_STATIC_DIRECTORY + templates_directory = ( + Path(templates_dir) if templates_dir else DEFAULT_TEMPLATES_DIRECTORY + ) + template_path = templates_directory / "project.html" + if not static_directory.is_dir(): + raise FileNotFoundError(f"static asset directory not found: {static_directory}") + if not template_path.is_file(): + raise FileNotFoundError(f"project page template not found: {template_path}") + grouped = group_records_by_project(read_dump(dump_path)) + cards = load_project_cards(Path(repo_root) / "LeanPool" / "projects.yml") + source_cache = SourceCache(Path(repo_root)) + shards = { + slug: build_project_shard(slug, records, cards.get(slug), source_cache) + for slug, records in grouped.items() + } + index = build_index(shards, commit) + out_directory = Path(out_dir) + out_directory.mkdir(parents=True, exist_ok=True) + shutil.copytree(static_directory, out_directory, dirs_exist_ok=True) + for slug, shard in shards.items(): + _write_json(out_directory / "data" / "projects" / f"{slug}.json", shard) + _write_json(out_directory / "data" / "index.json", index) + _write_json( + out_directory / "data" / "decls.json", + build_declaration_index(shards, index), + ) + _write_project_pages(out_directory, shards, template_path) + return SiteSummary( + projects=index["totals"]["projects"], + decls=index["totals"]["decls"], + edges=index["totals"]["edges"], + ) diff --git a/python/lean_pool/exposition/layout.py b/python/lean_pool/exposition/layout.py new file mode 100644 index 0000000000..433290956c --- /dev/null +++ b/python/lean_pool/exposition/layout.py @@ -0,0 +1,163 @@ +"""Layered layout for per-project dependency graphs. + +Pure Python, no third-party dependencies. The pipeline is: + +1. iterative Tarjan strongly-connected components (the largest project has + ~7.7K nodes, so no recursion), +2. condensation + longest-path layering: layer 0 = no intra-project + dependencies; every member of an SCC shares a layer; otherwise + ``layer = 1 + max(layer(dep))`` over dependencies outside the SCC, +3. within-layer ordering by barycenter crossing reduction: the initial + order is ascending node id (callers assign ids in ``(module, line)`` + order), then four alternating forward/backward sweeps sort each layer by + average neighbor position with a deterministic tie-break on the initial + order. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +BARYCENTER_SWEEPS = 4 + + +@dataclass +class Layout: + """Computed positions: per-node layer and order, plus per-layer sizes.""" + + node_layers: list[int] + node_orders: list[int] + layer_sizes: list[int] + + +def compute_layout(dependencies: list[list[int]]) -> Layout: + """Return the layered layout for a dependency graph. + + ``dependencies[n]`` lists the node ids that node ``n`` depends on. Node + ids double as the initial within-layer order, so callers must number + nodes in ``(module, line)`` order. + """ + node_layers = _longest_path_layers(dependencies) + node_orders, layer_sizes = _crossing_reduced_orders(dependencies, node_layers) + return Layout( + node_layers=node_layers, node_orders=node_orders, layer_sizes=layer_sizes + ) + + +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 + after every component it can reach, so components appear in an order + where all dependencies of a component precede it. + """ + node_count = len(adjacency) + visit_index = [-1] * node_count + low_link = [0] * node_count + on_stack = [False] * node_count + stack: list[int] = [] + components: list[list[int]] = [] + counter = 0 + for root in range(node_count): + if visit_index[root] != -1: + continue + work: list[tuple[int, int]] = [(root, 0)] + while work: + node, edge_index = work[-1] + if edge_index == 0: + visit_index[node] = low_link[node] = counter + counter += 1 + stack.append(node) + on_stack[node] = True + descended = False + for position in range(edge_index, len(adjacency[node])): + neighbor = adjacency[node][position] + if visit_index[neighbor] == -1: + work[-1] = (node, position + 1) + work.append((neighbor, 0)) + descended = True + break + if on_stack[neighbor]: + low_link[node] = min(low_link[node], visit_index[neighbor]) + if descended: + continue + work.pop() + if work: + parent = work[-1][0] + low_link[parent] = min(low_link[parent], low_link[node]) + if low_link[node] == visit_index[node]: + component: list[int] = [] + while True: + member = stack.pop() + on_stack[member] = False + component.append(member) + if member == node: + break + components.append(component) + return components + + +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) + component_of = [0] * len(dependencies) + for component_index, members in enumerate(components): + for node in members: + component_of[node] = component_index + component_layers = [0] * len(components) + for component_index, members in enumerate(components): + layer = 0 + for node in members: + for dependency in dependencies[node]: + if component_of[dependency] != component_index: + dependency_layer = component_layers[component_of[dependency]] + layer = max(layer, dependency_layer + 1) + component_layers[component_index] = layer + return [component_layers[component_of[node]] for node in range(len(dependencies))] + + +def _reorder_layer( + members: list[int], neighbor_lists: list[list[int]], positions: list[int] +) -> None: + """Sort one layer by average neighbor position; ties keep initial order. + + Nodes without neighbors keep their current position as barycenter, and + the node id (== initial order) breaks ties deterministically. + """ + + def sort_key(node: int) -> tuple[float, int]: + neighbors = neighbor_lists[node] + if not neighbors: + return (float(positions[node]), node) + barycenter = sum(positions[neighbor] for neighbor in neighbors) + return (barycenter / len(neighbors), node) + + members.sort(key=sort_key) + for position, node in enumerate(members): + positions[node] = position + + +def _crossing_reduced_orders( + dependencies: list[list[int]], node_layers: list[int] +) -> tuple[list[int], list[int]]: + """Return per-node within-layer orders and per-layer sizes.""" + layer_count = max(node_layers, default=-1) + 1 + layers: list[list[int]] = [[] for _ in range(layer_count)] + for node in range(len(node_layers)): # ascending id = initial order + layers[node_layers[node]].append(node) + dependents: list[list[int]] = [[] for _ in dependencies] + for node, node_dependencies in enumerate(dependencies): + for dependency in node_dependencies: + dependents[dependency].append(node) + positions = [0] * len(node_layers) + for members in layers: + for position, node in enumerate(members): + positions[node] = position + for sweep in range(BARYCENTER_SWEEPS): + if sweep % 2 == 0: # forward: order each layer by its dependencies + for members in layers[1:]: + _reorder_layer(members, dependencies, positions) + else: # backward: order each layer by its dependents + for members in reversed(layers[:-1]): + _reorder_layer(members, dependents, positions) + return positions, [len(members) for members in layers] diff --git a/python/lean_pool/exposition/source_text.py b/python/lean_pool/exposition/source_text.py new file mode 100644 index 0000000000..0437154521 --- /dev/null +++ b/python/lean_pool/exposition/source_text.py @@ -0,0 +1,335 @@ +"""Slice declaration keywords and statement text out of Lean source files. + +The lexical helpers here (``code_view``, ``_read_token``, ``_strip_prefixes`` +and the statement/body boundary scanner) are adapted from +``scripts/proof-profile/statements.py``. They are copied rather than imported +because that script is fetched standalone from ``origin/main`` in CI and +lives in a different tree; see its docstrings for the original rationale. + +The entry point is :func:`statement_slice`: given a pre-parsed +:class:`SourceFile` and a declaration's source range plus name selection, it +returns the refined declaration keyword (``lemma`` vs ``theorem``, ``abbrev`` +vs ``def``, ...) and the statement text — the original source from the +keyword up to the top-level ``:=`` / ``where`` / ``|``-arm boundary. +""" + +from __future__ import annotations + +import re +from collections.abc import Sequence +from dataclasses import dataclass + +# Keywords whose presence in the source refines the extractor's coarse kind. +DECLARATION_KEYWORDS = frozenset( + { + "theorem", + "lemma", + "def", + "abbrev", + "instance", + "structure", + "class", + "inductive", + "opaque", + "axiom", + } +) + +# Modifiers that may sit between the range start and the declaration keyword +# (from statements.py; ``@[...]`` attributes and ``... in`` prefixes are +# handled structurally, not through this set). +MODIFIERS = { + "private", + "protected", + "noncomputable", + "unsafe", + "partial", + "nonrec", + "scoped", + "local", + "mutual", +} + +OPEN_BRACKETS = "([{⟨⦃" +CLOSE_BRACKETS = ")]}⟩⦄" + +# Characters that terminate the name token following a declaration keyword. +NAME_STOP = set(" \t\r\n({[⦃⟨:=") + +# Maximum statement length emitted into the site data (schema: <= 1200). +STATEMENT_CHARACTER_LIMIT = 1200 + +_WHERE_RE = re.compile(r"(? str: + """Return ``text`` with comments and string literals blanked to spaces. + + Copied from ``scripts/proof-profile/statements.py``. Length and newline + positions are preserved so indices computed on the result line up with + the original source. Block comments (``/- -/``) nest, which also covers + doc comments (``/-- -/``) and module docs (``/-! -/``). + """ + out: list[str] = [] + i, n = 0, len(text) + normal, line, block, string_literal = 0, 1, 2, 3 + state = normal + block_depth = 0 + while i < n: + c = text[i] + two = text[i : i + 2] + if state == normal: + if two == "--": + out.append(" ") + i += 2 + state = line + continue + if two == "/-": + out.append(" ") + i += 2 + state = block + block_depth = 1 + continue + if c == '"': + out.append(" ") + i += 1 + state = string_literal + continue + out.append(c) + i += 1 + elif state == line: + if c == "\n": + out.append("\n") + state = normal + else: + out.append(" ") + i += 1 + elif state == block: + if two == "/-": + out.append(" ") + i += 2 + block_depth += 1 + continue + if two == "-/": + out.append(" ") + i += 2 + block_depth -= 1 + if block_depth == 0: + state = normal + continue + out.append("\n" if c == "\n" else " ") + i += 1 + else: # string literal + if c == "\\": + out.append(" " if i + 1 < n else " ") + i += 2 + continue + if c == '"': + out.append(" ") + state = normal + i += 1 + continue + out.append("\n" if c == "\n" else " ") + i += 1 + return "".join(out) + + +def _read_token(code: str, pos: int, end: int) -> str: + """Read one token starting at ``pos`` (from statements.py).""" + j = pos + while j < end and code[j] not in NAME_STOP and code[j] != "@": + j += 1 + return code[pos:j] + + +def _strip_prefixes(code: str, start: int, end: int) -> int: + """Skip attributes / modifiers / ``... in`` prefixes; return keyword index. + + Copied from ``scripts/proof-profile/statements.py``. Doc comments have + already been blanked by :func:`code_view`, so leading whitespace covers + them too. + """ + pos = start + while pos < end: + while pos < end and code[pos] in " \t\r\n": + pos += 1 + if pos >= end: + break + if code[pos] == "@" and pos + 1 < end and code[pos + 1] == "[": + depth = 0 + while pos < end: + if code[pos] == "[": + depth += 1 + elif code[pos] == "]": + depth -= 1 + if depth == 0: + pos += 1 + break + pos += 1 + continue + token = _read_token(code, pos, end) + if token in MODIFIERS: + pos += len(token) + continue + if token in ("set_option", "open"): + match = _IN_RE.search(code, pos, end) + if match: + pos = match.end() + continue + break + return pos + + +def _line_prefix(code: str, pos: int) -> str: + """Return the text on ``pos``'s line, up to ``pos`` (from statements.py).""" + start = code.rfind("\n", 0, pos) + 1 + return code[start:pos] + + +def _find_boundary( + code: str, start: int, end: int, bar_always_ends: bool = False +) -> int: + """Return the index in ``[start, end)`` where the declaration body begins. + + Adapted from ``scripts/proof-profile/statements.py``. Bracket depth is + tracked locally. The body begins at the first top-level ``:=`` or + ``where``, or — for equation-compiler declarations — at the first + line-leading ``|`` arm (recognised by a following top-level ``=>``). + When ``bar_always_ends`` is set (inductive-like declarations, whose + constructor arms carry no ``=>``), any line-leading top-level ``|`` ends + the statement. Returns ``end`` if no boundary is found. + """ + b_assign = b_where = b_bar = None + seen_bars: list[int] = [] + depth = 0 + i = start + while i < end: + c = code[i] + if depth == 0: + if b_assign is None and code[i : i + 2] == ":=": + b_assign = i + elif ( + code[i : i + 2] == "=>" + and seen_bars + and b_bar is None + and b_assign is None + and b_where is None + ): + # A line-leading `|` is an equation-compiler arm only if its + # `=>` arrives before any top-level `:=`/`where` (keeps an + # absolute-value bar in a type from being read as an arm). + b_bar = seen_bars[0] + elif b_where is None and _WHERE_RE.match(code, i): + b_where = i + if c == "|" and _line_prefix(code, i).strip() == "": + seen_bars.append(i) + if bar_always_ends and b_bar is None: + b_bar = i + if c in OPEN_BRACKETS: + depth += 1 + elif c in CLOSE_BRACKETS: + depth = max(0, depth - 1) + i += 1 + candidates = [b for b in (b_assign, b_where, b_bar) if b is not None] + return min(candidates) if candidates else end + + +@dataclass +class SourceFile: + """One Lean source file, read once and pre-processed for slicing.""" + + text: str + code: str + line_offsets: list[int] + + @classmethod + def from_text(cls, text: str) -> SourceFile: + """Build a :class:`SourceFile` (blanked view + line offsets) from text.""" + offsets = [0] + for index, character in enumerate(text): + if character == "\n": + offsets.append(index + 1) + return cls(text=text, code=code_view(text), line_offsets=offsets) + + def offset(self, line: int, column: int) -> int: + """Return the character offset of 1-based ``line`` / 0-based ``column``.""" + if line < 1: + return 0 + if line > len(self.line_offsets): + return len(self.text) + return min(self.line_offsets[line - 1] + max(column, 0), len(self.text)) + + +def _next_token(code: str, pos: int, end: int) -> str: + """Return the next token at or after ``pos``, skipping whitespace.""" + while pos < end and code[pos] in " \t\r\n": + pos += 1 + return _read_token(code, pos, end) + + +def _boundary_scan_start( + source: SourceFile, + keyword_position: int, + keyword_length: int, + selection: Sequence[int], + end: int, +) -> int: + """Return where the body-boundary scan starts: after the name token. + + The extractor's selection points at the declaration's name token; scanning + from past it mirrors ``statements.py`` (which scans from after the parsed + name). When the selection is unusable, scan from after the keyword. + """ + selection_offset = source.offset(selection[0], selection[1]) + after_keyword = keyword_position + keyword_length + if selection_offset < after_keyword or selection_offset >= end: + return after_keyword + name_end = selection_offset + while name_end < end and source.code[name_end] not in NAME_STOP: + name_end += 1 + return name_end + + +def statement_slice( + source: SourceFile, + declaration_range: Sequence[int], + selection: Sequence[int], + fallback_kind: str, +) -> tuple[str, str]: + """Return ``(kind, statement)`` for one declaration. + + ``declaration_range`` is ``[startLine, startCol, endLine, endCol]`` with + 1-based lines; ``selection`` is the ``[line, col]`` of the name token. + ``kind`` is the source keyword when it is a known declaration keyword + (``class inductive`` reports ``class``), else ``fallback_kind``. The + statement is original source from the keyword to the body boundary, + trimmed only at the edges and capped at 1200 characters. + """ + start = source.offset(declaration_range[0], declaration_range[1]) + end = source.offset(declaration_range[2], declaration_range[3]) + if end <= start: + return fallback_kind, "" + code = source.code + keyword_position = _strip_prefixes(code, start, end) + keyword = _read_token(code, keyword_position, end) + kind = keyword if keyword in DECLARATION_KEYWORDS else fallback_kind + if keyword not in DECLARATION_KEYWORDS: + # Attribute/deriving-generated declarations (`@[simps]`, `deriving + # DecidableEq`, `to_additive`, ...) point their range at a mid-line + # token; slicing from there yields a meaningless fragment. + line_start = source.line_offsets[declaration_range[0] - 1] + if source.text[line_start:start].strip(): + return fallback_kind, "" + inductive_like = keyword == "inductive" or ( + keyword == "class" + and _next_token(code, keyword_position + len(keyword), end) == "inductive" + ) + scan_start = _boundary_scan_start( + source, keyword_position, len(keyword), selection, end + ) + boundary = _find_boundary(code, scan_start, end, bar_always_ends=inductive_like) + statement = source.text[keyword_position:boundary].strip() + if len(statement) > STATEMENT_CHARACTER_LIMIT: + statement = statement[: STATEMENT_CHARACTER_LIMIT - 1].rstrip() + "…" + return kind, statement diff --git a/python/lean_pool/exposition/static/assets/graph.js b/python/lean_pool/exposition/static/assets/graph.js new file mode 100644 index 0000000000..9d3e636f19 --- /dev/null +++ b/python/lean_pool/exposition/static/assets/graph.js @@ -0,0 +1,1423 @@ +/* Lean Pool exposition — per-project dependency-graph viewer. + Vanilla JS, Canvas 2D. Loaded by p//index.html, which carries the + project slug in . Fetches ../../data/projects/.json. + Hash routing: #d selects declaration , #cone= shows its + dependency cone. */ +(() => { + 'use strict'; + + // ----- constants --------------------------------------------------------- + + const LAYER_X = 170; // x = layer * LAYER_X + const ROW_Y = 26; // y = (order - (layerSize - 1) / 2) * ROW_Y + const NODE_SIZE = 8; // node glyph, graph units + const GRID_CELL = 64; // hit-test grid cell, graph units + const CHEAP_EDGE_THRESHOLD = 8000; // straight edges while panning above this + const DEP_LIST_INITIAL = 100; // panel Uses/Used-by rows before "Show all" + const MAX_LABEL_PX = 400; // widen the left label cull by one label width + const KINDS = ['theorem', 'lemma', 'def', 'abbrev', 'instance', 'structure', + 'class', 'inductive', 'axiom', 'opaque']; + const GITHUB_BLOB = 'https://github.com/Vilin97/lean-pool/blob/main/'; + const MONO = 'ui-monospace, SFMono-Regular, Menlo, Consolas, monospace'; + + // ----- DOM ---------------------------------------------------------------- + + const byId = (id) => document.getElementById(id); + const canvas = byId('graph-canvas'); + const viewportEl = byId('graph-viewport'); + if (!canvas || !viewportEl) return; + const ctx = canvas.getContext('2d'); + const tooltipEl = byId('graph-tooltip'); + const messageEl = byId('graph-message'); + const panelEl = byId('decl-panel'); + const panelBodyEl = byId('panel-body'); + const panelCloseEl = byId('panel-close'); + const searchInputEl = byId('search-input'); + const searchCountEl = byId('search-count'); + const fitButtonEl = byId('fit-button'); + const breadcrumbEl = byId('cone-breadcrumb'); + const coneBackEl = byId('cone-back'); + const coneLabelEl = byId('cone-label'); + const titleEl = byId('project-title'); + const provenanceEl = byId('provenance-badge'); + const statsEl = byId('info-stats'); + const legendEl = byId('kind-legend'); + const slug = document.body.dataset.slug || ''; + + function elWith(tag, className, text) { + const node = document.createElement(tag); + if (className) node.className = className; + if (text !== null && text !== undefined) node.textContent = text; + return node; + } + + // ----- theme -------------------------------------------------------------- + + let theme = null; + let edgeColors = ['', '', '']; // [dim, normal, accent] + let labelColor = ''; + + function hexToRgb(hex) { + let h = (hex || '').trim(); + if (h.startsWith('#')) h = h.slice(1); + if (h.length === 3) h = h[0] + h[0] + h[1] + h[1] + h[2] + h[2]; + const num = parseInt(h, 16); + if (h.length !== 6 || Number.isNaN(num)) return [128, 128, 128]; + return [(num >> 16) & 255, (num >> 8) & 255, num & 255]; + } + + function mixRgb(a, b, t) { + return [ + Math.round(a[0] + (b[0] - a[0]) * t), + Math.round(a[1] + (b[1] - a[1]) * t), + Math.round(a[2] + (b[2] - a[2]) * t), + ]; + } + + function rgbaStr(rgb, alpha) { + return 'rgba(' + rgb[0] + ',' + rgb[1] + ',' + rgb[2] + ',' + alpha + ')'; + } + + function readTheme() { + const rootStyle = getComputedStyle(document.documentElement); + const token = (name, fallback) => + rootStyle.getPropertyValue(name).trim() || fallback; + const kinds = {}; + for (const k of KINDS) kinds[k] = token('--kind-' + k, '#57606a'); + theme = { + fg: token('--fg', '#1c1c1c'), + muted: token('--muted', '#6b6960'), + border: token('--border', '#e3ded4'), + accent: token('--accent', '#1a6baa'), + star: token('--star', '#bf8700'), + kinds, + }; + } + + function updateDerivedColors() { + const edgeRgb = mixRgb(hexToRgb(theme.border), hexToRgb(theme.muted), 0.5); + const alpha = view ? view.edgeAlpha : 0.4; + edgeColors = [ + rgbaStr(edgeRgb, Math.max(0.02, alpha * 0.15)), + rgbaStr(edgeRgb, alpha), + rgbaStr(hexToRgb(theme.accent), 0.85), + ]; + labelColor = rgbaStr(hexToRgb(theme.fg), 0.85); + } + + // ----- model state -------------------------------------------------------- + + let decls = []; + let modules = []; + let N = 0; + let names = []; + let lowerNames = []; + let nodeKinds = []; + let deps = []; // Int32Array per node: nodes this one uses + let rev = []; // Int32Array per node: nodes using this one + + let matchFlags = null; // Uint8Array(N), search matches + let neighborFlags = null; // Uint8Array(N), selected + 1-step neighborhood + let matchTotal = 0; + let firstMatch = -1; + let searchQuery = ''; + let mainIds = []; // node ids flagged as main results (card metadata) + let mainInformal = {}; // node id -> informal statement from the card + + let fullView = null; + let coneView = null; + let coneRoot = -1; + let view = null; + + let selected = -1; // shard-local declaration id + let hoverId = -1; // shard-local declaration id + + const camera = { scale: 1, tx: 0, ty: 0, minScale: 0.05, maxScale: 8 }; + let dirty = true; + let interacting = false; + let autoFit = true; // refit on resize until the user pans/zooms + let wheelTimer = 0; + let cssW = 1; + let cssH = 1; + let dpr = 1; + + // ----- views (full graph / dependency cone) ------------------------------- + + function gridKey(cx, cy) { + return cx * 262144 + cy; + } + + function buildGrid(xs, ys, n) { + const map = new Map(); + for (let i = 0; i < n; i++) { + const key = gridKey(Math.floor(xs[i] / GRID_CELL), + Math.floor(ys[i] / GRID_CELL)); + let cell = map.get(key); + if (!cell) { + cell = []; + map.set(key, cell); + } + cell.push(i); + } + return map; + } + + // A view is a renderable (sub)graph: node positions, view-local edges, a + // hit-test grid and kind groupings. All arrays are allocated once here, + // never per frame. + function buildView(ids, layerOf, orderOf, layerSizes) { + const n = ids.length; + const xs = new Float32Array(n); + const ys = new Float32Array(n); + let minX = 0; + let maxX = 0; + let minY = 0; + let maxY = 0; + for (let i = 0; i < n; i++) { + const layer = layerOf[i]; + const size = layerSizes[layer] || 1; + const x = layer * LAYER_X; + const y = (orderOf[i] - (size - 1) / 2) * ROW_Y; + xs[i] = x; + ys[i] = y; + if (i === 0) { + minX = maxX = x; + minY = maxY = y; + } else { + if (x < minX) minX = x; + if (x > maxX) maxX = x; + if (y < minY) minY = y; + if (y > maxY) maxY = y; + } + } + const toView = new Int32Array(N).fill(-1); + for (let i = 0; i < n; i++) toView[ids[i]] = i; + let edgeCount = 0; + for (let i = 0; i < n; i++) { + const list = deps[ids[i]]; + for (let j = 0; j < list.length; j++) { + const s = toView[list[j]]; + if (s >= 0 && s !== i) edgeCount++; + } + } + const edgeSrc = new Int32Array(edgeCount); + const edgeDst = new Int32Array(edgeCount); + let e = 0; + for (let i = 0; i < n; i++) { + const list = deps[ids[i]]; + for (let j = 0; j < list.length; j++) { + const s = toView[list[j]]; + if (s >= 0 && s !== i) { + edgeSrc[e] = s; // dependency on the left… + edgeDst[e] = i; // …drawn toward the declaration using it + e++; + } + } + } + const groupIndex = new Map(); + const groupLists = []; + for (let i = 0; i < n; i++) { + const kind = nodeKinds[ids[i]]; + let gi = groupIndex.get(kind); + if (gi === undefined) { + gi = groupLists.length; + groupIndex.set(kind, gi); + groupLists.push({ kind, list: [] }); + } + groupLists[gi].list.push(i); + } + const kindGroups = groupLists.map((g) => ({ + kind: g.kind, + indices: Int32Array.from(g.list), + })); + return { + ids, + n, + xs, + ys, + toView, + edgeSrc, + edgeDst, + kindGroups, + grid: buildGrid(xs, ys, n), + bounds: { minX, maxX, minY, maxY }, + edgeAlpha: Math.max(0.05, Math.min(0.55, 1500 / Math.max(1, edgeCount))), + }; + } + + function pickNode(gx, gy, radius) { + if (!view || view.n === 0) return -1; + const cx0 = Math.floor((gx - radius) / GRID_CELL); + const cx1 = Math.floor((gx + radius) / GRID_CELL); + const cy0 = Math.floor((gy - radius) / GRID_CELL); + const cy1 = Math.floor((gy + radius) / GRID_CELL); + let best = -1; + let bestD = radius * radius; + for (let cx = cx0; cx <= cx1; cx++) { + for (let cy = cy0; cy <= cy1; cy++) { + const cell = view.grid.get(gridKey(cx, cy)); + if (!cell) continue; + for (let j = 0; j < cell.length; j++) { + const i = cell[j]; + const dx = view.xs[i] - gx; + const dy = view.ys[i] - gy; + const d = dx * dx + dy * dy; + if (d <= bestD) { + bestD = d; + best = i; + } + } + } + } + return best; + } + + // ----- camera --------------------------------------------------------------- + + function toGraphX(sx) { + return (sx - camera.tx) / camera.scale; + } + + function toGraphY(sy) { + return (sy - camera.ty) / camera.scale; + } + + function availableWidth() { + return panelEl && !panelEl.hidden + ? Math.max(cssW - 400, cssW * 0.4) + : cssW; + } + + function fitCamera() { + if (!view || view.n === 0) return; + const pad = 60; + const labelRoom = 150; // labels extend to the right of nodes + const availW = availableWidth(); + const b = view.bounds; + const bw = b.maxX - b.minX + pad * 2 + labelRoom; + const bh = b.maxY - b.minY + pad * 2; + let s = Math.min(availW / bw, cssH / bh); + if (!Number.isFinite(s) || s <= 0) s = 1; + s = Math.min(s, 1.2); + camera.minScale = Math.min(0.05, s * 0.8); + camera.scale = s; + camera.tx = availW / 2 - ((b.minX + b.maxX) / 2 + labelRoom / 4) * s; + camera.ty = cssH / 2 - ((b.minY + b.maxY) / 2) * s; + autoFit = true; + dirty = true; + } + + function panTo(id) { + const vi = view ? view.toView[id] : -1; + if (vi < 0) return; + autoFit = false; + if (camera.scale < 0.75) camera.scale = Math.min(1, camera.maxScale); + camera.tx = availableWidth() / 2 - view.xs[vi] * camera.scale; + camera.ty = cssH / 2 - view.ys[vi] * camera.scale; + dirty = true; + } + + function zoomAt(mx, my, factor) { + const old = camera.scale; + const next = Math.min(camera.maxScale, + Math.max(camera.minScale, old * factor)); + if (next === old) return; + camera.tx = mx - (mx - camera.tx) * (next / old); + camera.ty = my - (my - camera.ty) * (next / old); + camera.scale = next; + autoFit = false; + dirty = true; + } + + // ----- highlight state ------------------------------------------------------ + + // 0 = nothing dimmed, 1 = search dimming, 2 = selection-neighborhood dimming. + function dimModeNow() { + if (searchQuery) return 1; + if (selected >= 0) return 2; + return 0; + } + + function isLit(id, mode) { + if (mode === 1) return matchFlags[id] === 1 || id === selected; + if (mode === 2) return neighborFlags[id] === 1; + return true; + } + + function edgeClass(a, b, mode) { + if (selected >= 0 && (a === selected || b === selected)) return 2; + if (mode === 0) return 1; + return isLit(a, mode) && isLit(b, mode) ? 1 : 0; + } + + function recomputeNeighborhood() { + neighborFlags.fill(0); + if (selected < 0) return; + neighborFlags[selected] = 1; + const down = deps[selected]; + for (let j = 0; j < down.length; j++) neighborFlags[down[j]] = 1; + const up = rev[selected]; + for (let j = 0; j < up.length; j++) neighborFlags[up[j]] = 1; + } + + // ----- rendering ------------------------------------------------------------ + + function render() { + ctx.setTransform(dpr, 0, 0, dpr, 0, 0); + ctx.clearRect(0, 0, cssW, cssH); + if (!view || view.n === 0) return; + const margin = 80; + const gx0 = toGraphX(-margin); + const gx1 = toGraphX(cssW + margin); + const gy0 = toGraphY(-margin); + const gy1 = toGraphY(cssH + margin); + const mode = dimModeNow(); + drawEdges(mode, gx0, gy0, gx1, gy1); + drawNodes(mode, gx0, gy0, gx1, gy1); + drawRings(); + drawLabels(mode, gx0, gy0, gx1, gy1); + } + + function drawEdges(mode, gx0, gy0, gx1, gy1) { + const v = view; + const total = v.edgeSrc.length; + if (total === 0) return; + const cheap = interacting && total > CHEAP_EDGE_THRESHOLD; + const sc = camera.scale; + const tx = camera.tx; + const ty = camera.ty; + const first = mode === 0 ? 1 : 0; + const last = mode === 0 ? 1 : 2; + for (let cls = first; cls <= last; cls++) { + ctx.strokeStyle = edgeColors[cls]; + ctx.lineWidth = cls === 2 ? 1.6 : 1; + ctx.beginPath(); + let any = false; + for (let e = 0; e < total; e++) { + const a = v.edgeSrc[e]; + const b = v.edgeDst[e]; + const x1 = v.xs[a]; + const y1 = v.ys[a]; + const x2 = v.xs[b]; + const y2 = v.ys[b]; + if ((x1 < gx0 && x2 < gx0) || (x1 > gx1 && x2 > gx1) + || (y1 < gy0 && y2 < gy0) || (y1 > gy1 && y2 > gy1)) continue; + if (edgeClass(v.ids[a], v.ids[b], mode) !== cls) continue; + const sx1 = x1 * sc + tx; + const sy1 = y1 * sc + ty; + const sx2 = x2 * sc + tx; + const sy2 = y2 * sc + ty; + ctx.moveTo(sx1, sy1); + if (cheap) ctx.lineTo(sx2, sy2); + else ctx.quadraticCurveTo((sx1 + sx2) / 2, sy1, sx2, sy2); + any = true; + } + if (any) ctx.stroke(); + } + } + + function nodeScreenSize() { + return Math.max(2.5, Math.min(16, NODE_SIZE * camera.scale)); + } + + function drawNodes(mode, gx0, gy0, gx1, gy1) { + const v = view; + const sc = camera.scale; + const tx = camera.tx; + const ty = camera.ty; + const size = nodeScreenSize(); + const half = size / 2; + const useRound = size >= 6 && typeof ctx.roundRect === 'function'; + const corner = size / 4; + for (let pass = 0; pass < 2; pass++) { + if (pass === 0 && mode === 0) continue; // no dim pass needed + const wantDim = pass === 0; + ctx.globalAlpha = wantDim ? 0.15 : 1; + for (let g = 0; g < v.kindGroups.length; g++) { + const group = v.kindGroups[g]; + ctx.fillStyle = theme.kinds[group.kind] || theme.muted; + const list = group.indices; + for (let j = 0; j < list.length; j++) { + const i = list[j]; + const x = v.xs[i]; + const y = v.ys[i]; + if (x < gx0 || x > gx1 || y < gy0 || y > gy1) continue; + const lit = mode === 0 || isLit(v.ids[i], mode); + if (lit === wantDim) continue; + const sx = x * sc + tx - half; + const sy = y * sc + ty - half; + if (useRound) { + ctx.beginPath(); + ctx.roundRect(sx, sy, size, size, corner); + ctx.fill(); + } else { + ctx.fillRect(sx, sy, size, size); + } + } + } + } + ctx.globalAlpha = 1; + } + + function drawOneRing(id, color, grow, width) { + const vi = view.toView[id]; + if (vi < 0) return; + const sc = camera.scale; + const sx = view.xs[vi] * sc + camera.tx; + const sy = view.ys[vi] * sc + camera.ty; + const r = nodeScreenSize() / 2 + grow; + ctx.strokeStyle = color; + ctx.lineWidth = width; + ctx.beginPath(); + if (typeof ctx.roundRect === 'function') { + ctx.roundRect(sx - r, sy - r, r * 2, r * 2, r / 2); + } else { + ctx.rect(sx - r, sy - r, r * 2, r * 2); + } + ctx.stroke(); + } + + function drawRings() { + ctx.globalAlpha = 0.9; + for (let i = 0; i < mainIds.length; i++) { + if (mainIds[i] !== selected) { + drawOneRing(mainIds[i], theme.star, 2.5, 1.5); + } + } + ctx.globalAlpha = 1; + if (view === coneView && coneRoot >= 0) { + drawOneRing(coneRoot, theme.accent, 6, 2); + } + if (selected >= 0) drawOneRing(selected, theme.accent, 3, 1.5); + if (hoverId >= 0 && hoverId !== selected) { + drawOneRing(hoverId, theme.muted, 3, 1); + } + } + + function drawLabels(mode, gx0, gy0, gx1, gy1) { + const v = view; + const effective = 10 * camera.scale; + if (effective < 9) return; + if (interacting && v.edgeSrc.length > CHEAP_EDGE_THRESHOLD) return; + const sc = camera.scale; + const tx = camera.tx; + const ty = camera.ty; + const offset = nodeScreenSize() / 2 + 5; + ctx.font = Math.min(13, effective) + 'px ' + MONO; + ctx.textBaseline = 'middle'; + ctx.textAlign = 'left'; + ctx.fillStyle = labelColor; + // Labels extend right of their node, so a node just left of the viewport + // may still own visible text: widen only the left cull bound. + const labelGx0 = gx0 - MAX_LABEL_PX / sc; + for (let i = 0; i < v.n; i++) { + const x = v.xs[i]; + const y = v.ys[i]; + if (x < labelGx0 || x > gx1 || y < gy0 || y > gy1) continue; + if (mode !== 0 && !isLit(v.ids[i], mode)) continue; + ctx.fillText(names[v.ids[i]], x * sc + tx + offset, y * sc + ty); + } + } + + let lastFrameAt = 0; + + function frame() { + lastFrameAt = Date.now(); + if (dirty) { + dirty = false; + render(); + } + requestAnimationFrame(frame); + } + + // Fallback for contexts where requestAnimationFrame is throttled or + // suspended (hidden/background tabs, some embedded webviews): keep dirty state + // from going stale. A no-op whenever the rAF loop is running normally. + setInterval(() => { + if (dirty && Date.now() - lastFrameAt > 300) { + dirty = false; + render(); + } + }, 250); + + // ----- tooltip -------------------------------------------------------------- + + function positionTooltip(clientX, clientY) { + const rect = viewportEl.getBoundingClientRect(); + let x = clientX - rect.left + 14; + let y = clientY - rect.top + 14; + const w = tooltipEl.offsetWidth; + const h = tooltipEl.offsetHeight; + if (x + w > rect.width - 8) x = Math.max(8, clientX - rect.left - w - 10); + if (y + h > rect.height - 8) y = Math.max(8, clientY - rect.top - h - 10); + tooltipEl.style.left = x + 'px'; + tooltipEl.style.top = y + 'px'; + } + + function showTooltip(id, clientX, clientY) { + tooltipEl.textContent = ''; + tooltipEl.appendChild(elWith('span', 'tt-name', names[id])); + tooltipEl.appendChild(elWith('span', 'tt-kind', decls[id].kind || '')); + tooltipEl.hidden = false; + positionTooltip(clientX, clientY); + } + + function hideTooltip() { + tooltipEl.hidden = true; + } + + // ----- side panel ----------------------------------------------------------- + + function kindDotEl(kind) { + const dot = elWith('span', 'kind-dot', null); + if (KINDS.indexOf(kind) >= 0) dot.classList.add('k-' + kind); + return dot; + } + + function moduleSourcePath(moduleName) { + return moduleName.replace(/\./g, '/') + '.lean'; + } + + function moduleDocsPath(moduleName) { + return moduleName.replace(/\./g, '/') + '.html'; + } + + function appendDepSection(label, list) { + panelBodyEl.appendChild( + elWith('div', 'panel-h', label + ' (' + list.length + ')')); + if (list.length === 0) { + panelBodyEl.appendChild( + elWith('div', 'panel-meta', 'none within this project')); + return; + } + const ul = elWith('ul', 'dep-list', null); + const appendRows = (from, to) => { + for (let j = from; j < to; j++) { + const target = list[j]; + const li = document.createElement('li'); + const btn = elWith('button', 'dep-link', null); + btn.type = 'button'; + btn.appendChild(kindDotEl(decls[target].kind)); + btn.appendChild(document.createTextNode(names[target])); + btn.addEventListener('click', () => { + selectNode(target, { pan: true }); + }); + li.appendChild(btn); + ul.appendChild(li); + } + }; + // Hub nodes can have thousands of dependents; cap the initial render. + const initial = Math.min(list.length, DEP_LIST_INITIAL); + appendRows(0, initial); + if (list.length > initial) { + const li = document.createElement('li'); + const more = elWith('button', 'dep-link dep-more', + 'Show all ' + list.length); + more.type = 'button'; + more.addEventListener('click', () => { + li.remove(); + appendRows(initial, list.length); + }); + li.appendChild(more); + ul.appendChild(li); + } + panelBodyEl.appendChild(ul); + } + + function buildPanel(id) { + const d = decls[id]; + panelBodyEl.textContent = ''; + + const nameEl = elWith('h2', 'panel-name', d.name || ''); + if (d.private) { + nameEl.appendChild(elWith('span', 'badge badge-private', 'private')); + } + panelBodyEl.appendChild(nameEl); + + const chips = elWith('div', 'panel-chips', null); + const kindChip = elWith('span', 'kind-chip', null); + kindChip.appendChild(kindDotEl(d.kind)); + kindChip.appendChild(document.createTextNode(d.kind || 'unknown')); + chips.appendChild(kindChip); + if (d.main) { + chips.appendChild(elWith('span', 'badge badge-main', '★ main result')); + } + panelBodyEl.appendChild(chips); + + if (mainInformal[id]) { + panelBodyEl.appendChild( + elWith('p', 'panel-informal', mainInformal[id])); + } + + const moduleName = modules[d.module] || ''; + const lineText = d.endLine && d.endLine !== d.line + ? d.line + '–' + d.endLine + : String(d.line); + panelBodyEl.appendChild( + elWith('div', 'panel-meta', moduleName + ':' + lineText)); + + const links = elWith('div', 'panel-links', null); + const src = elWith('a', null, 'source'); + src.href = GITHUB_BLOB + moduleSourcePath(moduleName) + + '#L' + d.line + '-L' + (d.endLine || d.line); + src.target = '_blank'; + src.rel = 'noopener'; + links.appendChild(src); + if (!d.full) { + const docs = elWith('a', null, 'API docs'); + docs.href = '../../../' + moduleDocsPath(moduleName) + '#' + d.name; + docs.target = '_blank'; + docs.rel = 'noopener'; + links.appendChild(docs); + } + panelBodyEl.appendChild(links); + + if (typeof d.ext === 'number' && d.ext > 0) { + panelBodyEl.appendChild(elWith('div', 'panel-meta', + 'uses ' + d.ext + ' declaration' + (d.ext === 1 ? '' : 's') + + ' from Mathlib/core')); + } + + const actions = elWith('div', 'panel-actions', null); + const coneBtn = elWith('button', 'btn btn-accent', 'Dependency cone'); + coneBtn.type = 'button'; + coneBtn.addEventListener('click', () => { + setHash('cone=' + id); + }); + actions.appendChild(coneBtn); + panelBodyEl.appendChild(actions); + + if (d.doc) { + const doc = elWith('div', 'panel-doc', null); + const parts = String(d.doc).split(/\n\s*\n/); + for (const part of parts) { + const trimmed = part.trim(); + if (trimmed) doc.appendChild(elWith('p', null, trimmed)); + } + panelBodyEl.appendChild(doc); + } + + if (d.statement) { + panelBodyEl.appendChild(elWith('pre', 'statement', d.statement)); + } + + appendDepSection('Uses', deps[id]); + appendDepSection('Used by', rev[id]); + panelBodyEl.scrollTop = 0; + } + + // ----- selection ------------------------------------------------------------ + + function selectNode(id, opts) { + const options = opts || {}; + if (id < 0 || id >= N) return; + if (view === coneView && coneView && coneView.toView[id] < 0) { + // The target sits outside the cone: fall back to the full graph. + exitCone(false); + } + selected = id; + recomputeNeighborhood(); + buildPanel(id); + panelEl.hidden = false; + if (options.pan) panTo(id); + if (options.hash !== false && view === fullView) setHash('d' + id); + dirty = true; + } + + function deselect(updateHash) { + if (selected < 0) return; + selected = -1; + neighborFlags.fill(0); + panelEl.hidden = true; + dirty = true; + if (updateHash && view === fullView) clearHash(); + } + + // ----- dependency cone -------------------------------------------------------- + + // Marks everything reachable from `start` via `adjacency` (excluding start); + // returns the count. + function reachableSet(start, adjacency, flags) { + const seen = new Uint8Array(N); + seen[start] = 1; + const stack = [start]; + let count = 0; + while (stack.length) { + const v = stack.pop(); + const list = adjacency[v]; + for (let j = 0; j < list.length; j++) { + const w = list[j]; + if (!seen[w]) { + seen[w] = 1; + flags[w] = 1; + count++; + stack.push(w); + } + } + } + return count; + } + + // Iterative Tarjan SCC over a view-local adjacency (arrays of ints). + function tarjanScc(n, adj) { + const index = new Int32Array(n).fill(-1); + const low = new Int32Array(n); + const onStack = new Uint8Array(n); + const sccId = new Int32Array(n).fill(-1); + const stack = []; + const callStack = []; + const iterStack = []; + let counter = 0; + let count = 0; + for (let root = 0; root < n; root++) { + if (index[root] !== -1) continue; + callStack.push(root); + iterStack.push(0); + while (callStack.length) { + const v = callStack[callStack.length - 1]; + if (iterStack[iterStack.length - 1] === 0 && index[v] === -1) { + index[v] = counter; + low[v] = counter; + counter++; + stack.push(v); + onStack[v] = 1; + } + const edges = adj[v]; + let i = iterStack[iterStack.length - 1]; + let advanced = false; + while (i < edges.length) { + const w = edges[i]; + if (index[w] === -1) { + iterStack[iterStack.length - 1] = i + 1; + callStack.push(w); + iterStack.push(0); + advanced = true; + break; + } + if (onStack[w] && index[w] < low[v]) low[v] = index[w]; + i++; + } + if (advanced) continue; + callStack.pop(); + iterStack.pop(); + if (low[v] === index[v]) { + for (;;) { + const w = stack.pop(); + onStack[w] = 0; + sccId[w] = count; + if (w === v) break; + } + count++; + } + if (callStack.length) { + const parent = callStack[callStack.length - 1]; + if (low[v] < low[parent]) low[parent] = low[v]; + } + } + } + return { id: sccId, count }; + } + + // Longest-path layering of the subgraph induced by `ids`, with SCCs + // condensed (every member of an SCC shares the layer). Within-layer order + // follows the original shard `order`. + function layerSubgraph(ids) { + const n = ids.length; + const local = new Int32Array(N).fill(-1); + for (let i = 0; i < n; i++) local[ids[i]] = i; + const adj = new Array(n); // dependency -> dependent + for (let i = 0; i < n; i++) adj[i] = []; + for (let i = 0; i < n; i++) { + const list = deps[ids[i]]; + for (let j = 0; j < list.length; j++) { + const s = local[list[j]]; + if (s >= 0 && s !== i) adj[s].push(i); + } + } + const scc = tarjanScc(n, adj); + const sccAdj = new Array(scc.count); + for (let s = 0; s < scc.count; s++) sccAdj[s] = []; + const indegree = new Int32Array(scc.count); + for (let u = 0; u < n; u++) { + const out = adj[u]; + const su = scc.id[u]; + for (let j = 0; j < out.length; j++) { + const sv = scc.id[out[j]]; + if (su !== sv) { + sccAdj[su].push(sv); + indegree[sv]++; + } + } + } + const sccLayer = new Int32Array(scc.count); + const queue = []; + for (let s = 0; s < scc.count; s++) if (indegree[s] === 0) queue.push(s); + let qi = 0; + while (qi < queue.length) { + const s = queue[qi++]; + const out = sccAdj[s]; + for (let j = 0; j < out.length; j++) { + const t = out[j]; + if (sccLayer[s] + 1 > sccLayer[t]) sccLayer[t] = sccLayer[s] + 1; + indegree[t]--; + if (indegree[t] === 0) queue.push(t); + } + } + const layerOf = new Int32Array(n); + let maxLayer = 0; + for (let i = 0; i < n; i++) { + layerOf[i] = sccLayer[scc.id[i]]; + if (layerOf[i] > maxLayer) maxLayer = layerOf[i]; + } + const byLayer = new Array(maxLayer + 1); + for (let L = 0; L <= maxLayer; L++) byLayer[L] = []; + for (let i = 0; i < n; i++) byLayer[layerOf[i]].push(i); + const orderOf = new Int32Array(n); + const layerSizes = new Array(maxLayer + 1).fill(0); + for (let L = 0; L <= maxLayer; L++) { + const members = byLayer[L]; + members.sort((a, b) => { + const oa = (decls[ids[a]].order || 0) - (decls[ids[b]].order || 0); + return oa !== 0 ? oa : ids[a] - ids[b]; + }); + layerSizes[L] = members.length; + for (let j = 0; j < members.length; j++) orderOf[members[j]] = j; + } + return { layerOf, orderOf, layerSizes }; + } + + function enterCone(id) { + if (id < 0 || id >= N) return; + if (view === coneView && coneRoot === id) { + if (selected !== id) selectNode(id, { hash: false }); + return; + } + const ancFlags = new Uint8Array(N); + const descFlags = new Uint8Array(N); + const ancestors = reachableSet(id, deps, ancFlags); + const descendants = reachableSet(id, rev, descFlags); + const memberList = []; + for (let i = 0; i < N; i++) { + if (i === id || ancFlags[i] || descFlags[i]) memberList.push(i); + } + const ids = Int32Array.from(memberList); + const layered = layerSubgraph(ids); + coneView = buildView(ids, layered.layerOf, layered.orderOf, + layered.layerSizes); + coneRoot = id; + view = coneView; + breadcrumbEl.hidden = false; + coneBackEl.href = '#d' + id; + coneLabelEl.textContent = ' · cone of ' + names[id] + ': ' + + ancestors + ' ancestor' + (ancestors === 1 ? '' : 's') + + ' · ' + descendants + ' descendant' + + (descendants === 1 ? '' : 's'); + updateDerivedColors(); + recomputeMatches(); + selected = id; + recomputeNeighborhood(); + buildPanel(id); + panelEl.hidden = false; + hoverId = -1; + hideTooltip(); + fitCamera(); + dirty = true; + } + + function exitCone(updateHash) { + const wasCone = view === coneView && coneView !== null; + coneView = null; + coneRoot = -1; + if (!wasCone) return; + view = fullView; + breadcrumbEl.hidden = true; + hoverId = -1; + hideTooltip(); + updateDerivedColors(); + recomputeMatches(); + fitCamera(); + dirty = true; + if (updateHash) { + if (selected >= 0) setHash('d' + selected); + else clearHash(); + } + } + + // ----- search --------------------------------------------------------------- + + function updateSearchCount() { + if (!searchCountEl) return; + if (!searchQuery) { + searchCountEl.textContent = ''; + return; + } + searchCountEl.textContent = matchTotal + + (matchTotal === 1 ? ' match' : ' matches'); + } + + function recomputeMatches() { + if (!matchFlags) return; + matchFlags.fill(0); + matchTotal = 0; + firstMatch = -1; + if (searchQuery && view) { + for (let i = 0; i < view.n; i++) { + const id = view.ids[i]; + if (lowerNames[id].indexOf(searchQuery) >= 0) { + matchFlags[id] = 1; + matchTotal++; + if (firstMatch < 0) firstMatch = id; + } + } + } + updateSearchCount(); + dirty = true; + } + + // ----- hash routing ----------------------------------------------------------- + + function setHash(fragment) { + if (location.hash === '#' + fragment) return; + location.hash = fragment; + } + + function clearHash() { + if (!location.hash) return; + history.pushState(null, '', location.pathname + location.search); + } + + function applyHash() { + if (N === 0) return; + const h = location.hash; + let m = /^#cone=(\d+)$/.exec(h); + if (m) { + const id = Number(m[1]); + if (id >= 0 && id < N) { + enterCone(id); + return; + } + } + m = /^#d(\d+)$/.exec(h); + if (m) { + const id = Number(m[1]); + if (id >= 0 && id < N) { + if (view === coneView && coneView) exitCone(false); + if (selected !== id) selectNode(id, { pan: true, hash: false }); + return; + } + } + if (view === coneView && coneView) exitCone(false); + deselect(false); + } + + // ----- pointer / wheel / keyboard interaction --------------------------------- + + let pointerActive = false; + let pointerMoved = false; + let lastX = 0; + let lastY = 0; + let downX = 0; + let downY = 0; + + function pickAtEvent(ev) { + const rect = canvas.getBoundingClientRect(); + const gx = toGraphX(ev.clientX - rect.left); + const gy = toGraphY(ev.clientY - rect.top); + return pickNode(gx, gy, 10 / camera.scale + NODE_SIZE / 2); + } + + function updateHover(ev) { + const vi = pickAtEvent(ev); + const id = vi >= 0 ? view.ids[vi] : -1; + if (id !== hoverId) { + hoverId = id; + dirty = true; + canvas.style.cursor = id >= 0 ? 'pointer' : ''; + if (id >= 0) showTooltip(id, ev.clientX, ev.clientY); + else hideTooltip(); + } else if (id >= 0) { + positionTooltip(ev.clientX, ev.clientY); + } + } + + canvas.addEventListener('pointerdown', (ev) => { + if (ev.button !== 0) return; + pointerActive = true; + pointerMoved = false; + interacting = true; + lastX = downX = ev.clientX; + lastY = downY = ev.clientY; + try { + canvas.setPointerCapture(ev.pointerId); + } catch (ignored) { /* older engines */ } + }); + + canvas.addEventListener('pointermove', (ev) => { + if (pointerActive) { + const dx = ev.clientX - lastX; + const dy = ev.clientY - lastY; + lastX = ev.clientX; + lastY = ev.clientY; + if (Math.abs(ev.clientX - downX) + Math.abs(ev.clientY - downY) > 4) { + pointerMoved = true; + viewportEl.classList.add('dragging'); + hideTooltip(); + } + if (pointerMoved) { + camera.tx += dx; + camera.ty += dy; + autoFit = false; + dirty = true; + } + } else if (view) { + updateHover(ev); + } + }); + + function endPointer(ev, wasClick) { + if (!pointerActive) return; + pointerActive = false; + interacting = false; + viewportEl.classList.remove('dragging'); + dirty = true; + if (wasClick && !pointerMoved && view) { + const vi = pickAtEvent(ev); + if (vi >= 0) selectNode(view.ids[vi], {}); + else deselect(true); + } + } + + canvas.addEventListener('pointerup', (ev) => endPointer(ev, true)); + canvas.addEventListener('pointercancel', (ev) => endPointer(ev, false)); + canvas.addEventListener('pointerleave', () => { + if (!pointerActive) { + hoverId = -1; + hideTooltip(); + canvas.style.cursor = ''; + dirty = true; + } + }); + + canvas.addEventListener('wheel', (ev) => { + ev.preventDefault(); + const rect = canvas.getBoundingClientRect(); + const unit = ev.deltaMode === 1 ? 0.045 : 0.0015; + zoomAt(ev.clientX - rect.left, ev.clientY - rect.top, + Math.exp(-ev.deltaY * unit)); + interacting = true; + clearTimeout(wheelTimer); + wheelTimer = setTimeout(() => { + interacting = false; + dirty = true; + }, 160); + }, { passive: false }); + + canvas.addEventListener('dblclick', (ev) => { + if (view && pickAtEvent(ev) < 0) fitCamera(); + }); + + document.addEventListener('keydown', (ev) => { + if (ev.key === 'Escape' && ev.target === document.body) deselect(true); + }); + + if (searchInputEl) { + searchInputEl.addEventListener('input', () => { + searchQuery = searchInputEl.value.trim().toLowerCase(); + recomputeMatches(); + }); + searchInputEl.addEventListener('keydown', (ev) => { + if (ev.key === 'Enter') { + if (firstMatch >= 0) selectNode(firstMatch, { pan: true }); + } else if (ev.key === 'Escape') { + searchInputEl.value = ''; + searchQuery = ''; + recomputeMatches(); + searchInputEl.blur(); + } + }); + } + + if (fitButtonEl) fitButtonEl.addEventListener('click', () => fitCamera()); + if (panelCloseEl) panelCloseEl.addEventListener('click', () => deselect(true)); + window.addEventListener('hashchange', applyHash); + + // ----- theme + resize wiring ---------------------------------------------------- + + const darkQuery = window.matchMedia('(prefers-color-scheme: dark)'); + const onThemeChange = () => { + readTheme(); + updateDerivedColors(); + dirty = true; + }; + if (typeof darkQuery.addEventListener === 'function') { + darkQuery.addEventListener('change', onThemeChange); + } + + function resizeCanvas() { + const rect = viewportEl.getBoundingClientRect(); + const w = Math.max(1, Math.round(rect.width)); + const h = Math.max(1, Math.round(rect.height)); + const stale = cssW <= 1 || cssH <= 1; + const changed = w !== cssW || h !== cssH; + cssW = w; + cssH = h; + dpr = window.devicePixelRatio || 1; + canvas.width = Math.max(1, Math.round(cssW * dpr)); + canvas.height = Math.max(1, Math.round(cssH * dpr)); + // Keep the graph fitted across viewport changes until the user takes + // over the camera (also heals a fit computed before layout settled). + if (changed && view) { + if (autoFit) fitCamera(); + else if (stale && selected >= 0) panTo(selected); + } + dirty = true; + } + + if (typeof ResizeObserver === 'function') { + new ResizeObserver(resizeCanvas).observe(viewportEl); + } + window.addEventListener('resize', resizeCanvas); + + // ----- info strip --------------------------------------------------------------- + + function fillInfoStrip(json) { + if (titleEl) titleEl.textContent = json.title || json.project || slug; + if (provenanceEl) { + if (json.provenance) { + provenanceEl.textContent = json.provenance; + provenanceEl.className = 'badge badge-prov-' + + String(json.provenance).toLowerCase(); + provenanceEl.hidden = false; + } else { + provenanceEl.hidden = true; + } + } + const stats = json.stats || {}; + if (statsEl) { + const nodes = stats.nodes !== undefined ? stats.nodes : N; + const edges = stats.edges !== undefined ? stats.edges : 0; + const maxDepth = stats.maxDepth !== undefined ? stats.maxDepth : 0; + const avgDepth = stats.avgDepth !== undefined ? stats.avgDepth : 0; + statsEl.textContent = nodes + ' nodes · ' + edges + + ' edges · max depth ' + maxDepth + ' · avg depth ' + + avgDepth; + } + if (legendEl) { + legendEl.textContent = ''; + const counts = stats.kinds || {}; + const known = new Set(KINDS); + const ordered = KINDS.filter((k) => counts[k]) + .concat(Object.keys(counts).filter((k) => !known.has(k))); + for (const kind of ordered) { + const chip = elWith('span', 'kind-chip', null); + chip.appendChild(kindDotEl(kind)); + chip.appendChild(document.createTextNode(kind + ' ' + counts[kind])); + legendEl.appendChild(chip); + } + } + } + + // ----- data load ---------------------------------------------------------------- + + function showMessage(text) { + messageEl.textContent = text; + messageEl.hidden = false; + } + + function computeLayerSizes(layerOf) { + let max = 0; + for (let i = 0; i < layerOf.length; i++) { + if (layerOf[i] > max) max = layerOf[i]; + } + const sizes = new Array(max + 1).fill(0); + for (let i = 0; i < layerOf.length; i++) sizes[layerOf[i]]++; + return sizes; + } + + function sourceLink(source) { + if (source.doi) return 'https://doi.org/' + source.doi; + if (source.arxiv) return 'https://arxiv.org/abs/' + source.arxiv; + return source.url || null; + } + + function fillCardStrip(json) { + const strip = byId('card-strip'); + if (!strip) return; + const card = json.card; + const results = Array.isArray(json.mainResults) ? json.mainResults : []; + if (!card && results.length === 0) return; + strip.textContent = ''; + + const meta = elWith('div', 'card-meta-line', null); + const addPiece = (node) => { + if (meta.childNodes.length) { + meta.appendChild(document.createTextNode(' · ')); + } + meta.appendChild(node); + }; + if (card && card.authors && card.authors.length) { + addPiece(document.createTextNode(card.authors.join(', '))); + } + if (card && card.branch) { + addPiece(document.createTextNode(card.branch)); + } + if (card && card.license) { + addPiece(document.createTextNode(card.license)); + } + if (card && card.source) { + const href = sourceLink(card.source); + if (href) { + const paper = elWith('a', null, card.source.title || 'paper'); + paper.href = href; + paper.target = '_blank'; + paper.rel = 'noopener'; + addPiece(paper); + } else if (card.source.title) { + addPiece(document.createTextNode(card.source.title)); + } + if (card.source.github_repo) { + const upstream = elWith('a', null, 'upstream repo'); + upstream.href = 'https://github.com/' + card.source.github_repo; + upstream.target = '_blank'; + upstream.rel = 'noopener'; + addPiece(upstream); + } + } + if (meta.childNodes.length) strip.appendChild(meta); + + if (card && card.summary) { + strip.appendChild(elWith('p', 'card-summary', card.summary)); + } + + if (results.length) { + const box = elWith('details', 'main-results', null); + box.open = results.length <= 4; + const label = elWith('summary', null, + 'Main results (' + results.length + ')'); + box.appendChild(label); + const list = elWith('ul', 'main-result-list', null); + for (const result of results) { + const item = elWith('li', 'main-result-item', null); + if (typeof result.id === 'number') { + const link = elWith('a', 'main-result-name mono', result.name); + link.href = '#d' + result.id; + item.appendChild(link); + } else { + item.appendChild(elWith('span', 'main-result-name mono', result.name)); + } + if (result.informal) { + item.appendChild(elWith('span', 'main-result-informal', + ' — ' + result.informal)); + } + list.appendChild(item); + } + box.appendChild(list); + strip.appendChild(box); + } + strip.hidden = false; + } + + function initData(json) { + decls = Array.isArray(json.decls) ? json.decls : []; + modules = Array.isArray(json.modules) ? json.modules : []; + N = decls.length; + fillInfoStrip(json); + fillCardStrip(json); + // The card strip just changed the viewport height; remeasure before the + // initial fit/hash-driven pan so deep links center correctly. + resizeCanvas(); + mainIds = []; + mainInformal = {}; + for (let i = 0; i < decls.length; i++) { + if (decls[i].main) mainIds.push(i); + } + const resultsList = Array.isArray(json.mainResults) ? json.mainResults : []; + for (const result of resultsList) { + if (typeof result.id === 'number' && result.informal) { + mainInformal[result.id] = result.informal; + } + } + if (N === 0) { + showMessage('This project has no declarations to display.'); + return; + } + names = new Array(N); + lowerNames = new Array(N); + nodeKinds = new Array(N); + deps = new Array(N); + for (let i = 0; i < N; i++) { + const d = decls[i]; + names[i] = d.name || '#' + i; + lowerNames[i] = names[i].toLowerCase(); + nodeKinds[i] = d.kind || 'def'; + const raw = Array.isArray(d.deps) ? d.deps : []; + const cleaned = []; + for (let j = 0; j < raw.length; j++) { + const t = raw[j]; + if (typeof t === 'number' && t >= 0 && t < N) cleaned.push(t); + } + deps[i] = Int32Array.from(cleaned); + } + const revCounts = new Int32Array(N); + for (let i = 0; i < N; i++) { + const list = deps[i]; + for (let j = 0; j < list.length; j++) revCounts[list[j]]++; + } + rev = new Array(N); + for (let i = 0; i < N; i++) rev[i] = new Int32Array(revCounts[i]); + const cursor = new Int32Array(N); + for (let i = 0; i < N; i++) { + const list = deps[i]; + for (let j = 0; j < list.length; j++) { + const t = list[j]; + rev[t][cursor[t]] = i; + cursor[t]++; + } + } + matchFlags = new Uint8Array(N); + neighborFlags = new Uint8Array(N); + const idsAll = new Int32Array(N); + const layerOf = new Int32Array(N); + const orderOf = new Int32Array(N); + for (let i = 0; i < N; i++) { + idsAll[i] = i; + layerOf[i] = decls[i].layer || 0; + orderOf[i] = decls[i].order || 0; + } + const layerSizes = Array.isArray(json.layers) && json.layers.length > 0 + ? json.layers + : computeLayerSizes(layerOf); + fullView = buildView(idsAll, layerOf, orderOf, layerSizes); + view = fullView; + updateDerivedColors(); + messageEl.hidden = true; + fitCamera(); + applyHash(); + dirty = true; + } + + function loadShard() { + showMessage('Loading…'); + fetch('../../data/projects/' + encodeURIComponent(slug) + '.json') + .then((response) => { + if (!response.ok) throw new Error('HTTP ' + response.status); + return response.json(); + }) + .then((json) => { + initData(json); + }) + .catch((error) => { + showMessage('Could not load the dependency graph for “' + slug + + '” — data/projects/' + slug + '.json failed to load (' + + error.message + ').'); + }); + } + + // ----- boot --------------------------------------------------------------------- + + readTheme(); + updateDerivedColors(); + resizeCanvas(); + loadShard(); + requestAnimationFrame(frame); +})(); diff --git a/python/lean_pool/exposition/static/assets/landing.js b/python/lean_pool/exposition/static/assets/landing.js new file mode 100644 index 0000000000..6f25ae85e1 --- /dev/null +++ b/python/lean_pool/exposition/static/assets/landing.js @@ -0,0 +1,288 @@ +/* Landing page for the Lean Pool exposition. + * + * Fetches data/index.json (relative to the exposition root) and renders: + * - stat tiles (projects / declarations / edges / deepest chain), + * - a segmented kind-breakdown bar with a legend, + * - a sortable, filterable project table, + * - a "generated … · commit …" footer. + */ +(function () { + "use strict"; + + const CANONICAL_KINDS = [ + "theorem", "lemma", "def", "abbrev", "instance", + "structure", "class", "inductive", "axiom", "opaque", + ]; + + const COLUMNS = [ + { key: "project", label: "Project", numeric: false }, + { key: "branch", label: "Area", numeric: false }, + { key: "provenance", label: "Provenance", numeric: false }, + { key: "license", label: "License", numeric: false }, + { key: "nodes", label: "Decls", numeric: true }, + { key: "edges", label: "Edges", numeric: true }, + { key: "maxDepth", label: "Max depth", numeric: true }, + { key: "avgDepth", label: "Avg depth", numeric: true }, + ]; + + // Default sort: declaration count, largest first. + const state = { column: "nodes", descending: true, filter: "" }; + let projects = []; + + function element(id) { + return document.getElementById(id); + } + + function formatCount(value) { + return Number(value).toLocaleString("en-US"); + } + + function kindColor(kind) { + return CANONICAL_KINDS.includes(kind) ? `var(--kind-${kind})` : "var(--muted)"; + } + + // ---------- stat tiles ---------- + + function renderTiles(totals) { + const tiles = [ + ["Projects", totals.projects], + ["Declarations", totals.decls], + ["Dependency edges", totals.edges], + ["Deepest chain", totals.maxDepth], + ]; + const box = element("statTiles"); + for (const [label, value] of tiles) { + const tile = document.createElement("div"); + tile.className = "stat-tile"; + const valueEl = document.createElement("div"); + valueEl.className = "stat-value"; + valueEl.textContent = formatCount(value); + const labelEl = document.createElement("div"); + labelEl.className = "stat-label"; + labelEl.textContent = label; + tile.append(valueEl, labelEl); + box.appendChild(tile); + } + box.hidden = false; + } + + // ---------- kind breakdown bar ---------- + + function renderKindBreakdown(kinds) { + const entries = Object.entries(kinds || {}) + .filter(([, count]) => count > 0) + .sort((a, b) => b[1] - a[1]); + if (entries.length === 0) return; + const total = entries.reduce((sum, [, count]) => sum + count, 0); + + const bar = element("kindBar"); + const legend = element("kindLegend"); + for (const [kind, count] of entries) { + const segment = document.createElement("div"); + segment.className = "kind-seg"; + segment.style.flexGrow = String(count); + segment.style.background = kindColor(kind); + const pct = ((100 * count) / total).toFixed(1); + segment.title = `${kind} — ${formatCount(count)} (${pct}%)`; + bar.appendChild(segment); + + const item = document.createElement("span"); + item.className = "legend-item"; + const dot = document.createElement("span"); + dot.className = "legend-dot"; + dot.style.background = kindColor(kind); + const name = document.createElement("span"); + name.textContent = kind; + const countEl = document.createElement("span"); + countEl.className = "legend-count"; + countEl.textContent = formatCount(count); + item.append(dot, name, countEl); + legend.appendChild(item); + } + element("kindBreakdown").hidden = false; + } + + // ---------- project table ---------- + + function sortValue(project, key) { + switch (key) { + case "project": + return (project.title || project.slug).toLowerCase(); + case "provenance": + case "branch": + case "license": + return (project[key] || "￿").toLowerCase(); // sort null values last (asc) + default: + return project[key]; + } + } + + function compareProjects(a, b) { + const va = sortValue(a, state.column); + const vb = sortValue(b, state.column); + let cmp = va < vb ? -1 : va > vb ? 1 : 0; + if (cmp === 0) cmp = a.slug < b.slug ? -1 : a.slug > b.slug ? 1 : 0; + return state.descending ? -cmp : cmp; + } + + function renderHead() { + const row = element("projectHead"); + row.textContent = ""; + for (const column of COLUMNS) { + const th = document.createElement("th"); + if (column.numeric) th.className = "num"; + th.setAttribute("aria-sort", state.column === column.key + ? (state.descending ? "descending" : "ascending") + : "none"); + const button = document.createElement("button"); + button.type = "button"; + button.className = "sort-button"; + button.textContent = column.label; + if (state.column === column.key) { + button.dataset.dir = state.descending ? "desc" : "asc"; + } + button.addEventListener("click", () => { + if (state.column === column.key) { + state.descending = !state.descending; + } else { + state.column = column.key; + state.descending = column.numeric; // numeric columns start descending + } + renderHead(); + renderBody(); + }); + th.appendChild(button); + row.appendChild(th); + } + } + + function numericCell(text) { + const td = document.createElement("td"); + td.className = "num"; + td.textContent = text; + return td; + } + + function renderRow(project) { + const tr = document.createElement("tr"); + + const projectCell = document.createElement("td"); + projectCell.className = "cell-project"; + const link = document.createElement("a"); + link.href = `p/${encodeURIComponent(project.slug)}/`; + const title = document.createElement("span"); + title.className = "project-name"; + title.textContent = project.title || project.slug; + const slug = document.createElement("span"); + slug.className = "project-slug"; + slug.textContent = project.slug; + link.append(title, slug); + projectCell.appendChild(link); + if (project.authors && project.authors.length) { + const authors = document.createElement("span"); + authors.className = "project-authors"; + authors.textContent = project.authors.join(", "); + projectCell.appendChild(authors); + } + tr.appendChild(projectCell); + + const branchCell = document.createElement("td"); + branchCell.className = "cell-branch"; + branchCell.textContent = project.branch || "—"; + tr.appendChild(branchCell); + + const provenanceCell = document.createElement("td"); + const badge = document.createElement("span"); + badge.className = `prov prov-${project.provenance || "none"}`; + badge.textContent = project.provenance || "—"; + provenanceCell.appendChild(badge); + tr.appendChild(provenanceCell); + + const licenseCell = document.createElement("td"); + licenseCell.className = "cell-license"; + licenseCell.textContent = project.license || "—"; + tr.appendChild(licenseCell); + + tr.appendChild(numericCell(formatCount(project.nodes))); + tr.appendChild(numericCell(formatCount(project.edges))); + tr.appendChild(numericCell(formatCount(project.maxDepth))); + tr.appendChild(numericCell(Number(project.avgDepth || 0).toFixed(2))); + return tr; + } + + function renderBody() { + const query = state.filter; + const rows = projects.filter((p) => + !query + || p.slug.toLowerCase().includes(query) + || (p.title || "").toLowerCase().includes(query) + || (p.branch || "").toLowerCase().includes(query) + || (p.authors || []).some((a) => a.toLowerCase().includes(query))); + rows.sort(compareProjects); + + const body = element("projectBody"); + body.textContent = ""; + const fragment = document.createDocumentFragment(); + for (const project of rows) fragment.appendChild(renderRow(project)); + body.appendChild(fragment); + + if (rows.length === 0) { + const tr = document.createElement("tr"); + const td = document.createElement("td"); + td.colSpan = COLUMNS.length; + td.className = "table-empty"; + td.textContent = "No projects match."; + tr.appendChild(td); + body.appendChild(tr); + } + + element("projectCount").textContent = query + ? `${rows.length} of ${projects.length} projects` + : `${projects.length} projects`; + } + + // ---------- footer ---------- + + function renderFooter(data) { + const footer = element("landingFooter"); + const date = (data.generated || "").slice(0, 10); + const sha = (data.commit || "").slice(0, 7); + footer.append(`generated ${date} · commit `); + const link = document.createElement("a"); + link.className = "mono"; + link.href = `https://github.com/Vilin97/lean-pool/commit/${encodeURIComponent(data.commit || "")}`; + link.textContent = sha; + footer.appendChild(link); + } + + // ---------- boot ---------- + + function init(data) { + projects = (data.projects || []).slice(); + renderTiles(data.totals || {}); + renderKindBreakdown((data.totals || {}).kinds); + renderHead(); + renderBody(); + renderFooter(data); + element("projectsSection").hidden = false; + + element("projectFilter").addEventListener("input", (event) => { + state.filter = event.target.value.trim().toLowerCase(); + renderBody(); + }); + } + + fetch("data/index.json") + .then((response) => { + if (!response.ok) throw new Error(`HTTP ${response.status}`); + return response.json(); + }) + .then(init) + .catch((error) => { + const box = element("loadError"); + box.hidden = false; + box.textContent = + `Failed to load data/index.json (${error.message}). ` + + "If you opened this page from disk, serve it over HTTP instead."; + }); +})(); diff --git a/python/lean_pool/exposition/static/assets/style.css b/python/lean_pool/exposition/static/assets/style.css new file mode 100644 index 0000000000..8087a7b44f --- /dev/null +++ b/python/lean_pool/exposition/static/assets/style.css @@ -0,0 +1,637 @@ +/* Lean Pool exposition — shared stylesheet. + Loaded by every page. Defines the design tokens, base/reset, shared header, + buttons/chips/badges, the declaration side panel, and all graph-page styles. + Viewer/landing-specific styles live in viewer.css (owned by the viewer). */ + +/* ---------- design tokens ---------- */ + +:root { + --bg: #faf9f7; + --fg: #1c1c1c; + --muted: #6b6960; + --card: #ffffff; + --border: #e3ded4; + --accent: #1a6baa; + --accent-fg: #ffffff; + --hover: #f0ede6; + --kind-theorem: #8250df; + --kind-lemma: #1a7f37; + --kind-def: #0969da; + --kind-abbrev: #54aeff; + --kind-instance: #bf8700; + --kind-structure: #cf222e; + --kind-class: #a40e26; + --kind-inductive: #bc4c00; + --kind-axiom: #57606a; + --kind-opaque: #57606a; + --star: #bf8700; + --shadow: 0 1px 3px rgb(0 0 0 / 0.08); + --font-sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, + Arial, sans-serif; + --font-mono: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; +} + +@media (prefers-color-scheme: dark) { + :root { + --bg: #161513; + --fg: #e8e6e1; + --muted: #94917f; + --card: #201f1c; + --border: #38352e; + --accent: #5ea3d8; + --accent-fg: #10222f; + --hover: #26241f; + --kind-theorem: #b197f5; + --kind-lemma: #57ab5a; + --kind-def: #539bf5; + --kind-abbrev: #76b6f7; + --kind-instance: #daaa3f; + --kind-structure: #e5534b; + --kind-class: #f47067; + --kind-inductive: #e0823d; + --kind-axiom: #768390; + --kind-opaque: #768390; + --star: #daaa3f; + } +} + +/* ---------- base / reset ---------- */ + +*, +*::before, +*::after { + box-sizing: border-box; +} + +html { + height: 100%; +} + +body { + margin: 0; + font-family: var(--font-sans); + font-size: 15px; + line-height: 1.55; + color: var(--fg); + background: var(--bg); + -webkit-font-smoothing: antialiased; +} + +code, +pre, +kbd, +samp { + font-family: var(--font-mono); +} + +a { + color: var(--accent); +} + +[hidden] { + display: none !important; +} + +h1, +h2, +h3, +h4 { + line-height: 1.3; +} + +/* Generic centered content column for landing/viewer pages. */ +.page-main { + max-width: 1100px; + margin: 0 auto; + padding: 28px 20px 48px; +} + +/* ---------- shared site header ---------- */ + +.site-header { + display: flex; + align-items: center; + justify-content: space-between; + gap: 16px; + height: 48px; + padding: 0 16px; + background: var(--card); + border-bottom: 1px solid var(--border); + flex: none; +} + +.site-title { + font-size: 15px; + font-weight: 600; + color: var(--fg); + text-decoration: none; + white-space: nowrap; +} + +.site-title:hover { + color: var(--accent); +} + +.site-nav { + display: flex; + gap: 18px; + overflow-x: auto; +} + +.site-nav a { + color: var(--muted); + font-size: 13.5px; + text-decoration: none; + white-space: nowrap; + line-height: 48px; +} + +.site-nav a:hover { + color: var(--fg); +} + +/* ---------- buttons ---------- */ + +.btn { + font: inherit; + font-size: 13px; + padding: 5px 12px; + border: 1px solid var(--border); + border-radius: 6px; + background: var(--card); + color: var(--fg); + cursor: pointer; +} + +.btn:hover { + background: var(--hover); +} + +.btn-accent { + background: var(--accent); + border-color: var(--accent); + color: var(--accent-fg); +} + +.btn-accent:hover { + background: var(--accent); + opacity: 0.9; +} + +.btn:focus-visible, +.search-input:focus-visible, +.dep-link:focus-visible, +.panel-close:focus-visible { + outline: 2px solid var(--accent); + outline-offset: 1px; +} + +/* ---------- chips ---------- */ + +.kind-chip { + display: inline-flex; + align-items: center; + gap: 5px; + font-size: 12px; + color: var(--muted); + white-space: nowrap; +} + +.kind-dot { + display: inline-block; + width: 8px; + height: 8px; + border-radius: 2px; + background: var(--muted); + flex: none; +} + +.kind-dot.k-theorem { background: var(--kind-theorem); } +.kind-dot.k-lemma { background: var(--kind-lemma); } +.kind-dot.k-def { background: var(--kind-def); } +.kind-dot.k-abbrev { background: var(--kind-abbrev); } +.kind-dot.k-instance { background: var(--kind-instance); } +.kind-dot.k-structure { background: var(--kind-structure); } +.kind-dot.k-class { background: var(--kind-class); } +.kind-dot.k-inductive { background: var(--kind-inductive); } +.kind-dot.k-axiom { background: var(--kind-axiom); } +.kind-dot.k-opaque { background: var(--kind-opaque); } + +/* ---------- badges ---------- */ + +.badge { + display: inline-block; + font-size: 11px; + font-weight: 500; + line-height: 1.6; + padding: 0 8px; + border-radius: 999px; + border: 1px solid var(--border); + color: var(--muted); + background: transparent; + vertical-align: middle; + white-space: nowrap; +} + +.badge-prov-human { color: var(--kind-lemma); border-color: currentcolor; } +.badge-prov-ai { color: var(--kind-theorem); border-color: currentcolor; } +.badge-prov-mix { color: var(--kind-inductive); border-color: currentcolor; } + +.badge-private { + color: var(--muted); + background: var(--hover); + border-color: var(--border); + font-family: var(--font-sans); + font-weight: 400; + margin-left: 8px; +} + +/* ---------- search input ---------- */ + +.search-input { + flex: 0 1 340px; + min-width: 140px; + padding: 5px 10px; + border: 1px solid var(--border); + border-radius: 6px; + background: var(--card); + color: var(--fg); + font: inherit; + font-size: 13.5px; +} + +.search-input::placeholder { + color: var(--muted); +} + +.search-count { + color: var(--muted); + font-size: 12.5px; + white-space: nowrap; +} + +/* ---------- graph page layout ---------- */ + +body.graph-body { + height: 100vh; + height: 100dvh; + overflow: hidden; + display: flex; + flex-direction: column; +} + +.info-strip { + display: flex; + align-items: baseline; + flex-wrap: wrap; + gap: 6px 16px; + padding: 10px 16px 8px; + border-bottom: 1px solid var(--border); + flex: none; +} + +.project-title { + font-size: 17px; + font-weight: 650; + margin: 0; +} + +/* card metadata strip (registry card + main results) */ + +.card-strip { + padding: 6px 16px 8px; + border-bottom: 1px solid var(--border); + flex: none; + max-height: 30vh; + overflow-y: auto; + font-size: 13px; +} + +.card-meta-line { + color: var(--muted); +} + +.card-meta-line a { + color: var(--accent); + text-decoration: none; +} + +.card-meta-line a:hover { + text-decoration: underline; +} + +.card-summary { + margin: 4px 0 0; + max-width: 900px; + color: var(--fg); +} + +.main-results { + margin-top: 4px; +} + +.main-results summary { + cursor: pointer; + color: var(--muted); + font-weight: 600; + -webkit-user-select: none; + user-select: none; +} + +.main-result-list { + margin: 4px 0 2px; + padding-left: 18px; +} + +.main-result-item { + margin: 2px 0; +} + +.main-result-item::marker { + content: "★ "; + color: var(--star); + font-size: 11px; +} + +.main-result-name { + font-family: var(--font-mono); + font-size: 12.5px; +} + +a.main-result-name { + color: var(--accent); + text-decoration: none; +} + +a.main-result-name:hover { + text-decoration: underline; +} + +.main-result-informal { + color: var(--muted); +} + +.badge-main { + border: 1px solid var(--star); + color: var(--star); +} + +.panel-informal { + margin: 6px 0 0; + font-style: italic; + color: var(--muted); +} + +.info-stats { + color: var(--muted); + font-size: 13px; +} + +.kind-legend { + display: inline-flex; + align-items: baseline; + flex-wrap: wrap; + gap: 4px 12px; + margin-left: auto; +} + +.graph-toolbar { + display: flex; + align-items: center; + gap: 10px; + padding: 8px 16px; + border-bottom: 1px solid var(--border); + flex: none; +} + +.breadcrumb-bar { + padding: 6px 16px; + font-size: 13px; + color: var(--muted); + background: var(--hover); + border-bottom: 1px solid var(--border); + flex: none; +} + +.breadcrumb-bar a { + color: var(--accent); + text-decoration: none; +} + +.breadcrumb-bar a:hover { + text-decoration: underline; +} + +/* ---------- graph viewport ---------- */ + +.graph-viewport { + position: relative; + flex: 1 1 auto; + min-height: 0; + overflow: hidden; +} + +.graph-viewport canvas { + position: absolute; + inset: 0; + width: 100%; + height: 100%; + display: block; + touch-action: none; +} + +.graph-viewport.dragging canvas { + cursor: grabbing; +} + +.graph-tooltip { + position: absolute; + z-index: 5; + pointer-events: none; + background: var(--card); + border: 1px solid var(--border); + border-radius: 6px; + box-shadow: var(--shadow); + padding: 4px 9px; + font-size: 12px; + max-width: 420px; + word-break: break-all; +} + +.graph-tooltip .tt-name { + font-family: var(--font-mono); +} + +.graph-tooltip .tt-kind { + color: var(--muted); + margin-left: 8px; +} + +.graph-message { + position: absolute; + left: 50%; + top: 40%; + transform: translate(-50%, -50%); + color: var(--muted); + font-size: 14px; + text-align: center; + max-width: 520px; + padding: 0 20px; +} + +/* ---------- declaration side panel ---------- */ + +.decl-panel { + position: absolute; + top: 0; + right: 0; + bottom: 0; + width: 400px; + max-width: calc(100% - 24px); + display: flex; + flex-direction: column; + background: var(--card); + border-left: 1px solid var(--border); + box-shadow: var(--shadow); + z-index: 6; +} + +.panel-bar { + flex: none; + display: flex; + justify-content: flex-end; + padding: 6px 8px 0; +} + +.panel-close { + border: none; + background: none; + color: var(--muted); + font-size: 18px; + line-height: 1; + padding: 4px 9px; + border-radius: 6px; + cursor: pointer; +} + +.panel-close:hover { + background: var(--hover); + color: var(--fg); +} + +.panel-body { + overflow-y: auto; + padding: 0 16px 28px; +} + +.panel-name { + font-family: var(--font-mono); + font-size: 14px; + font-weight: 600; + line-height: 1.4; + margin: 0 0 8px; + word-break: break-all; +} + +.panel-chips { + display: flex; + align-items: center; + flex-wrap: wrap; + gap: 8px; + margin-bottom: 10px; +} + +.panel-meta { + font-size: 12.5px; + color: var(--muted); + margin: 4px 0; + word-break: break-all; +} + +.panel-links { + display: flex; + gap: 14px; + font-size: 12.5px; + margin: 4px 0 10px; +} + +.panel-actions { + margin: 12px 0; +} + +.panel-doc { + font-size: 13px; +} + +.panel-doc p { + margin: 6px 0; +} + +pre.statement { + font-family: var(--font-mono); + font-size: 12px; + line-height: 1.5; + background: var(--hover); + border: 1px solid var(--border); + border-radius: 6px; + padding: 10px 12px; + overflow-x: auto; + white-space: pre; + margin: 8px 0 12px; +} + +.panel-h { + font-size: 11px; + font-weight: 600; + text-transform: uppercase; + letter-spacing: 0.07em; + color: var(--muted); + margin: 16px 0 4px; +} + +.dep-list { + list-style: none; + margin: 2px 0 10px; + padding: 0; +} + +.dep-list li { + margin: 2px 0; +} + +.dep-link { + display: inline-flex; + align-items: center; + gap: 6px; + font-family: var(--font-mono); + font-size: 12px; + color: var(--accent); + background: none; + border: none; + padding: 1px 0; + cursor: pointer; + text-align: left; + word-break: break-all; +} + +.dep-link:hover { + text-decoration: underline; +} + +/* ---------- responsive ---------- */ + +@media (max-width: 800px) { + .site-nav { + gap: 12px; + } + + .kind-legend { + margin-left: 0; + width: 100%; + } + + .decl-panel { + width: 100%; + max-width: 100%; + } +} diff --git a/python/lean_pool/exposition/static/assets/viewer.css b/python/lean_pool/exposition/static/assets/viewer.css new file mode 100644 index 0000000000..26a40c25ae --- /dev/null +++ b/python/lean_pool/exposition/static/assets/viewer.css @@ -0,0 +1,563 @@ +/* Styles specific to the landing page and the all-declarations viewer. + * Consumes the tokens defined in style.css (loaded first on both pages): + * --bg --fg --muted --card --border --accent --accent-fg --hover and the + * --kind-* colors. Shared chrome (header, base typography) lives in + * style.css and is NOT redefined here. */ + +/* ---------- small shared bits ---------- */ + +.mono { + font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; +} + +.load-error { + color: var(--kind-structure); + margin: 24px 0; +} + +/* Kind chip: colored label used in the viewer rows and filter chips. + * The per-kind classes only set --kc; the chips derive tint/border from it. + * (.kfilter-chip, not .kind-chip: the latter is a shared graph-page class.) */ +.kchip, +.kfilter-chip { + --kc: var(--muted); + color: var(--kc); +} + +.k-theorem { --kc: var(--kind-theorem); } +.k-lemma { --kc: var(--kind-lemma); } +.k-def { --kc: var(--kind-def); } +.k-abbrev { --kc: var(--kind-abbrev); } +.k-instance { --kc: var(--kind-instance); } +.k-structure { --kc: var(--kind-structure); } +.k-class { --kc: var(--kind-class); } +.k-inductive { --kc: var(--kind-inductive); } +.k-axiom { --kc: var(--kind-axiom); } +.k-opaque { --kc: var(--kind-opaque); } +.k-other { --kc: var(--muted); } + +/* ---------- landing page ---------- */ + +.landing-wrap { + max-width: 1080px; + margin: 0 auto; + padding: 36px 24px 48px; +} + +.hero h1 { + font-size: 30px; + font-weight: 650; + letter-spacing: -0.01em; + margin: 0 0 8px; +} + +.hero p { + color: var(--muted); + margin: 0; + max-width: 64ch; +} + +.stat-tiles { + display: grid; + grid-template-columns: repeat(auto-fit, minmax(160px, 1fr)); + gap: 12px; + margin-top: 28px; +} + +.stat-tile { + background: var(--card); + border: 1px solid var(--border); + border-radius: 6px; + padding: 14px 16px; +} + +.stat-value { + font-size: 26px; + font-weight: 650; + font-variant-numeric: tabular-nums; + line-height: 1.2; +} + +.stat-label { + color: var(--muted); + font-size: 12.5px; + text-transform: uppercase; + letter-spacing: 0.05em; + margin-top: 3px; +} + +.kind-breakdown { + margin-top: 20px; +} + +.kind-bar { + display: flex; + height: 12px; + border-radius: 6px; + overflow: hidden; + border: 1px solid var(--border); +} + +.kind-seg { + flex-basis: 0; /* flex-grow set inline, proportional to count */ + min-width: 2px; +} + +.pool-legend { + display: flex; + flex-wrap: wrap; + gap: 6px 16px; + margin-top: 10px; + font-size: 13px; + color: var(--muted); +} + +.legend-item { + display: inline-flex; + align-items: center; + gap: 6px; +} + +.legend-dot { + width: 10px; + height: 10px; + border-radius: 3px; + flex: none; +} + +.legend-count { + font-variant-numeric: tabular-nums; +} + +/* project table */ + +.projects { + margin-top: 36px; +} + +.table-tools { + display: flex; + align-items: center; + gap: 12px; + margin-bottom: 10px; +} + +.table-tools input[type="search"], +.viewer-toolbar input[type="search"], +.viewer-toolbar select { + background: var(--card); + color: var(--fg); + border: 1px solid var(--border); + border-radius: 6px; + padding: 7px 10px; + font: inherit; + font-size: 14px; +} + +.table-tools input[type="search"] { + flex: 0 1 280px; + min-width: 160px; +} + +.table-tools input[type="search"]:focus-visible, +.viewer-toolbar input[type="search"]:focus-visible, +.viewer-toolbar select:focus-visible { + outline: 2px solid var(--accent); + outline-offset: 1px; +} + +.table-count { + color: var(--muted); + font-size: 13px; + font-variant-numeric: tabular-nums; +} + +.table-wrap { + overflow-x: auto; + border: 1px solid var(--border); + border-radius: 6px; + background: var(--card); +} + +.project-table { + width: 100%; + min-width: 720px; + border-collapse: collapse; + font-size: 14px; +} + +.project-table th { + text-align: left; + padding: 0; + border-bottom: 1px solid var(--border); +} + +.project-table th.num, +.project-table td.num { + text-align: right; +} + +.project-table td.num { + font-variant-numeric: tabular-nums; + white-space: nowrap; +} + +.sort-button { + background: none; + border: none; + font: inherit; + font-size: 13px; + font-weight: 600; + color: var(--muted); + width: 100%; + text-align: inherit; + padding: 10px 14px; + cursor: pointer; +} + +.sort-button:hover { + color: var(--fg); +} + +.sort-button:focus-visible, +.vsort:focus-visible, +.kfilter-chip:focus-visible { + outline: 2px solid var(--accent); + outline-offset: -2px; +} + +.sort-button[data-dir]::after { + content: " ↑"; + color: var(--accent); +} + +.sort-button[data-dir="desc"]::after { + content: " ↓"; +} + +.project-table td { + padding: 9px 14px; + border-bottom: 1px solid var(--border); + vertical-align: middle; +} + +.project-table tbody tr:last-child td { + border-bottom: none; +} + +.project-table tbody tr:hover { + background: var(--hover); +} + +.cell-project a { + display: block; + text-decoration: none; + color: inherit; +} + +.project-name { + display: block; + color: var(--accent); + font-weight: 550; +} + +.cell-project a:hover .project-name { + text-decoration: underline; +} + +.project-slug { + display: block; + color: var(--muted); + font-size: 12px; + font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + margin-top: 1px; +} + +.project-authors { + display: block; + color: var(--muted); + font-size: 12px; + margin-top: 2px; +} + +.cell-branch, +.cell-license { + color: var(--muted); + font-size: 13px; + white-space: nowrap; +} + +@media (max-width: 1000px) { + .cell-license, + .project-table th:nth-child(4), + .cell-branch, + .project-table th:nth-child(2) { + display: none; + } +} + +.table-empty { + text-align: center; + color: var(--muted); + padding: 28px 14px; +} + +/* provenance badges */ + +.prov { + display: inline-block; + font-size: 11.5px; + font-weight: 600; + letter-spacing: 0.03em; + padding: 2px 9px; + border-radius: 999px; + border: 1px solid var(--border); + color: var(--muted); +} + +.prov-human { + color: var(--kind-lemma); + border-color: color-mix(in srgb, var(--kind-lemma) 40%, transparent); + background: color-mix(in srgb, var(--kind-lemma) 10%, transparent); +} + +.prov-AI { + color: var(--kind-theorem); + border-color: color-mix(in srgb, var(--kind-theorem) 40%, transparent); + background: color-mix(in srgb, var(--kind-theorem) 10%, transparent); +} + +.prov-mix { + color: var(--kind-inductive); + border-color: color-mix(in srgb, var(--kind-inductive) 40%, transparent); + background: color-mix(in srgb, var(--kind-inductive) 10%, transparent); +} + +.landing-footer { + margin-top: 44px; + padding-top: 16px; + border-top: 1px solid var(--border); + color: var(--muted); + font-size: 13px; +} + +/* ---------- declarations viewer ---------- */ + +.viewer-wrap { + display: flex; + flex-direction: column; + height: calc(100vh - var(--header-h, 49px)); + height: calc(100dvh - var(--header-h, 49px)); + max-width: 1200px; + margin: 0 auto; + padding: 16px 24px 16px; + box-sizing: border-box; +} + +.viewer-toolbar { + display: flex; + flex-wrap: wrap; + align-items: center; + gap: 10px; + padding-bottom: 12px; +} + +.viewer-toolbar input[type="search"] { + flex: 1 1 260px; + min-width: 180px; +} + +.viewer-toolbar select { + max-width: 240px; +} + +.decl-count { + color: var(--muted); + font-size: 13px; + white-space: nowrap; + font-variant-numeric: tabular-nums; + margin-left: auto; +} + +.kind-chips { + display: flex; + flex-wrap: wrap; + gap: 6px; + flex-basis: 100%; +} + +.kfilter-chip { + display: inline-flex; + align-items: center; + gap: 6px; + font: inherit; + font-size: 12.5px; + font-weight: 600; + padding: 3px 10px; + border-radius: 999px; + cursor: pointer; + background: color-mix(in srgb, var(--kc) 10%, transparent); + border: 1px solid color-mix(in srgb, var(--kc) 35%, transparent); +} + +.kfilter-chip:hover { + background: color-mix(in srgb, var(--kc) 18%, transparent); +} + +.kfilter-chip.chip-off { + color: var(--muted); + background: transparent; + border-color: var(--border); +} + +.kfilter-chip.chip-off:hover { + background: var(--hover); +} + +.chip-count { + font-weight: 400; + opacity: 0.75; + font-variant-numeric: tabular-nums; +} + +/* virtual list */ + +.vscroll { + flex: 1 1 auto; + min-height: 0; + overflow-y: auto; + border: 1px solid var(--border); + border-radius: 6px; + background: var(--card); + position: relative; +} + +.vhead, +.vrow { + display: grid; + grid-template-columns: minmax(0, 1fr) 110px 200px; + gap: 12px; + align-items: center; + padding: 0 14px; + box-sizing: border-box; +} + +.vhead { + position: sticky; + top: 0; + z-index: 1; + background: var(--card); + border-bottom: 1px solid var(--border); +} + +.vsort { + background: none; + border: none; + font: inherit; + font-size: 13px; + font-weight: 600; + color: var(--muted); + text-align: left; + padding: 10px 0; + cursor: pointer; +} + +.vsort:hover { + color: var(--fg); +} + +.vsort[data-dir]::after { + content: " ↑"; + color: var(--accent); +} + +.vsort[data-dir="desc"]::after { + content: " ↓"; +} + +.vspacer { + position: relative; +} + +.vwindow { + position: absolute; + top: 0; + left: 0; + right: 0; + will-change: transform; +} + +.vrow { + height: 34px; /* must match ROW_HEIGHT in viewer.js */ + cursor: pointer; + font-size: 13.5px; + box-shadow: inset 0 -1px var(--border); /* hairline that keeps height exact */ +} + +.vrow:hover { + background: var(--hover); +} + +.vcell-name { + font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; + font-size: 12.5px; + white-space: nowrap; + overflow: hidden; + text-overflow: ellipsis; +} + +/* the name cell is a real link (keyboard/a11y) but renders as plain text */ +a.vcell-name, +a.vcell-name:visited { + color: inherit; + text-decoration: none; +} + +a.vcell-name:hover, +a.vcell-name:focus-visible { + color: var(--accent); +} + +.vrow .kchip { + justify-self: start; + background: color-mix(in srgb, var(--kc) 10%, transparent); + border-radius: 999px; + padding: 1px 8px; + font-size: 12px; + font-weight: 600; +} + +.vcell-project { + color: var(--muted); + text-decoration: none; + white-space: nowrap; + overflow: hidden; + text-overflow: ellipsis; +} + +.vcell-project:hover { + color: var(--accent); + text-decoration: underline; +} + +.vempty { + padding: 48px 16px; + text-align: center; + color: var(--muted); +} + +/* ---------- narrow screens (chrome must survive down to ~800px) ---------- */ + +@media (max-width: 900px) { + .landing-wrap, + .viewer-wrap { + padding-left: 16px; + padding-right: 16px; + } + + .vhead, + .vrow { + grid-template-columns: minmax(0, 1fr) 92px 150px; + gap: 8px; + } +} diff --git a/python/lean_pool/exposition/static/assets/viewer.js b/python/lean_pool/exposition/static/assets/viewer.js new file mode 100644 index 0000000000..cffa2725f8 --- /dev/null +++ b/python/lean_pool/exposition/static/assets/viewer.js @@ -0,0 +1,335 @@ +/* All-declarations viewer for the Lean Pool exposition. + * + * Fetches ../data/decls.json (~55K rows, compact arrays) and renders a + * virtual-scrolled table: one absolutely positioned window of recycled row + * elements inside a fixed-height spacer. All heavy work happens once at + * load (lowercased names, per-column sorted index arrays); interactions are + * a single O(N) pass over typed arrays, well under 50 ms at pool scale. + */ +(function () { + "use strict"; + + const ROW_HEIGHT = 34; // px; must match .vrow height in viewer.css + const OVERSCAN = 12; // extra rows rendered above/below the viewport + const SEARCH_DEBOUNCE_MS = 150; + const CANONICAL_KINDS = [ + "theorem", "lemma", "def", "abbrev", "instance", + "structure", "class", "inductive", "axiom", "opaque", + ]; + + const scroller = document.getElementById("vscroll"); + const spacer = document.getElementById("vspacer"); + const windowEl = document.getElementById("vwindow"); + const emptyEl = document.getElementById("vempty"); + const countEl = document.getElementById("declCount"); + const searchEl = document.getElementById("declSearch"); + const selectEl = document.getElementById("projectSelect"); + const chipsEl = document.getElementById("kindChips"); + const headEl = document.getElementById("vhead"); + const errorEl = document.getElementById("loadError"); + + // Column-store over the decls array (filled in init). + let total = 0; + let kinds = []; + let projects = []; + let names = null; // string[] + let lowerNames = null; // string[], precomputed once for search + sort + let kindOf = null; // Uint8Array + let projectOf = null; // Uint16Array + let declIdOf = null; // Uint32Array + let kindRank = null; // Uint8Array: kind index -> canonical display rank + + const sortedOrders = new Map(); // column name -> ascending Uint32Array + let filtered = null; // Uint32Array scratch; first filteredCount valid + let filteredCount = 0; + + const state = { + column: "name", + descending: false, + query: "", + project: -1, // -1 = all projects + kindActive: [], // boolean per kind index + }; + + const rowPool = []; // recycled .vrow elements + let renderScheduled = false; + + function formatCount(value) { + return value.toLocaleString("en-US"); + } + + function kindClass(kindName) { + return CANONICAL_KINDS.includes(kindName) ? `k-${kindName}` : "k-other"; + } + + // ---------- sorting ---------- + + function nameCompare(a, b) { + const la = lowerNames[a]; + const lb = lowerNames[b]; + if (la < lb) return -1; + if (la > lb) return 1; + return a - b; // deterministic tie-break + } + + function orderFor(column) { + let order = sortedOrders.get(column); + if (order) return order; + order = new Uint32Array(total); + for (let i = 0; i < total; i++) order[i] = i; + let compare = nameCompare; + if (column === "kind") { + 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); + } + order.sort(compare); + sortedOrders.set(column, order); + return order; + } + + // ---------- filtering ---------- + + function applyFilter() { + const order = orderFor(state.column); + const descending = state.descending; + const query = state.query; + const hasQuery = query.length > 0; + const project = state.project; + const kindActive = state.kindActive; + const allKindsActive = kindActive.every(Boolean); + let n = 0; + for (let j = 0; j < total; j++) { + // Descending = walk the ascending order backwards (no array reversal). + const i = order[descending ? total - 1 - j : j]; + if (project !== -1 && projectOf[i] !== project) continue; + if (!allKindsActive && !kindActive[kindOf[i]]) continue; + if (hasQuery && lowerNames[i].indexOf(query) === -1) continue; + filtered[n++] = i; + } + filteredCount = n; + } + + function refresh(resetScroll) { + applyFilter(); + spacer.style.height = `${filteredCount * ROW_HEIGHT}px`; + emptyEl.hidden = filteredCount !== 0; + countEl.textContent = + `${formatCount(filteredCount)} of ${formatCount(total)} declarations`; + if (resetScroll) scroller.scrollTop = 0; + renderWindow(); + } + + // ---------- virtual window ---------- + + function makeRow() { + const row = document.createElement("div"); + row.className = "vrow"; + // A real link gives keyboard focus, Enter activation, and open-in-new-tab. + 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._name = name; + row._kind = kind; + row._project = project; + return row; + } + + function ensureRows(count) { + while (rowPool.length < count) { + const row = makeRow(); + windowEl.appendChild(row); + rowPool.push(row); + } + } + + function fillRow(row, i) { + row.dataset.index = i; + row._name.textContent = names[i]; + const slug = projects[projectOf[i]]; + row._name.href = `../p/${encodeURIComponent(slug)}/index.html#d${declIdOf[i]}`; + const kindName = kinds[kindOf[i]]; + row._kind.textContent = kindName; + row._kind.className = `kchip ${kindClass(kindName)}`; + row._project.textContent = slug; + row._project.href = `../p/${encodeURIComponent(slug)}/`; + } + + function renderWindow() { + let first = Math.floor(scroller.scrollTop / ROW_HEIGHT) - OVERSCAN; + if (first < 0) first = 0; + const visible = Math.ceil(scroller.clientHeight / ROW_HEIGHT) + 2 * OVERSCAN; + const needed = Math.max(0, Math.min(visible, filteredCount - first)); + ensureRows(needed); + windowEl.style.transform = `translateY(${first * ROW_HEIGHT}px)`; + for (let r = 0; r < rowPool.length; r++) { + const row = rowPool[r]; + if (r < needed) { + fillRow(row, filtered[first + r]); + row.style.display = ""; + } else { + row.style.display = "none"; + } + } + } + + function scheduleRender() { + if (renderScheduled) return; + renderScheduled = true; + requestAnimationFrame(() => { + renderScheduled = false; + renderWindow(); + }); + } + + // ---------- toolbar ---------- + + function buildProjectSelect() { + const fragment = document.createDocumentFragment(); + for (let p = 0; p < projects.length; p++) { + const option = document.createElement("option"); + option.value = String(p); + option.textContent = projects[p]; + fragment.appendChild(option); + } + selectEl.appendChild(fragment); + } + + function buildKindChips(kindCounts) { + const displayOrder = kinds.map((_, k) => k) + .sort((a, b) => kindRank[a] - kindRank[b] || a - b); + for (const k of displayOrder) { + const chip = document.createElement("button"); + chip.type = "button"; + chip.className = `kfilter-chip ${kindClass(kinds[k])}`; + chip.setAttribute("aria-pressed", "true"); + const label = document.createElement("span"); + label.textContent = kinds[k]; + const count = document.createElement("span"); + count.className = "chip-count"; + count.textContent = formatCount(kindCounts[k]); + chip.append(label, count); + chip.addEventListener("click", () => { + state.kindActive[k] = !state.kindActive[k]; + chip.setAttribute("aria-pressed", String(state.kindActive[k])); + chip.classList.toggle("chip-off", !state.kindActive[k]); + refresh(true); + }); + chipsEl.appendChild(chip); + } + } + + function updateSortIndicators() { + for (const button of headEl.querySelectorAll(".vsort")) { + if (button.dataset.col === state.column) { + button.dataset.dir = state.descending ? "desc" : "asc"; + button.setAttribute("aria-sort", + state.descending ? "descending" : "ascending"); + } else { + delete button.dataset.dir; + button.setAttribute("aria-sort", "none"); + } + } + } + + function wireEvents() { + scroller.addEventListener("scroll", scheduleRender); + window.addEventListener("resize", scheduleRender); + + // Row click -> project page anchored at the declaration. Clicks on the + // project keep their default navigation (to the project page top). + windowEl.addEventListener("click", (event) => { + if (event.target.closest("a")) return; + const row = event.target.closest(".vrow"); + if (!row) return; + const i = Number(row.dataset.index); + const slug = encodeURIComponent(projects[projectOf[i]]); + window.location.href = `../p/${slug}/index.html#d${declIdOf[i]}`; + }); + + let searchTimer = 0; + searchEl.addEventListener("input", () => { + clearTimeout(searchTimer); + searchTimer = setTimeout(() => { + state.query = searchEl.value.trim().toLowerCase(); + refresh(true); + }, SEARCH_DEBOUNCE_MS); + }); + + selectEl.addEventListener("change", () => { + state.project = Number(selectEl.value); + refresh(true); + }); + + headEl.addEventListener("click", (event) => { + const button = event.target.closest(".vsort"); + if (!button) return; + const column = button.dataset.col; + if (state.column === column) { + state.descending = !state.descending; + } else { + state.column = column; + state.descending = false; + } + updateSortIndicators(); + refresh(true); + }); + } + + // ---------- boot ---------- + + function init(data) { + kinds = data.kinds || []; + projects = data.projects || []; + const raw = data.decls || []; + total = raw.length; + + names = new Array(total); + lowerNames = new Array(total); + kindOf = new Uint8Array(total); + projectOf = new Uint16Array(total); + declIdOf = new Uint32Array(total); + const kindCounts = new Array(kinds.length).fill(0); + for (let i = 0; i < total; i++) { + const row = raw[i]; + names[i] = row[0]; + lowerNames[i] = row[0].toLowerCase(); + kindOf[i] = row[1]; + projectOf[i] = row[2]; + declIdOf[i] = row[3]; + kindCounts[row[1]] += 1; + } + + kindRank = new Uint8Array(kinds.length); + for (let k = 0; k < kinds.length; k++) { + const rank = CANONICAL_KINDS.indexOf(kinds[k]); + kindRank[k] = rank === -1 ? CANONICAL_KINDS.length : rank; + } + state.kindActive = new Array(kinds.length).fill(true); + filtered = new Uint32Array(total); + + buildProjectSelect(); + buildKindChips(kindCounts); + wireEvents(); + updateSortIndicators(); + refresh(true); + } + + fetch("../data/decls.json") + .then((response) => { + if (!response.ok) throw new Error(`HTTP ${response.status}`); + return response.json(); + }) + .then(init) + .catch((error) => { + countEl.textContent = ""; + errorEl.hidden = false; + errorEl.textContent = + `Failed to load ../data/decls.json (${error.message}). ` + + "If you opened this page from disk, serve it over HTTP instead."; + }); +})(); diff --git a/python/lean_pool/exposition/static/decls/index.html b/python/lean_pool/exposition/static/decls/index.html new file mode 100644 index 0000000000..8dc11ffab5 --- /dev/null +++ b/python/lean_pool/exposition/static/decls/index.html @@ -0,0 +1,54 @@ + + + + + + + Declarations · Lean Pool exposition + + + + +
+ Lean Pool exposition + +
+ +
+
+ + + Loading… +
+
+ +
+
+ + + +
+
+
+
+ +
+ + +
+ + + + diff --git a/python/lean_pool/exposition/static/index.html b/python/lean_pool/exposition/static/index.html new file mode 100644 index 0000000000..99511c2696 --- /dev/null +++ b/python/lean_pool/exposition/static/index.html @@ -0,0 +1,60 @@ + + + + + + + Lean Pool exposition + + + + +
+ Lean Pool exposition + +
+ +
+
+

Lean Pool exposition

+

Interactive dependency graphs and a declaration index for every + project in the pool — API docs hold the full + signatures.

+
+ + + + + + + + + +
+
+ + + + diff --git a/python/lean_pool/exposition/templates/project.html b/python/lean_pool/exposition/templates/project.html new file mode 100644 index 0000000000..b1d31070d8 --- /dev/null +++ b/python/lean_pool/exposition/templates/project.html @@ -0,0 +1,49 @@ + + + + + + ${TITLE} · Lean Pool exposition + + + +
+ Lean Pool exposition + +
+
+

${TITLE}

+ + + +
+ +
+ + + +
+ +
+ + + + +
+ + + diff --git a/python/tests/test_exposition_generate.py b/python/tests/test_exposition_generate.py new file mode 100644 index 0000000000..bab704987e --- /dev/null +++ b/python/tests/test_exposition_generate.py @@ -0,0 +1,391 @@ +"""End-to-end tests for the exposition site generator.""" + +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from lean_pool.exposition.generate import SiteSummary, generate_site + +ALPHA_ONE = """lemma a1 : True := trivial + +theorem a2 : True := a1 + +/-- Third. -/ +def a3 : Nat := + 2 +""" + +ALPHA_TWO = """theorem a4 : True := by + exact a2 +""" + +BETA = """def b1 : Nat := 1 + +lemma b2 : b1 = 1 := rfl + +private theorem b3 : True := trivial +""" + +PROJECTS_YML = """projects: + - slug: alpha-project + title: Alpha & Co + entry_module: LeanPool.Alpha + provenance: AI + authors: + - Ada Lovelace + license: Apache-2.0 + branch: order theory + summary: Toy project. + tags: + - toy + msc: + - 06B35 + status: verified + source: + title: A Paper + doi: 10.1000/xyz + github_repo: ada/alpha + main_declarations: + - a2 + - a3 + main_results: + - declaration: a2 + informal: Truth holds, twice. + - declaration: NotInShard.thm + informal: An unresolved headline. +""" + +TEMPLATE = ( + "${TITLE}" + '
${TITLE}
' + "" +) + +# Deliberately out of source order; ids are assigned after sorting by +# (module, line, name). a4 carries a dangling and a self dependency. +RECORDS = [ + { + "id": "a4", + "n": "a4", + "m": "LeanPool.Alpha.Two", + "k": "theorem", + "r": [1, 0, 2, 10], + "s": [1, 8], + "deps": ["a2", "a4", "Missing.dep"], + "ext": 3, + }, + { + "id": "a2", + "n": "a2", + "m": "LeanPool.Alpha.One", + "k": "theorem", + "r": [3, 0, 3, 23], + "s": [3, 8], + "deps": ["a1"], + "ext": 2, + }, + { + "id": "a1", + "n": "a1", + "m": "LeanPool.Alpha.One", + "k": "theorem", + "r": [1, 0, 1, 26], + "s": [1, 6], + "deps": [], + "ext": 1, + }, + { + "id": "a3", + "n": "a3", + "m": "LeanPool.Alpha.One", + "k": "def", + "r": [5, 0, 7, 3], + "s": [6, 4], + "d": "Third.", + "deps": [], + "ext": 0, + }, + { + "id": "b1", + "n": "b1", + "m": "LeanPool.Beta", + "k": "def", + "r": [1, 0, 1, 17], + "s": [1, 4], + "deps": [], + "ext": 0, + }, + { + "id": "b2", + "n": "b2", + "m": "LeanPool.Beta", + "k": "theorem", + "r": [3, 0, 3, 24], + "s": [3, 6], + "deps": ["b1"], + "ext": 1, + }, + { + "id": "_private.LeanPool.Beta.0.b3", + "n": "b3", + "m": "LeanPool.Beta", + "k": "theorem", + "r": [5, 0, 5, 36], + "s": [5, 16], + "p": True, + "deps": [], + "ext": 1, + }, +] + + +def _write_inputs(tmp_path: Path) -> tuple[Path, Path, Path, Path]: + """Create the fake repo, static, templates, and dump under tmp_path.""" + repo = tmp_path / "repo" + (repo / "LeanPool" / "Alpha").mkdir(parents=True) + (repo / "LeanPool" / "Alpha" / "One.lean").write_text(ALPHA_ONE) + (repo / "LeanPool" / "Alpha" / "Two.lean").write_text(ALPHA_TWO) + (repo / "LeanPool" / "Beta.lean").write_text(BETA) + (repo / "LeanPool" / "projects.yml").write_text(PROJECTS_YML) + static = tmp_path / "static" + (static / "decls").mkdir(parents=True) + (static / "assets").mkdir() + (static / "index.html").write_text("LANDING") + (static / "decls" / "index.html").write_text("DECLS") + (static / "assets" / "style.css").write_text("/*css*/") + templates = tmp_path / "templates" + templates.mkdir() + (templates / "project.html").write_text(TEMPLATE) + dump = tmp_path / "dump.jsonl" + dump.write_text("\n".join(json.dumps(record) for record in RECORDS) + "\n") + return repo, static, templates, dump + + +@pytest.fixture +def site(tmp_path: Path) -> tuple[Path, SiteSummary]: + """Generate the site from the synthetic dump; return (out_dir, summary).""" + repo, static, templates, dump = _write_inputs(tmp_path) + out = tmp_path / "out" + summary = generate_site( + dump, + repo, + out, + commit="deadbeef", + static_dir=static, + templates_dir=templates, + ) + return out, summary + + +def _load(out: Path, relative: str) -> dict: + """Load one generated JSON file.""" + return json.loads((out / relative).read_text()) + + +def test_summary_totals(site: tuple[Path, SiteSummary]) -> None: + """The returned summary reports pool-wide totals.""" + _, summary = site + assert summary == SiteSummary(projects=2, decls=7, edges=3) + + +def test_project_shard_schema_and_stats(site: tuple[Path, SiteSummary]) -> None: + """The Alpha shard has schema key order, stats, layout, and remapped deps.""" + out, _ = site + shard = _load(out, "data/projects/Alpha.json") + assert list(shard) == [ + "schema", + "project", + "title", + "provenance", + "card", + "mainResults", + "stats", + "modules", + "layers", + "decls", + ] + assert shard["schema"] == 1 + assert shard["project"] == "Alpha" + assert shard["title"] == "Alpha & Co" + assert shard["provenance"] == "AI" + assert shard["stats"] == { + "nodes": 4, + "edges": 2, + "maxDepth": 2, + "avgDepth": 0.75, + "kinds": {"theorem": 2, "def": 1, "lemma": 1}, + } + assert shard["modules"] == ["LeanPool.Alpha.One", "LeanPool.Alpha.Two"] + assert shard["layers"] == [2, 1, 1] + names = [node["name"] for node in shard["decls"]] + assert names == ["a1", "a2", "a3", "a4"] + a4 = shard["decls"][3] + assert a4["deps"] == [1] # dangling and self deps dropped, id remapped + assert a4["layer"] == 2 + assert a4["module"] == 1 + assert shard["decls"][1]["deps"] == [0] + + +def test_card_and_main_results(site: tuple[Path, SiteSummary]) -> None: + """Shards carry the registry card and resolved main results (schema 1.1).""" + out, _ = site + shard = _load(out, "data/projects/Alpha.json") + assert shard["card"] == { + "authors": ["Ada Lovelace"], + "license": "Apache-2.0", + "branch": "order theory", + "summary": "Toy project.", + "tags": ["toy"], + "msc": ["06B35"], + "status": "verified", + "source": { + "title": "A Paper", + "doi": "10.1000/xyz", + "github_repo": "ada/alpha", + }, + } + # a2 (id 1) keeps its informal text; a3 (id 2) comes from + # main_declarations only; the unknown name stays unresolved with id null. + assert shard["mainResults"] == [ + {"id": 1, "name": "a2", "informal": "Truth holds, twice."}, + {"id": None, "name": "NotInShard.thm", "informal": "An unresolved headline."}, + {"id": 2, "name": "a3"}, + ] + decls = shard["decls"] + assert decls[1].get("main") is True + assert decls[2].get("main") is True + assert "main" not in decls[0] + beta = _load(out, "data/projects/Beta.json") + assert beta["card"] is None + assert beta["mainResults"] == [] + + +def test_declaration_nodes(site: tuple[Path, SiteSummary]) -> None: + """Node rows carry refined kinds, statements, docs, and privacy flags.""" + out, _ = site + alpha = _load(out, "data/projects/Alpha.json")["decls"] + assert alpha[0]["kind"] == "lemma" + assert alpha[0]["statement"] == "lemma a1 : True" + assert alpha[2]["doc"] == "Third." + assert alpha[2]["statement"] == "def a3 : Nat" + assert alpha[2]["line"] == 5 + assert alpha[2]["endLine"] == 7 + assert list(alpha[2]) == [ + "name", + "kind", + "module", + "line", + "endLine", + "doc", + "statement", + "deps", + "ext", + "layer", + "order", + "main", # a3 is one of the card's main declarations + ] + beta = _load(out, "data/projects/Beta.json")["decls"] + b3 = beta[2] + assert b3["full"] == "_private.LeanPool.Beta.0.b3" + assert b3["private"] is True + assert b3["statement"] == "theorem b3 : True" + assert list(b3) == [ + "name", + "full", + "kind", + "module", + "line", + "endLine", + "statement", + "private", + "deps", + "ext", + "layer", + "order", + ] + + +def test_index_json(site: tuple[Path, SiteSummary]) -> None: + """index.json carries the commit, totals, and per-project rows by slug.""" + out, _ = site + index = _load(out, "data/index.json") + assert index["schema"] == 1 + assert index["commit"] == "deadbeef" + assert index["generated"].endswith("Z") + assert index["totals"] == { + "projects": 2, + "decls": 7, + "edges": 3, + "maxDepth": 2, + "kinds": {"theorem": 3, "def": 2, "lemma": 2}, + } + assert [row["slug"] for row in index["projects"]] == ["Alpha", "Beta"] + assert index["projects"][0] == { + "slug": "Alpha", + "title": "Alpha & Co", + "provenance": "AI", + "nodes": 4, + "edges": 2, + "maxDepth": 2, + "avgDepth": 0.75, + "authors": ["Ada Lovelace"], + "license": "Apache-2.0", + "branch": "order theory", + "mainResults": 3, + } + beta_row = index["projects"][1] + 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["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].""" + 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], + ] + + +def test_static_copy_and_project_pages(site: tuple[Path, SiteSummary]) -> None: + """Static files are copied verbatim; project pages are instantiated.""" + out, _ = site + assert (out / "index.html").read_text() == "LANDING" + assert (out / "decls" / "index.html").read_text() == "DECLS" + assert (out / "assets" / "style.css").read_text() == "/*css*/" + alpha_page = (out / "p" / "Alpha" / "index.html").read_text() + assert "Alpha & Co" in alpha_page + assert 'data-slug="Alpha"' in alpha_page + assert "`${d.name}`" in alpha_page # JS template literals survive + beta_page = (out / "p" / "Beta" / "index.html").read_text() + assert "Beta" in beta_page # title falls back to the slug + assert 'data-slug="Beta"' in beta_page + + +def test_missing_static_directory_raises(tmp_path: Path) -> None: + """A missing static directory fails loudly instead of emitting a site.""" + repo, _, templates, dump = _write_inputs(tmp_path) + with pytest.raises(FileNotFoundError, match="static asset directory"): + generate_site( + dump, + repo, + tmp_path / "out2", + static_dir=tmp_path / "no-such-static", + templates_dir=templates, + ) diff --git a/python/tests/test_exposition_layout.py b/python/tests/test_exposition_layout.py new file mode 100644 index 0000000000..b5b50ebe02 --- /dev/null +++ b/python/tests/test_exposition_layout.py @@ -0,0 +1,90 @@ +"""Tests for the pure-Python layered graph layout.""" + +from __future__ import annotations + +import random + +from lean_pool.exposition.layout import compute_layout + + +def test_empty_graph() -> None: + """An empty graph yields empty layers, orders, and sizes.""" + layout = compute_layout([]) + assert layout.node_layers == [] + assert layout.node_orders == [] + assert layout.layer_sizes == [] + + +def test_chain() -> None: + """A linear chain puts each node on its own layer.""" + layout = compute_layout([[], [0], [1], [2]]) + assert layout.node_layers == [0, 1, 2, 3] + assert layout.node_orders == [0, 0, 0, 0] + assert layout.layer_sizes == [1, 1, 1, 1] + + +def test_diamond() -> None: + """A diamond shares the middle layer and peaks one layer above it.""" + layout = compute_layout([[], [0], [0], [1, 2]]) + assert layout.node_layers == [0, 1, 1, 2] + assert layout.layer_sizes == [1, 2, 1] + assert sorted(layout.node_orders[1:3]) == [0, 1] + assert layout.node_orders[0] == 0 + assert layout.node_orders[3] == 0 + + +def test_two_cycle_shares_layer() -> None: + """Members of a 2-cycle SCC share a layer; dependents sit above it.""" + layout = compute_layout([[1], [0], [0]]) + assert layout.node_layers[0] == layout.node_layers[1] == 0 + assert layout.node_layers[2] == 1 + assert layout.layer_sizes == [2, 1] + + +def test_barycenter_removes_crossing() -> None: + """Crossed edges between two layers are uncrossed by the sweeps.""" + # Layer 0: nodes 0, 1. Layer 1: node 2 above node 1, node 3 above node 0. + layout = compute_layout([[], [], [1], [0]]) + assert layout.node_layers == [0, 0, 1, 1] + assert layout.node_orders[0] == 0 + assert layout.node_orders[1] == 1 + # Node 3 (over node 0) must come before node 2 (over node 1). + assert layout.node_orders[3] == 0 + assert layout.node_orders[2] == 1 + + +def _random_graph(seed: int, node_count: int) -> list[list[int]]: + """Build a mostly-acyclic random graph with one planted 2-cycle.""" + generator = random.Random(seed) + dependencies: list[list[int]] = [[] for _ in range(node_count)] + for node in range(1, node_count): + for _ in range(generator.randint(0, 3)): + dependencies[node].append(generator.randrange(node)) + dependencies[10].append(20) + dependencies[20].append(10) + return [sorted(set(deps)) for deps in dependencies] + + +def test_deterministic_across_runs() -> None: + """Two runs over equal inputs give identical layouts.""" + first = compute_layout(_random_graph(42, 60)) + second = compute_layout(_random_graph(42, 60)) + assert first == second + + +def test_random_graph_invariants() -> None: + """Layers respect dependencies and orders are per-layer permutations.""" + dependencies = _random_graph(7, 50) + layout = compute_layout(dependencies) + assert sum(layout.layer_sizes) == 50 + assert layout.node_layers[10] == layout.node_layers[20] + for node, deps in enumerate(dependencies): + if not deps: + assert layout.node_layers[node] == 0 + for dependency in deps: + assert layout.node_layers[node] >= layout.node_layers[dependency] + per_layer: dict[int, list[int]] = {} + for node, layer in enumerate(layout.node_layers): + per_layer.setdefault(layer, []).append(layout.node_orders[node]) + for layer, orders in per_layer.items(): + assert sorted(orders) == list(range(layout.layer_sizes[layer])) diff --git a/python/tests/test_exposition_source_text.py b/python/tests/test_exposition_source_text.py new file mode 100644 index 0000000000..db0a753fef --- /dev/null +++ b/python/tests/test_exposition_source_text.py @@ -0,0 +1,98 @@ +"""Tests for statement slicing and kind refinement from Lean source text.""" + +from __future__ import annotations + +from lean_pool.exposition.source_text import SourceFile, statement_slice + +THEOREM_BLOCK = """\ +/-- Doc for foo. -/ +@[simp] +private theorem foo (n : Nat) : + n + 0 = n := by + simp +""" + + +def _slice( + text: str, + declaration_range: list[int], + selection: list[int], + fallback: str = "theorem", +) -> tuple[str, str]: + """Run statement_slice over freshly parsed source text.""" + source = SourceFile.from_text(text) + return statement_slice(source, declaration_range, selection, fallback) + + +def test_theorem_with_assignment_boundary() -> None: + """Doc comment, attribute, and modifier are skipped; body is cut at :=.""" + kind, statement = _slice(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16]) + assert kind == "theorem" + assert statement == "theorem foo (n : Nat) :\n n + 0 = n" + + +def test_lemma_keyword_refines_theorem_kind() -> None: + """A source `lemma` refines the extractor's coarse `theorem` kind.""" + text = "lemma bar : True := trivial\n" + kind, statement = _slice(text, [1, 0, 1, 27], [1, 6], fallback="theorem") + assert kind == "lemma" + assert statement == "lemma bar : True" + + +def test_def_with_where_boundary() -> None: + """A structure-instance body introduced by `where` ends the statement.""" + text = "def origin : Point where\n x := 1\n y := 2\n" + kind, statement = _slice(text, [1, 0, 3, 8], [1, 4], fallback="def") + assert kind == "def" + assert statement == "def origin : Point" + + +def test_inductive_arms_boundary() -> None: + """Constructor arms (no `=>`) still end an inductive's statement.""" + text = "inductive Color\n | red\n | green\n" + kind, statement = _slice(text, [1, 0, 3, 9], [1, 10], fallback="inductive") + assert kind == "inductive" + assert statement == "inductive Color" + + +def test_class_inductive_reports_class() -> None: + """`class inductive` reports kind `class` and keeps the full header.""" + text = "class inductive Weird (α : Type) : Type\n | intro : Weird α\n" + kind, statement = _slice(text, [1, 0, 2, 19], [1, 16], fallback="class") + assert kind == "class" + assert statement == "class inductive Weird (α : Type) : Type" + + +def test_generated_decl_with_midline_range_gets_empty_statement() -> None: + """Attribute-generated decls (range at a mid-line token) blank the statement.""" + text = "@[to_additive]\ntheorem prod_thing : True := trivial\n" + kind, statement = _slice(text, [1, 2, 1, 13], [1, 2], fallback="theorem") + assert kind == "theorem" + assert statement == "" + + +def test_deriving_generated_instance_gets_empty_statement() -> None: + """`deriving`-generated instances point mid-line and blank the statement.""" + text = "structure Point where\n x : Nat\n deriving DecidableEq\n" + kind, statement = _slice(text, [3, 11, 3, 22], [3, 11], fallback="instance") + assert kind == "instance" + assert statement == "" + + +def test_unknown_keyword_at_line_start_keeps_raw_slice() -> None: + """A column-0 non-declaration command (e.g. notation) keeps its source text.""" + text = 'notation "⟦" x "⟧" => quot x\n' + kind, statement = _slice(text, [1, 0, 1, 28], [1, 0], fallback="def") + assert kind == "def" + assert statement.startswith("notation") + + +def test_statement_capped_at_1200_characters() -> None: + """Over-long statements are cut to 1200 characters ending in an ellipsis.""" + long_type = " → ".join(["Nat"] * 400) + text = f"def long : {long_type} := fun value => value\n" + kind, statement = _slice(text, [1, 0, 1, len(text) - 1], [1, 4], fallback="def") + assert kind == "def" + assert 1150 <= len(statement) <= 1200 + assert statement.endswith("…") + assert statement.startswith("def long : Nat") diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean new file mode 100644 index 0000000000..9151917ff2 --- /dev/null +++ b/scripts/exposition/Extract.lean @@ -0,0 +1,185 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vasily Ilin +-/ +import Lean + +/-! +# Exposition extractor + +Dumps every human-written declaration in the pool, together with its +intra-pool dependency edges, as JSONL. One line per declaration: + +```json +{"id": "", "n": "", "m": "", "k": "", + "p": , "r": [startLine, startCol, endLine, endCol], "s": [nameLine, nameCol], + "d": "", "deps": ["", ...], "ext": } +``` + +Dependency edges follow the kernel closure: references to compiler-generated +auxiliaries (`match_*`, equation lemmas, `.rec`, constructors, projections, ...) +are expanded transitively until a human-written declaration is reached, so an +edge `A -> B` means "checking `A` requires `B`". `ext` counts distinct +declarations outside the pool (Mathlib/core) encountered on that boundary. + +Usage: `lake env lean --run scripts/exposition/Extract.lean ` +-/ + +open Lean Meta + +namespace Exposition + +/-- The library whose declarations we extract. -/ +def poolRoot : Name := `LeanPool + +/-- Is `module` one of the pool's own modules? -/ +def isPoolModule (module : Name) : Bool := + poolRoot.isPrefixOf module + +/-- Coarse declaration kind, used only as a fallback: the site generator +refines it from the source keyword (`lemma` vs `theorem`, `abbrev` vs `def`, +`instance`, `class`, ...). Extension-backed queries (`isClass`, +`Meta.isInstance`) are unavailable here because the environment is imported +without extension states (`loadExts := false`). -/ +def kindOf (env : Environment) (name : Name) (info : ConstantInfo) : Option String := + match info with + | .thmInfo _ => some "theorem" + | .defnInfo _ => some "def" + | .opaqueInfo _ => some "opaque" + | .axiomInfo _ => some "axiom" + | .inductInfo _ => if isStructure env name then some "structure" else some "inductive" + | _ => none + +/-- Mirrors the doc-gen4 / import-graph blacklist for generated declarations. -/ +def isGenerated (env : Environment) (name : Name) : CoreM Bool := do + let display := privateToUserName name + if display.isInternalDetail then return true + if isAuxRecursor env name || isNoConfusion env name then return true + if (← isRec name) || (← Meta.isMatcher name) then return true + if (env.getProjectionFnInfo? name).isSome then return true + -- `declare_syntax_cat` generates a quotation parser `.quot`; the type + -- guard keeps genuine user definitions that happen to be named `quot`. + if let .str _ "quot" := display then + if let some info := env.find? name then + if info.type.isConstOf ``Lean.ParserDescr + || info.type.isConstOf ``Lean.TrailingParserDescr then + return true + return false + +/-- Should `name` appear as a node of the exposition? -/ +def isExposed (env : Environment) (name : Name) (info : ConstantInfo) : CoreM Bool := do + let some moduleIdx := env.getModuleIdxFor? name | return false + unless isPoolModule env.header.moduleNames[moduleIdx.toNat]! do return false + if (kindOf env name info).isNone then return false + if ← isGenerated env name then return false + return (← findDeclarationRanges? name).isSome + +/-- Constants a declaration mentions, including constructor signatures for +inductives/structures (field types live in the constructor's type). -/ +def directUses (env : Environment) (info : ConstantInfo) : Array Name := + match info with + | .inductInfo v => + v.ctors.foldl (init := info.getUsedConstantsAsSet) + (fun acc c => match env.find? c with + | some ci => acc.insertMany ci.getUsedConstantsAsSet + | none => acc) + |>.toArray + | _ => info.getUsedConstantsAsSet.toArray + +/-- Expand the used-constant set of `info`, tunnelling through generated pool +auxiliaries, until exposed pool declarations (edges) or non-pool constants +(externals) are reached. -/ +def resolveDeps (env : Environment) (self : Name) (info : ConstantInfo) + (exposed : NameSet) : NameSet × Nat := Id.run do + let mut edges : NameSet := {} + let mut externals : NameSet := {} + let mut visited : NameSet := {} + let mut stack : Array Name := directUses env info + while h : stack.size > 0 do + let c := stack[stack.size - 1] + stack := stack.pop + if c == self || visited.contains c then continue + visited := visited.insert c + if exposed.contains c then + edges := edges.insert c + continue + let inPool := match env.getModuleIdxFor? c with + | some idx => isPoolModule env.header.moduleNames[idx.toNat]! + | none => false + if inPool then + if let some ci := env.find? c then + stack := stack ++ directUses env ci + else + externals := externals.insert c + return (edges, externals.size) + +def escapeName (n : Name) : String := n.toString + +def declJson (env : Environment) (name : Name) (info : ConstantInfo) + (exposed : NameSet) : CoreM (Option Json) := do + let some ranges ← findDeclarationRanges? name | return none + let some kind := kindOf env name info | return none + let some moduleIdx := env.getModuleIdxFor? name | return none + let module := env.header.moduleNames[moduleIdx.toNat]! + let display := privateToUserName name + let doc ← findDocString? env name + let (edges, extCount) := resolveDeps env name info exposed + let r := ranges.range + let s := ranges.selectionRange + return some <| Json.mkObj <| [ + ("id", Json.str (escapeName name)), + ("n", Json.str (escapeName display)), + ("m", Json.str module.toString), + ("k", Json.str kind), + ("r", toJson [r.pos.line, r.pos.column, r.endPos.line, r.endPos.column]), + ("s", toJson [s.pos.line, s.pos.column]), + ("deps", Json.arr (edges.toArray.map (Json.str ∘ escapeName))), + ("ext", Json.num extCount) + ] ++ (if isPrivateName name then [("p", Json.bool true)] else []) + ++ (match doc with | some d => [("d", Json.str d)] | none => []) + +def extract (outPath : System.FilePath) : CoreM Unit := do + let env ← getEnv + -- Pass 1: collect the exposed node set. + let mut exposed : NameSet := {} + let mut names : Array Name := #[] + for moduleIdx in [0:env.header.moduleNames.size] do + unless isPoolModule env.header.moduleNames[moduleIdx]! do continue + let moduleData : ModuleData := env.header.moduleData[moduleIdx]! + for name in moduleData.constNames do + -- A constant can appear in several modules' `constNames` when two files + -- declare it textually; keep the first occurrence only. + if exposed.contains name then continue + let some info := env.find? name | continue + if ← isExposed env name info then + exposed := exposed.insert name + names := names.push name + -- Pass 2: emit one JSON line per exposed declaration. + IO.FS.createDirAll (outPath.parent.getD ".") + let handle ← IO.FS.Handle.mk outPath .write + for name in names do + let some info := env.find? name | continue + if let some json ← declJson env name info exposed then + handle.putStrLn json.compress + handle.flush + IO.println s!"exposition: wrote {names.size} declarations to {outPath}" + +end Exposition + +def main (args : List String) : IO UInt32 := do + let outPath := args[0]?.getD "exposition-dump.jsonl" + -- Further arguments override the imported modules (default: the whole pool); + -- useful for testing against a partially built tree. + let modules := if args.length > 1 then args.drop 1 |>.map (·.toName) else [Exposition.poolRoot] + Lean.initSearchPath (← Lean.findSysroot) + let imports := modules.toArray.map fun module => ({ module } : Lean.Import) + let env ← Lean.importModules imports {} (trustLevel := 1024) + let coreContext : Lean.Core.Context := { + fileName := "", + fileMap := default, + maxHeartbeats := 0 + } + let (result, _) ← (Exposition.extract outPath).toIO coreContext { env } + let _ := result + return 0