From 8db29fc761a3c6a8f1de02b9f276cf513fe9d499 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 10:43:54 -0700
Subject: [PATCH 1/8] Draft aggregator subpackage that fetches the Reservoir
 manifest

---
 python/lean_pool/aggregator/__init__.py  |  1 +
 python/lean_pool/aggregator/__main__.py  | 62 ++++++++++++++++++++++++
 python/lean_pool/aggregator/reservoir.py | 46 ++++++++++++++++++
 3 files changed, 109 insertions(+)
 create mode 100644 python/lean_pool/aggregator/__init__.py
 create mode 100644 python/lean_pool/aggregator/__main__.py
 create mode 100644 python/lean_pool/aggregator/reservoir.py

diff --git a/python/lean_pool/aggregator/__init__.py b/python/lean_pool/aggregator/__init__.py
new file mode 100644
index 0000000000..a1a84e6072
--- /dev/null
+++ b/python/lean_pool/aggregator/__init__.py
@@ -0,0 +1 @@
+"""Aggregation tooling that fetches Reservoir data and filters Lean packages."""
diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
new file mode 100644
index 0000000000..135353a860
--- /dev/null
+++ b/python/lean_pool/aggregator/__main__.py
@@ -0,0 +1,62 @@
+"""CLI entry point for the aggregator.
+
+Run with ``uv run python -m lean_pool.aggregator`` from ``python/``.
+"""
+
+import argparse
+import logging
+import sys
+from pathlib import Path
+
+from lean_pool.aggregator.reservoir import (
+    MANIFEST_URL,
+    fetch_manifest,
+    save_manifest,
+)
+
+
+def main() -> int:
+    """Download the Reservoir manifest and print a summary.
+
+    Returns:
+        Process exit code (0 on success).
+    """
+    parser = argparse.ArgumentParser(
+        description="Fetch the Reservoir manifest and summarize it."
+    )
+    parser.add_argument(
+        "--url",
+        default=MANIFEST_URL,
+        help=f"Manifest URL (default: {MANIFEST_URL})",
+    )
+    parser.add_argument(
+        "--output",
+        type=Path,
+        default=Path("manifest.json"),
+        help="Where to save the downloaded manifest (default: ./manifest.json)",
+    )
+    args = parser.parse_args()
+
+    logging.basicConfig(level=logging.INFO, format="%(message)s")
+
+    manifest = fetch_manifest(args.url)
+    save_manifest(manifest, args.output)
+
+    packages = manifest.get("packages", [])
+    print(f"Bundled at: {manifest.get('bundledAt')}")
+    print(f"Toolchains: {len(manifest.get('toolchains', []))}")
+    print(f"Packages:   {len(packages)}")
+    print(f"Aliases:    {len(manifest.get('packageAliases', {}))}")
+    print(f"Saved to:   {args.output}")
+
+    if packages:
+        print("\nTop 10 by stars:")
+        top = sorted(packages, key=lambda p: p.get("stars", 0), reverse=True)[:10]
+        for pkg in top:
+            print(f"  {pkg.get('stars', 0):>5}  {pkg['fullName']}")
+
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/python/lean_pool/aggregator/reservoir.py b/python/lean_pool/aggregator/reservoir.py
new file mode 100644
index 0000000000..22e3b18585
--- /dev/null
+++ b/python/lean_pool/aggregator/reservoir.py
@@ -0,0 +1,46 @@
+"""Fetch the Reservoir package manifest.
+
+The Reservoir website bundles every indexed Lean package into a single
+JSON file at ``https://reservoir.lean-lang.org/index/manifest.json``.
+That file is the canonical input for aggregation: it contains every
+package's metadata, recent versions, and per-toolchain build results.
+"""
+
+from __future__ import annotations
+
+import json
+import logging
+from pathlib import Path
+from typing import Any
+from urllib.request import urlopen
+
+logger = logging.getLogger(__name__)
+
+MANIFEST_URL = "https://reservoir.lean-lang.org/index/manifest.json"
+
+
+def fetch_manifest(url: str = MANIFEST_URL) -> dict[str, Any]:
+    """Download and parse the Reservoir manifest JSON.
+
+    Args:
+        url: The URL to fetch the manifest from.
+
+    Returns:
+        The parsed manifest as a dictionary with keys ``bundledAt``,
+        ``toolchains``, ``packages``, and ``packageAliases``.
+    """
+    logger.info("Fetching %s", url)
+    with urlopen(url) as response:
+        return json.load(response)
+
+
+def save_manifest(manifest: dict[str, Any], path: Path) -> None:
+    """Write the manifest to disk as pretty-printed JSON.
+
+    Args:
+        manifest: The parsed manifest.
+        path: The output file path; parent directories are created.
+    """
+    path.parent.mkdir(parents=True, exist_ok=True)
+    with path.open("w") as f:
+        json.dump(manifest, f, indent=2)

From d6ed0763901d56614eef43a8468f3d93a0b1db64 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:00:26 -0700
Subject: [PATCH 2/8] Address review: add fetch timeout and ignore cache
 directory

- Pass a 60s timeout to urlopen so a stalled connection cannot hang the CLI.
- Default --output to cache/manifest.json and gitignore cache/ so the
  53 MB Reservoir file does not land at the repo root.
---
 .gitignore                               | 1 +
 python/lean_pool/aggregator/__main__.py  | 4 ++--
 python/lean_pool/aggregator/reservoir.py | 8 ++++++--
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index b52e204e72..dca4334122 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,4 +6,5 @@ __pycache__/
 .venv/
 .ruff_cache/
 .pytest_cache/
+cache/
 
diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index 135353a860..f35755ec08 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -32,8 +32,8 @@ def main() -> int:
     parser.add_argument(
         "--output",
         type=Path,
-        default=Path("manifest.json"),
-        help="Where to save the downloaded manifest (default: ./manifest.json)",
+        default=Path("cache/manifest.json"),
+        help="Where to save the downloaded manifest (default: ./cache/manifest.json)",
     )
     args = parser.parse_args()
 
diff --git a/python/lean_pool/aggregator/reservoir.py b/python/lean_pool/aggregator/reservoir.py
index 22e3b18585..be054700b0 100644
--- a/python/lean_pool/aggregator/reservoir.py
+++ b/python/lean_pool/aggregator/reservoir.py
@@ -17,20 +17,24 @@
 logger = logging.getLogger(__name__)
 
 MANIFEST_URL = "https://reservoir.lean-lang.org/index/manifest.json"
+DEFAULT_TIMEOUT_SECONDS = 60
 
 
-def fetch_manifest(url: str = MANIFEST_URL) -> dict[str, Any]:
+def fetch_manifest(
+    url: str = MANIFEST_URL, timeout: float = DEFAULT_TIMEOUT_SECONDS
+) -> dict[str, Any]:
     """Download and parse the Reservoir manifest JSON.
 
     Args:
         url: The URL to fetch the manifest from.
+        timeout: Socket timeout in seconds for the HTTP request.
 
     Returns:
         The parsed manifest as a dictionary with keys ``bundledAt``,
         ``toolchains``, ``packages``, and ``packageAliases``.
     """
     logger.info("Fetching %s", url)
-    with urlopen(url) as response:
+    with urlopen(url, timeout=timeout) as response:
         return json.load(response)
 
 

From 894ae45d0939a02e6d94e1a96fe124b437a104b9 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:14:44 -0700
Subject: [PATCH 3/8] Align aggregator with contributing guidelines

- Rename abbreviated locals (pkg/p/f) to package/output_file per the
  no-abbreviations naming rule.
- Add tests for fetch_manifest (mocked urlopen) and save_manifest
  (round-trip to disk) under python/tests/.
---
 python/lean_pool/aggregator/__main__.py  |  8 +++--
 python/lean_pool/aggregator/reservoir.py |  4 +--
 python/tests/test_reservoir.py           | 41 ++++++++++++++++++++++++
 3 files changed, 48 insertions(+), 5 deletions(-)
 create mode 100644 python/tests/test_reservoir.py

diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index f35755ec08..0c77cbd2a3 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -51,9 +51,11 @@ def main() -> int:
 
     if packages:
         print("\nTop 10 by stars:")
-        top = sorted(packages, key=lambda p: p.get("stars", 0), reverse=True)[:10]
-        for pkg in top:
-            print(f"  {pkg.get('stars', 0):>5}  {pkg['fullName']}")
+        top = sorted(
+            packages, key=lambda package: package.get("stars", 0), reverse=True
+        )[:10]
+        for package in top:
+            print(f"  {package.get('stars', 0):>5}  {package['fullName']}")
 
     return 0
 
diff --git a/python/lean_pool/aggregator/reservoir.py b/python/lean_pool/aggregator/reservoir.py
index be054700b0..9cb585b1d7 100644
--- a/python/lean_pool/aggregator/reservoir.py
+++ b/python/lean_pool/aggregator/reservoir.py
@@ -46,5 +46,5 @@ def save_manifest(manifest: dict[str, Any], path: Path) -> None:
         path: The output file path; parent directories are created.
     """
     path.parent.mkdir(parents=True, exist_ok=True)
-    with path.open("w") as f:
-        json.dump(manifest, f, indent=2)
+    with path.open("w") as output_file:
+        json.dump(manifest, output_file, indent=2)
diff --git a/python/tests/test_reservoir.py b/python/tests/test_reservoir.py
new file mode 100644
index 0000000000..f8f1ebcba8
--- /dev/null
+++ b/python/tests/test_reservoir.py
@@ -0,0 +1,41 @@
+"""Tests for the Reservoir manifest fetcher and writer."""
+
+from __future__ import annotations
+
+import io
+import json
+from pathlib import Path
+from unittest.mock import patch
+
+from lean_pool.aggregator.reservoir import (
+    MANIFEST_URL,
+    fetch_manifest,
+    save_manifest,
+)
+
+
+def test_save_manifest_round_trip(tmp_path: Path) -> None:
+    """save_manifest writes JSON that can be read back identically."""
+    manifest = {"bundledAt": "2026-05-09T00:00:00Z", "packages": [{"stars": 3}]}
+    output_path = tmp_path / "nested" / "manifest.json"
+
+    save_manifest(manifest, output_path)
+
+    assert output_path.exists()
+    assert json.loads(output_path.read_text()) == manifest
+
+
+def test_fetch_manifest_parses_response() -> None:
+    """fetch_manifest decodes JSON returned by urlopen."""
+    payload = {"bundledAt": "now", "packages": []}
+    response = io.BytesIO(json.dumps(payload).encode())
+    response.__enter__ = lambda self: self  # type: ignore[method-assign]
+    response.__exit__ = lambda self, *exc: None  # type: ignore[method-assign]
+
+    with patch(
+        "lean_pool.aggregator.reservoir.urlopen", return_value=response
+    ) as mock_urlopen:
+        result = fetch_manifest(timeout=5)
+
+    assert result == payload
+    mock_urlopen.assert_called_once_with(MANIFEST_URL, timeout=5)

From 177f99754523979286080dc145bcdc090320ba7e Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:16:07 -0700
Subject: [PATCH 4/8] Use logger instead of print in aggregator CLI

Match the no-print convention used in reservoir.py: route the manifest
summary and top-stars listing through a module logger so the CLI uses
one output channel.
---
 python/lean_pool/aggregator/__main__.py | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index 0c77cbd2a3..cf5124acaa 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -14,9 +14,11 @@
     save_manifest,
 )
 
+logger = logging.getLogger(__name__)
+
 
 def main() -> int:
-    """Download the Reservoir manifest and print a summary.
+    """Download the Reservoir manifest and log a summary.
 
     Returns:
         Process exit code (0 on success).
@@ -43,19 +45,20 @@ def main() -> int:
     save_manifest(manifest, args.output)
 
     packages = manifest.get("packages", [])
-    print(f"Bundled at: {manifest.get('bundledAt')}")
-    print(f"Toolchains: {len(manifest.get('toolchains', []))}")
-    print(f"Packages:   {len(packages)}")
-    print(f"Aliases:    {len(manifest.get('packageAliases', {}))}")
-    print(f"Saved to:   {args.output}")
+    logger.info("Bundled at: %s", manifest.get("bundledAt"))
+    logger.info("Toolchains: %d", len(manifest.get("toolchains", [])))
+    logger.info("Packages:   %d", len(packages))
+    logger.info("Aliases:    %d", len(manifest.get("packageAliases", {})))
+    logger.info("Saved to:   %s", args.output)
 
     if packages:
-        print("\nTop 10 by stars:")
+        logger.info("")
+        logger.info("Top 10 by stars:")
         top = sorted(
             packages, key=lambda package: package.get("stars", 0), reverse=True
         )[:10]
         for package in top:
-            print(f"  {package.get('stars', 0):>5}  {package['fullName']}")
+            logger.info("  %5d  %s", package.get("stars", 0), package["fullName"])
 
     return 0
 

From 8e9ee141140657277bbecfd9cb52e8c9f6fa9855 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:18:49 -0700
Subject: [PATCH 5/8] Mirror source layout under tests/

Move test_reservoir.py into tests/aggregator/ so the test tree mirrors
lean_pool/aggregator/. Adds tests/aggregator/__init__.py.
---
 python/tests/aggregator/__init__.py             | 0
 python/tests/{ => aggregator}/test_reservoir.py | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 python/tests/aggregator/__init__.py
 rename python/tests/{ => aggregator}/test_reservoir.py (100%)

diff --git a/python/tests/aggregator/__init__.py b/python/tests/aggregator/__init__.py
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/python/tests/test_reservoir.py b/python/tests/aggregator/test_reservoir.py
similarity index 100%
rename from python/tests/test_reservoir.py
rename to python/tests/aggregator/test_reservoir.py

From d090196de682e54d40b0224f7121e233b8a92194 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:21:35 -0700
Subject: [PATCH 6/8] Switch CLI to click and stop logging summary to console

The aggregator CLI now just fetches the manifest and writes it to disk;
the summary stats and top-stars listing are gone. Replace argparse with
click for option parsing and add click as a runtime dependency.
---
 python/lean_pool/aggregator/__main__.py | 71 ++++++++-----------------
 python/pyproject.toml                   |  4 +-
 python/uv.lock                          | 18 ++++++-
 3 files changed, 41 insertions(+), 52 deletions(-)

diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index cf5124acaa..5048fd84f3 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -3,65 +3,36 @@
 Run with ``uv run python -m lean_pool.aggregator`` from ``python/``.
 """
 
-import argparse
-import logging
-import sys
 from pathlib import Path
 
+import click
+
 from lean_pool.aggregator.reservoir import (
     MANIFEST_URL,
     fetch_manifest,
     save_manifest,
 )
 
-logger = logging.getLogger(__name__)
-
-
-def main() -> int:
-    """Download the Reservoir manifest and log a summary.
-
-    Returns:
-        Process exit code (0 on success).
-    """
-    parser = argparse.ArgumentParser(
-        description="Fetch the Reservoir manifest and summarize it."
-    )
-    parser.add_argument(
-        "--url",
-        default=MANIFEST_URL,
-        help=f"Manifest URL (default: {MANIFEST_URL})",
-    )
-    parser.add_argument(
-        "--output",
-        type=Path,
-        default=Path("cache/manifest.json"),
-        help="Where to save the downloaded manifest (default: ./cache/manifest.json)",
-    )
-    args = parser.parse_args()
-
-    logging.basicConfig(level=logging.INFO, format="%(message)s")
 
-    manifest = fetch_manifest(args.url)
-    save_manifest(manifest, args.output)
-
-    packages = manifest.get("packages", [])
-    logger.info("Bundled at: %s", manifest.get("bundledAt"))
-    logger.info("Toolchains: %d", len(manifest.get("toolchains", [])))
-    logger.info("Packages:   %d", len(packages))
-    logger.info("Aliases:    %d", len(manifest.get("packageAliases", {})))
-    logger.info("Saved to:   %s", args.output)
-
-    if packages:
-        logger.info("")
-        logger.info("Top 10 by stars:")
-        top = sorted(
-            packages, key=lambda package: package.get("stars", 0), reverse=True
-        )[:10]
-        for package in top:
-            logger.info("  %5d  %s", package.get("stars", 0), package["fullName"])
-
-    return 0
+@click.command()
+@click.option(
+    "--url",
+    default=MANIFEST_URL,
+    show_default=True,
+    help="Reservoir manifest URL.",
+)
+@click.option(
+    "--output",
+    type=click.Path(dir_okay=False, path_type=Path),
+    default=Path("cache/manifest.json"),
+    show_default=True,
+    help="Where to save the downloaded manifest.",
+)
+def main(url: str, output: Path) -> None:
+    """Download the Reservoir manifest and save it to disk."""
+    manifest = fetch_manifest(url)
+    save_manifest(manifest, output)
 
 
 if __name__ == "__main__":
-    sys.exit(main())
+    main()
diff --git a/python/pyproject.toml b/python/pyproject.toml
index 2789a3c227..14b2db8788 100644
--- a/python/pyproject.toml
+++ b/python/pyproject.toml
@@ -4,7 +4,9 @@ version = "0.0.1"
 description = "Python tooling for the lean-pool repository (Reservoir aggregation, candidate filtering)."
 readme = "README.md"
 requires-python = ">=3.13"
-dependencies = []
+dependencies = [
+    "click>=8.1",
+]
 
 
 [dependency-groups]
diff --git a/python/uv.lock b/python/uv.lock
index 9dba789105..78f8b7c559 100644
--- a/python/uv.lock
+++ b/python/uv.lock
@@ -1,5 +1,5 @@
 version = 1
-revision = 3
+revision = 2
 requires-python = ">=3.13"
 
 [[package]]
@@ -32,6 +32,18 @@ wheels = [
     { url = "https://files.pythonhosted.org/packages/22/30/7cd8fdcdfbc5b869528b079bfb76dcdf6056b1a2097a662e5e8c04f42965/certifi-2026.4.22-py3-none-any.whl", hash = "sha256:3cb2210c8f88ba2318d29b0388d1023c8492ff72ecdde4ebdaddbb13a31b1c4a", size = 135707, upload-time = "2026-04-22T11:26:09.372Z" },
 ]
 
+[[package]]
+name = "click"
+version = "8.3.3"
+source = { registry = "https://pypi.org/simple" }
+dependencies = [
+    { name = "colorama", marker = "sys_platform == 'win32'" },
+]
+sdist = { url = "https://files.pythonhosted.org/packages/bb/63/f9e1ea081ce35720d8b92acde70daaedace594dc93b693c869e0d5910718/click-8.3.3.tar.gz", hash = "sha256:398329ad4837b2ff7cbe1dd166a4c0f8900c3ca3a218de04466f38f6497f18a2", size = 328061, upload-time = "2026-04-22T15:11:27.506Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/ae/44/c1221527f6a71a01ec6fbad7fa78f1d50dfa02217385cf0fa3eec7087d59/click-8.3.3-py3-none-any.whl", hash = "sha256:a2bf429bb3033c89fa4936ffb35d5cb471e3719e1f3c8a7c3fff0b8314305613", size = 110502, upload-time = "2026-04-22T15:11:25.044Z" },
+]
+
 [[package]]
 name = "colorama"
 version = "0.4.6"
@@ -232,6 +244,9 @@ wheels = [
 name = "lean-pool-tools"
 version = "0.0.1"
 source = { virtual = "." }
+dependencies = [
+    { name = "click" },
+]
 
 [package.dev-dependencies]
 dev = [
@@ -246,6 +261,7 @@ test = [
 ]
 
 [package.metadata]
+requires-dist = [{ name = "click", specifier = ">=8.1" }]
 
 [package.metadata.requires-dev]
 dev = [{ name = "ruff", specifier = ">=0.9" }]

From 99b35e54627db91c2ea1f3e52fb8c25956c862a2 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:24:10 -0700
Subject: [PATCH 7/8] Type the manifest as TypedDict and echo a one-line
 summary

- Define ReservoirManifest TypedDict for fetch_manifest / save_manifest
  signatures instead of dict[str, Any].
- Echo "Saved N packages to <path>" once on success so users see what
  landed without the previous verbose summary.
---
 python/lean_pool/aggregator/__main__.py  |  1 +
 python/lean_pool/aggregator/reservoir.py | 19 ++++++++++++++-----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py
index 5048fd84f3..de236a4299 100644
--- a/python/lean_pool/aggregator/__main__.py
+++ b/python/lean_pool/aggregator/__main__.py
@@ -32,6 +32,7 @@ def main(url: str, output: Path) -> None:
     """Download the Reservoir manifest and save it to disk."""
     manifest = fetch_manifest(url)
     save_manifest(manifest, output)
+    click.echo(f"Saved {len(manifest['packages'])} packages to {output}")
 
 
 if __name__ == "__main__":
diff --git a/python/lean_pool/aggregator/reservoir.py b/python/lean_pool/aggregator/reservoir.py
index 9cb585b1d7..8cc6756d92 100644
--- a/python/lean_pool/aggregator/reservoir.py
+++ b/python/lean_pool/aggregator/reservoir.py
@@ -11,7 +11,7 @@
 import json
 import logging
 from pathlib import Path
-from typing import Any
+from typing import Any, TypedDict
 from urllib.request import urlopen
 
 logger = logging.getLogger(__name__)
@@ -20,9 +20,18 @@
 DEFAULT_TIMEOUT_SECONDS = 60
 
 
+class ReservoirManifest(TypedDict):
+    """Top-level shape of the Reservoir manifest JSON."""
+
+    bundledAt: str
+    toolchains: list[dict[str, Any]]
+    packages: list[dict[str, Any]]
+    packageAliases: dict[str, str]
+
+
 def fetch_manifest(
     url: str = MANIFEST_URL, timeout: float = DEFAULT_TIMEOUT_SECONDS
-) -> dict[str, Any]:
+) -> ReservoirManifest:
     """Download and parse the Reservoir manifest JSON.
 
     Args:
@@ -30,15 +39,15 @@ def fetch_manifest(
         timeout: Socket timeout in seconds for the HTTP request.
 
     Returns:
-        The parsed manifest as a dictionary with keys ``bundledAt``,
-        ``toolchains``, ``packages``, and ``packageAliases``.
+        The parsed manifest with ``bundledAt``, ``toolchains``,
+        ``packages``, and ``packageAliases`` fields.
     """
     logger.info("Fetching %s", url)
     with urlopen(url, timeout=timeout) as response:
         return json.load(response)
 
 
-def save_manifest(manifest: dict[str, Any], path: Path) -> None:
+def save_manifest(manifest: ReservoirManifest, path: Path) -> None:
     """Write the manifest to disk as pretty-printed JSON.
 
     Args:

From e5eb7f64757131bd7418f331fdbd1be0ab0d991b Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:28:30 -0700
Subject: [PATCH 8/8] Mirror Reservoir's TypedDict hierarchy for the manifest

Replace the loose ReservoirManifest with a full hierarchy that
matches Reservoir's own type definitions in scripts/utils/
(package.py, manifest.py, toolchain.py): Package, PackageVersion,
PackageSource, Build / BuildResult, Dependency / Dependent,
Toolchain. The decoded manifest is now statically typed end to end
instead of relying on dict[str, Any] for nested structures.
---
 python/lean_pool/aggregator/reservoir.py | 116 ++++++++++++++++++++++-
 1 file changed, 111 insertions(+), 5 deletions(-)

diff --git a/python/lean_pool/aggregator/reservoir.py b/python/lean_pool/aggregator/reservoir.py
index 8cc6756d92..05ebadbea8 100644
--- a/python/lean_pool/aggregator/reservoir.py
+++ b/python/lean_pool/aggregator/reservoir.py
@@ -1,9 +1,14 @@
-"""Fetch the Reservoir package manifest.
+"""Fetch and decode the Reservoir package manifest.
 
 The Reservoir website bundles every indexed Lean package into a single
 JSON file at ``https://reservoir.lean-lang.org/index/manifest.json``.
 That file is the canonical input for aggregation: it contains every
 package's metadata, recent versions, and per-toolchain build results.
+
+The TypedDicts below mirror Reservoir's own type definitions in
+``reservoir/scripts/utils/`` (``package.py``, ``manifest.py``,
+``toolchain.py``) so the decoded manifest is statically typed end to
+end, not just ``dict[str, Any]``.
 """
 
 from __future__ import annotations
@@ -11,7 +16,7 @@
 import json
 import logging
 from pathlib import Path
-from typing import Any, TypedDict
+from typing import TypedDict
 from urllib.request import urlopen
 
 logger = logging.getLogger(__name__)
@@ -20,12 +25,113 @@
 DEFAULT_TIMEOUT_SECONDS = 60
 
 
+class PackageSource(TypedDict, total=False):
+    """A source location for a package. Most entries are GitHub repos."""
+
+    type: str
+    host: str
+    id: str
+    fullName: str
+    repoUrl: str
+    gitUrl: str
+    defaultBranch: str
+
+
+class BuildResult(TypedDict):
+    """Outcome of building a package against a single toolchain."""
+
+    built: bool | None
+    tested: bool | None
+    toolchain: str
+    requiredUpdate: bool | None
+    archiveSize: int | None
+    archiveHash: str | None
+    runAt: str
+    url: str | None
+
+
+class Build(BuildResult):
+    """A build result tagged with the source revision it ran against."""
+
+    revision: str
+
+
+class DependencyBase(TypedDict):
+    """Fields shared by outgoing dependencies and incoming dependents."""
+
+    type: str
+    name: str
+    scope: str | None
+    version: str
+    transitive: bool | None
+    rev: str | None
+    inputRev: str | None
+    url: str | None
+
+
+class Dependency(DependencyBase, total=False):
+    """An outgoing dependency. ``fullName`` is set when resolvable."""
+
+    fullName: str
+
+
+class Dependent(DependencyBase):
+    """A package that depends on this one. ``fullName`` is always set."""
+
+    fullName: str
+
+
+class PackageVersion(TypedDict):
+    """A released version of a package, as serialized in the manifest."""
+
+    version: str
+    revision: str
+    date: str
+    tag: str | None
+    toolchain: str | None
+    platformIndependent: bool | None
+    license: str | None
+    licenseFiles: list[str]
+    readmeFile: str | None
+    dependencies: list[Dependency]
+
+
+class Package(TypedDict):
+    """A package as published in the Reservoir manifest."""
+
+    name: str
+    owner: str
+    fullName: str
+    description: str | None
+    keywords: list[str] | None
+    homepage: str | None
+    license: str | None
+    createdAt: str
+    updatedAt: str
+    stars: int
+    sources: list[PackageSource]
+    versions: list[PackageVersion]
+    dependents: list[Dependent]
+    builds: list[Build]
+
+
+class Toolchain(TypedDict):
+    """An indexed Lean toolchain release."""
+
+    name: str
+    version: int | None
+    tag: str
+    date: str
+    releaseUrl: str
+    prerelease: bool
+
+
 class ReservoirManifest(TypedDict):
-    """Top-level shape of the Reservoir manifest JSON."""
+    """The decoded ``manifest.json`` produced by Reservoir's bundler."""
 
     bundledAt: str
-    toolchains: list[dict[str, Any]]
-    packages: list[dict[str, Any]]
+    toolchains: list[Toolchain]
+    packages: list[Package]
     packageAliases: dict[str, str]