Generate FILE_TREE.md from the source tree and check it in CI

.github/workflows/ci.yml

@@ -16,3 +16,10 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           check-reservoir-eligibility: true
+
+  file-tree:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Check FILE_TREE.md is up to date
+        run: python3 scripts/file_tree.py --check

CONTRIBUTING.md

@@ -24,6 +24,13 @@ Run the whole-library verification from the repository root:
 LEAN_NUM_THREADS=$(nproc) lake build
 ```
 
+If the change adds, moves, or deletes a module, regenerate the module index; CI fails when
+[`FILE_TREE.md`](./FILE_TREE.md) is out of date:
+
+```bash
+python3 scripts/file_tree.py
+```
+
 Describe the mathematical result, its source, the owning module, and any API decisions in the pull
 request. New modules should include a Mathlib-style file header and module docstring.
 

FILE_TREE.md

@@ -1,21 +1,24 @@
 # StatsMLlib file tree
 
-This document presents the public Lean source tree after the Mathlib-style subject refactor.
-`StatsMLlib/` contains 144 Lean modules under eight layer-one directories and no root-level Lean
-files. A filesystem path such as `StatsMLlib/Probability/Process/Dudley.lean` corresponds to the Lean
-module `StatsMLlib.Probability.Process.Dudley`.
+<!-- Generated by scripts/file_tree.py; do not edit by hand. -->
+
+This document presents the public Lean source tree after the Mathlib-style subject
+refactor.
+`StatsMLlib/` contains 146 Lean modules under eight layer-one directories and
+no root-level Lean files. A filesystem path such as `StatsMLlib/Probability/Process/Dudley.lean`
+corresponds to the Lean module `StatsMLlib.Probability.Process.Dudley`.
 
 | Layer | Modules |
 | --- | ---: |
 | `Analysis` | 9 |
 | `LearningTheory` | 33 |
-| `LinearAlgebra` | 6 |
+| `LinearAlgebra` | 7 |
 | `MeasureTheory` | 4 |
 | `Order` | 1 |
-| `Probability` | 68 |
+| `Probability` | 69 |
 | `Statistics` | 21 |
 | `Topology` | 2 |
-| **Total** | **144** |
+| **Total** | **146** |
 
 ```text
 StatsMLlib/
@@ -33,14 +36,14 @@ StatsMLlib/
 │   ├── LogSumExp.lean
 │   └── SoftMinMax.lean
 ├── LearningTheory/
+│   ├── EmpiricalProcess/
+│   │   ├── FunctionClass.lean
+│   │   └── Metric.lean
 │   ├── EmpiricalRiskMinimization/
 │   │   ├── Basic.lean
 │   │   ├── Defs.lean
 │   │   ├── Generalization.lean
 │   │   └── KernelPredictor.lean
-│   ├── EmpiricalProcess/
-│   │   ├── FunctionClass.lean
-│   │   └── Metric.lean
 │   ├── FunctionClass/
 │   │   ├── LinearPredictor/
 │   │   │   ├── L1.lean
@@ -78,6 +81,7 @@ StatsMLlib/
 │   └── Matrix/
 │       ├── CourantFischer.lean
 │       ├── EckartYoungMirsky.lean
+│       ├── InterlacingPR.lean
 │       ├── Lieb.lean
 │       ├── OperatorNorm.lean
 │       ├── Perturbation.lean
@@ -153,7 +157,8 @@ StatsMLlib/
 │   │   ├── Markov.lean
 │   │   └── Separation.lean
 │   ├── Independence/
-│   │   └── FinsetPi.lean
+│   │   ├── FinsetPi.lean
+│   │   └── Grouping.lean
 │   ├── Moments/
 │   │   ├── Cumulant.lean
 │   │   ├── Expectation.lean
@@ -207,6 +212,6 @@ StatsMLlib/
         └── Supremum.lean
 ```
 
-Only the public `StatsMLlib/` source tree is shown. Historical provenance is recorded in file headers
-and the README; build artifacts and dependency caches are omitted. See
+Only the public `StatsMLlib/` source tree is shown. Historical provenance is recorded in
+file headers and the README; build artifacts and dependency caches are omitted. See
 [`ARCHITECTURE.md`](./ARCHITECTURE.md) for ownership and import-direction rules.

scripts/file_tree.py

@@ -0,0 +1,100 @@
+#!/usr/bin/env python3
+"""Generate FILE_TREE.md from the StatsMLlib/ source tree.
+
+Usage:
+    python3 scripts/file_tree.py          # rewrite FILE_TREE.md
+    python3 scripts/file_tree.py --check  # exit 1 if FILE_TREE.md is out of date
+
+Every part of FILE_TREE.md that depends on the filesystem (module counts and the tree) is
+derived here, so the file must not be edited by hand.
+"""
+
+import difflib
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+SRC = ROOT / "StatsMLlib"
+OUT = ROOT / "FILE_TREE.md"
+
+NUMBER_WORDS = ["zero", "one", "two", "three", "four", "five", "six", "seven", "eight",
+                "nine", "ten", "eleven", "twelve"]
+
+
+def count_modules(path: Path) -> int:
+    return sum(1 for _ in path.rglob("*.lean"))
+
+
+def tree_lines(path: Path, prefix: str = "") -> list[str]:
+    """Directories first, then Lean files, each in sorted order."""
+    dirs = sorted(p for p in path.iterdir() if p.is_dir() and count_modules(p) > 0)
+    files = sorted(p for p in path.iterdir() if p.is_file() and p.suffix == ".lean")
+    entries = dirs + files
+    lines = []
+    for i, entry in enumerate(entries):
+        last = i == len(entries) - 1
+        lines.append(f"{prefix}{'└── ' if last else '├── '}{entry.name}"
+                     f"{'/' if entry.is_dir() else ''}")
+        if entry.is_dir():
+            lines.extend(tree_lines(entry, prefix + ("    " if last else "│   ")))
+    return lines
+
+
+def render() -> str:
+    layers = sorted(p for p in SRC.iterdir() if p.is_dir() and count_modules(p) > 0)
+    root_files = sorted(p for p in SRC.iterdir() if p.is_file() and p.suffix == ".lean")
+    total = count_modules(SRC)
+    n_layers = len(layers)
+    layer_word = NUMBER_WORDS[n_layers] if n_layers < len(NUMBER_WORDS) else str(n_layers)
+    root_clause = ("no root-level Lean files" if not root_files
+                   else f"{len(root_files)} root-level Lean files")
+
+    out = [
+        "# StatsMLlib file tree",
+        "",
+        "<!-- Generated by scripts/file_tree.py; do not edit by hand. -->",
+        "",
+        "This document presents the public Lean source tree after the Mathlib-style subject",
+        "refactor.",
+        f"`StatsMLlib/` contains {total} Lean modules under {layer_word} layer-one directories and",
+        f"{root_clause}. A filesystem path such as `StatsMLlib/Probability/Process/Dudley.lean`",
+        "corresponds to the Lean module `StatsMLlib.Probability.Process.Dudley`.",
+        "",
+        "| Layer | Modules |",
+        "| --- | ---: |",
+    ]
+    out += [f"| `{p.name}` | {count_modules(p)} |" for p in layers]
+    out += [
+        f"| **Total** | **{total}** |",
+        "",
+        "```text",
+        "StatsMLlib/",
+        *tree_lines(SRC),
+        "```",
+        "",
+        "Only the public `StatsMLlib/` source tree is shown. Historical provenance is recorded in",
+        "file headers and the README; build artifacts and dependency caches are omitted. See",
+        "[`ARCHITECTURE.md`](./ARCHITECTURE.md) for ownership and import-direction rules.",
+        "",
+    ]
+    return "\n".join(out)
+
+
+def main() -> int:
+    generated = render()
+    if "--check" in sys.argv[1:]:
+        current = OUT.read_text(encoding="utf-8") if OUT.exists() else ""
+        if current == generated:
+            return 0
+        sys.stdout.writelines(difflib.unified_diff(
+            current.splitlines(keepends=True), generated.splitlines(keepends=True),
+            "FILE_TREE.md", "FILE_TREE.md (generated)"))
+        print("\nFILE_TREE.md is out of date; run `python3 scripts/file_tree.py`.",
+              file=sys.stderr)
+        return 1
+    OUT.write_text(generated, encoding="utf-8")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())