Add auto-updating README stats (project count + Lean LOC)

.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

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 <https://vilin97.github.io/lean-pool/>.
 
+<!-- BEGIN STATS -->
+**90** formalization projects · **676,138** lines of Lean
+<!-- END STATS -->
+
+<sub>(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)</sub>
+
 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

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:
+
+    <!-- BEGIN STATS -->
+    ...generated line goes here...
+    <!-- END STATS -->
+
+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 = "<!-- BEGIN STATS -->"
+END_MARKER = "<!-- END STATS -->"
+
+_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())

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<!-- BEGIN STATS -->\nold\n<!-- END STATS -->\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("<!-- BEGIN STATS -->\n\n<!-- END STATS -->\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("<!-- BEGIN STATS -->\nstale\n<!-- END STATS -->\n")
+    assert main(["--repo", str(tmp_path), "--check"]) == 1