From e1611cd6e998222dc17433ce133af6bba1e9b99b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 23 Jun 2026 23:59:23 -0700 Subject: [PATCH] Add auto-updating README stats (project count + Lean LOC) Adds `lean_pool.stats`, which derives the number of pooled projects (from LeanPool/projects.yml) and total lines of Lean (from the LeanPool/ tree) and rewrites a marked block in README.md. A new `readme-stats.yml` workflow refreshes and commits the block on pushes to main that touch Lean source, the stats module, or the workflow. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/readme-stats.yml | 49 ++++++++ README.md | 6 + python/lean_pool/stats.py | 176 +++++++++++++++++++++++++++++ python/tests/test_stats.py | 104 +++++++++++++++++ 4 files changed, 335 insertions(+) create mode 100644 .github/workflows/readme-stats.yml create mode 100644 python/lean_pool/stats.py create mode 100644 python/tests/test_stats.py diff --git a/.github/workflows/readme-stats.yml b/.github/workflows/readme-stats.yml new file mode 100644 index 0000000000..6734c37f92 --- /dev/null +++ b/.github/workflows/readme-stats.yml @@ -0,0 +1,49 @@ +name: README stats + +on: + push: + branches: + - main + # Only the inputs to the stats can change them. The refresh commit + # below touches README.md only, which is NOT in this list, so it + # cannot re-trigger this workflow (no commit loop). + paths: + - 'LeanPool/**' + - 'python/lean_pool/stats.py' + - '.github/workflows/readme-stats.yml' + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: write + +jobs: + refresh: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + + - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Install dependencies + run: cd python && uv sync --locked + + - name: Refresh README stats + run: cd python && uv run python -m lean_pool.stats --repo .. + + - name: Commit if changed + run: | + if git diff --quiet -- README.md; then + echo "README stats already up to date." + exit 0 + fi + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git add README.md + git commit -m "chore: refresh README stats [skip ci]" + git push diff --git a/README.md b/README.md index 03946bdbc2..efc0d0b7fd 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,12 @@ Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, and browse the API docs at . + +**90** formalization projects · **676,138** lines of Lean + + +(stats above are refreshed automatically by [`readme-stats.yml`](.github/workflows/readme-stats.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers) + So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged. ### Getting started diff --git a/python/lean_pool/stats.py b/python/lean_pool/stats.py new file mode 100644 index 0000000000..5e3f01ccef --- /dev/null +++ b/python/lean_pool/stats.py @@ -0,0 +1,176 @@ +"""Compute headline repository statistics and write them into the README. + +The main ``README.md`` carries a short, machine-maintained line reporting +how many projects live in the pool and how many lines of Lean they total. +This module derives both numbers from the single sources of truth +(``LeanPool/projects.yml`` for the project count, the ``LeanPool/`` tree +for the line count) and rewrites the block delimited by two HTML comment +markers: + + + ...generated line goes here... + + +Run ``python -m lean_pool.stats --repo .`` to rewrite the block, or pass +``--check`` to fail without writing when the block is stale (used by CI to +decide whether a refresh commit is needed). +""" + +from __future__ import annotations + +import argparse +import re +import sys +from dataclasses import dataclass +from pathlib import Path + +import yaml + +BEGIN_MARKER = "" +END_MARKER = "" + +_MARKER_BLOCK = re.compile( + re.escape(BEGIN_MARKER) + r".*?" + re.escape(END_MARKER), + re.DOTALL, +) + +# Directories whose ``.lean`` files are build artefacts or vendored +# dependencies rather than pooled project source. ``LeanPool/`` should +# never contain these, but excluding them keeps the count honest if a +# stray build tree ever lands under it. +_LOC_EXCLUDE_DIR_NAMES = frozenset({".lake", ".git", "lake-packages", "build"}) + + +@dataclass(frozen=True) +class Stats: + """Headline counts shown in the README.""" + + projects: int + lines_of_lean: int + + +def count_projects(projects_yml_path: Path) -> int: + """Return the number of projects registered in ``projects.yml``. + + Args: + projects_yml_path: Path to ``LeanPool/projects.yml``. + + Returns: + The length of the top-level ``projects`` list, or ``0`` if the + file is missing, malformed, or has no ``projects`` key. + """ + if not projects_yml_path.is_file(): + return 0 + data = yaml.safe_load(projects_yml_path.read_text()) or {} + if not isinstance(data, dict): + return 0 + projects = data.get("projects") or [] + if not isinstance(projects, list): + return 0 + return len(projects) + + +def count_lean_loc(pool_dir: Path) -> int: + """Sum lines across every ``.lean`` file under the pool tree. + + Walks ``pool_dir`` recursively and totals lines across all files + matching ``*.lean``, skipping build/dependency directories. Line + counting uses raw newline semantics so it matches ``wc -l``. + + Args: + pool_dir: Path to the ``LeanPool/`` directory. + + Returns: + The total line count, or ``0`` if the directory is missing. + """ + if not pool_dir.is_dir(): + return 0 + total = 0 + for path in pool_dir.rglob("*.lean"): + if any(part in _LOC_EXCLUDE_DIR_NAMES for part in path.parts): + continue + try: + with path.open("rb") as handle: + total += sum(1 for _ in handle) + except OSError: + continue + return total + + +def collect_stats(root: Path) -> Stats: + """Gather all README statistics for the checkout at ``root``.""" + return Stats( + projects=count_projects(root / "LeanPool" / "projects.yml"), + lines_of_lean=count_lean_loc(root / "LeanPool"), + ) + + +def render_stats(stats: Stats) -> str: + """Render the stats block body (without the surrounding markers).""" + return ( + f"**{stats.projects}** formalization projects · " + f"**{stats.lines_of_lean:,}** lines of Lean" + ) + + +def apply_stats(readme_text: str, stats: Stats) -> str: + """Return ``readme_text`` with the stats block replaced. + + Raises: + ValueError: If the BEGIN/END markers are not present. + """ + if not _MARKER_BLOCK.search(readme_text): + raise ValueError( + f"Could not find stats markers in README. " + f"Expected '{BEGIN_MARKER}' ... '{END_MARKER}'." + ) + replacement = f"{BEGIN_MARKER}\n{render_stats(stats)}\n{END_MARKER}" + return _MARKER_BLOCK.sub(replacement, readme_text, count=1) + + +def _parse_args(argv: list[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--repo", + type=Path, + default=Path(__file__).resolve().parents[2], + help="Repository root. Defaults to the checkout containing this package.", + ) + parser.add_argument( + "--check", + action="store_true", + help="Exit non-zero if the README stats block is stale; do not write.", + ) + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + """Run the stats CLI.""" + args = _parse_args(sys.argv[1:] if argv is None else argv) + root = args.repo.resolve() + readme_path = root / "README.md" + original = readme_path.read_text() + stats = collect_stats(root) + updated = apply_stats(original, stats) + + if args.check: + if updated != original: + print( + "README stats are out of date. Run " + "`uv run python -m lean_pool.stats --repo .` and commit.", + file=sys.stderr, + ) + return 1 + print("README stats are up to date.") + return 0 + + if updated != original: + readme_path.write_text(updated) + print(f"Updated README stats: {render_stats(stats)}") + else: + print("README stats already up to date.") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/tests/test_stats.py b/python/tests/test_stats.py new file mode 100644 index 0000000000..555c8bed68 --- /dev/null +++ b/python/tests/test_stats.py @@ -0,0 +1,104 @@ +"""Tests for README statistics generation.""" + +from __future__ import annotations + +from pathlib import Path + +import pytest + +from lean_pool.stats import ( + Stats, + apply_stats, + collect_stats, + count_lean_loc, + count_projects, + main, + render_stats, +) + +PROJECTS_YML = """projects: + - slug: alpha + title: Alpha + - slug: beta + title: Beta +""" + + +def _write_pool(root: Path) -> None: + """Create a minimal LeanPool tree with two projects and known LOC.""" + pool = root / "LeanPool" + pool.mkdir() + (pool / "projects.yml").write_text(PROJECTS_YML) + (pool / "Alpha.lean").write_text("line1\nline2\nline3\n") + nested = pool / "Beta" + nested.mkdir() + (nested / "Core.lean").write_text("only-one-line\n") + + +def test_count_projects(tmp_path: Path) -> None: + """The project count is the length of the projects list.""" + _write_pool(tmp_path) + assert count_projects(tmp_path / "LeanPool" / "projects.yml") == 2 + + +def test_count_projects_missing_file(tmp_path: Path) -> None: + """A missing registry yields zero rather than raising.""" + assert count_projects(tmp_path / "nope.yml") == 0 + + +def test_count_lean_loc(tmp_path: Path) -> None: + """Lines are summed recursively across every .lean file.""" + _write_pool(tmp_path) + assert count_lean_loc(tmp_path / "LeanPool") == 4 + + +def test_count_lean_loc_skips_build_dirs(tmp_path: Path) -> None: + """Build/dependency directories are excluded from the count.""" + _write_pool(tmp_path) + artefact = tmp_path / "LeanPool" / ".lake" / "Dep.lean" + artefact.parent.mkdir() + artefact.write_text("a\nb\nc\nd\ne\n") + assert count_lean_loc(tmp_path / "LeanPool") == 4 + + +def test_collect_stats(tmp_path: Path) -> None: + """Both headline numbers are gathered from the checkout.""" + _write_pool(tmp_path) + assert collect_stats(tmp_path) == Stats(projects=2, lines_of_lean=4) + + +def test_apply_stats_replaces_block() -> None: + """Only the marked block is rewritten; surrounding text is kept.""" + readme = "intro\n\nold\n\noutro\n" + updated = apply_stats(readme, Stats(projects=2, lines_of_lean=4)) + assert render_stats(Stats(projects=2, lines_of_lean=4)) in updated + assert "old" not in updated + assert updated.startswith("intro\n") + assert updated.endswith("outro\n") + + +def test_apply_stats_requires_markers() -> None: + """A README without the markers is a hard error.""" + with pytest.raises(ValueError, match="stats markers"): + apply_stats("no markers here", Stats(projects=1, lines_of_lean=1)) + + +def test_main_writes_and_is_idempotent(tmp_path: Path) -> None: + """Writing fills the block, and re-running changes nothing.""" + _write_pool(tmp_path) + readme = tmp_path / "README.md" + readme.write_text("\n\n\n") + + assert main(["--repo", str(tmp_path)]) == 0 + assert "**2** formalization projects" in readme.read_text() + # A second write is a no-op, and --check now passes. + assert main(["--repo", str(tmp_path)]) == 0 + assert main(["--repo", str(tmp_path), "--check"]) == 0 + + +def test_main_check_fails_when_stale(tmp_path: Path) -> None: + """`--check` exits non-zero when the block is out of date.""" + _write_pool(tmp_path) + readme = tmp_path / "README.md" + readme.write_text("\nstale\n\n") + assert main(["--repo", str(tmp_path), "--check"]) == 1