diff --git a/.gitignore b/.gitignore index 8e9bf91e72..0505ec9126 100644 --- a/.gitignore +++ b/.gitignore @@ -12,5 +12,5 @@ __pycache__/ # Aggregator: the Reservoir manifest is fetched on demand and kept # locally only. Curated per-package files in candidates/packages/ # are the source of truth that gets committed. -/aggregator/candidates/raw_data/ +/candidates/raw_data/ .claude/ diff --git a/aggregator/candidates/CRITERIA.txt b/candidates/CRITERIA.txt similarity index 100% rename from aggregator/candidates/CRITERIA.txt rename to candidates/CRITERIA.txt diff --git a/aggregator/candidates/README.md b/candidates/README.md similarity index 100% rename from aggregator/candidates/README.md rename to candidates/README.md diff --git a/aggregator/candidates/decisions.jsonl b/candidates/decisions.jsonl similarity index 100% rename from aggregator/candidates/decisions.jsonl rename to candidates/decisions.jsonl diff --git a/aggregator/candidates/manual.txt b/candidates/manual.txt similarity index 100% rename from aggregator/candidates/manual.txt rename to candidates/manual.txt diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py index b9529aea0a..1d3c60c25c 100644 --- a/python/lean_pool/aggregator/__main__.py +++ b/python/lean_pool/aggregator/__main__.py @@ -34,7 +34,7 @@ ) REPO_ROOT = Path(__file__).resolve().parents[3] -CANDIDATES_DIR = REPO_ROOT / "aggregator" / "candidates" +CANDIDATES_DIR = REPO_ROOT / "candidates" DEFAULT_MANIFEST = CANDIDATES_DIR / "raw_data" / "manifest.json" DEFAULT_MANUAL_LIST = CANDIDATES_DIR / "manual.txt" DEFAULT_MANUAL_DATA = CANDIDATES_DIR / "raw_data" / "manual_packages.json" diff --git a/python/lean_pool/aggregator/cloner.py b/python/lean_pool/aggregator/cloner.py index 398fbd288f..5c95cf56cb 100644 --- a/python/lean_pool/aggregator/cloner.py +++ b/python/lean_pool/aggregator/cloner.py @@ -6,7 +6,7 @@ clone is typically a few hundred KB. The cache lives at -``aggregator/candidates/raw_data/clones///``, keyed by the +``candidates/raw_data/clones///``, keyed by the package's canonical GitHub key (lowercased, ``.lean``/``.git`` suffix stripped) so two manifest entries pointing at the same repo (e.g. Reservoir's ``leanprover-community/mathlib`` and a manual entry's diff --git a/python/lean_pool/aggregator/manual.py b/python/lean_pool/aggregator/manual.py index e733a8a68a..e861e5452a 100644 --- a/python/lean_pool/aggregator/manual.py +++ b/python/lean_pool/aggregator/manual.py @@ -8,8 +8,8 @@ metadata from the GitHub REST API at the same time we fetch the Reservoir manifest. -The list lives at ``aggregator/candidates/manual.txt`` — one GitHub URL -per line, ``#`` comments and blank lines allowed. +The list lives at ``candidates/manual.txt`` — one GitHub URL per line, +``#`` comments and blank lines allowed. """ from __future__ import annotations diff --git a/python/lean_pool/aggregator/render.py b/python/lean_pool/aggregator/render.py index 0f1856f639..3e00ac9ea6 100644 --- a/python/lean_pool/aggregator/render.py +++ b/python/lean_pool/aggregator/render.py @@ -6,7 +6,7 @@ one source of truth for the descriptive fields. The renderer replaces the content between two HTML comment markers in -``aggregator/candidates/README.md``: +``candidates/README.md``: ...generated table goes here...