Add Reservoir manifest fetcher to aggregator subpackage

.gitignore

@@ -6,4 +6,5 @@ __pycache__/
 .venv/
 .ruff_cache/
 .pytest_cache/
+cache/
 

python/lean_pool/aggregator/__init__.py

@@ -0,0 +1 @@
+"""Aggregation tooling that fetches Reservoir data and filters Lean packages."""

python/lean_pool/aggregator/__main__.py

@@ -0,0 +1,39 @@
+"""CLI entry point for the aggregator.
+
+Run with ``uv run python -m lean_pool.aggregator`` from ``python/``.
+"""
+
+from pathlib import Path
+
+import click
+
+from lean_pool.aggregator.reservoir import (
+    MANIFEST_URL,
+    fetch_manifest,
+    save_manifest,
+)
+
+
+@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)
+    click.echo(f"Saved {len(manifest['packages'])} packages to {output}")
+
+
+if __name__ == "__main__":
+    main()

python/lean_pool/aggregator/reservoir.py

@@ -0,0 +1,165 @@
+"""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
+
+import json
+import logging
+from pathlib import Path
+from typing import TypedDict
+from urllib.request import urlopen
+
+logger = logging.getLogger(__name__)
+
+MANIFEST_URL = "https://reservoir.lean-lang.org/index/manifest.json"
+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):
+    """The decoded ``manifest.json`` produced by Reservoir's bundler."""
+
+    bundledAt: str
+    toolchains: list[Toolchain]
+    packages: list[Package]
+    packageAliases: dict[str, str]
+
+
+def fetch_manifest(
+    url: str = MANIFEST_URL, timeout: float = DEFAULT_TIMEOUT_SECONDS
+) -> ReservoirManifest:
+    """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 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: ReservoirManifest, 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 output_file:
+        json.dump(manifest, output_file, indent=2)

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]

python/tests/aggregator/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)