Enforce project entry imports in LeanPool root

.github/CODE_QUALITY.md

@@ -42,6 +42,7 @@ Current checks:
 - project summaries and branches are nonempty strings, MSC codes are a nonempty string list, and `main_results` is a nonempty list of `declaration` / `informal` entries
 - project `main_results[*].declaration` values include every `main_declarations` entry, so compact project cards and richer documentation metadata cannot drift
 - project `slug` and `entry_module` values are unique
+- every registered project `entry_module` is imported directly by `LeanPool.lean`
 - every top-level project module `LeanPool/Foo.lean`, except `LeanPool/Basic.lean`, is registered as an `entry_module`
 - project entry modules and listed main declarations resolve in Lean
 - generated entry-point project cards match `LeanPool/projects.yml`

python/lean_pool/quality.py

@@ -1122,6 +1122,9 @@ def _check_projects(root: Path) -> list[_QualityError]:
         return errors
 
     errors.extend(_check_project_uniqueness(path, projects))
+    if errors:
+        return errors
+    errors.extend(_check_project_entry_imports(root, projects))
     if errors:
         return errors
     errors.extend(_check_top_level_project_modules(root, path, projects))
@@ -1165,6 +1168,30 @@ def _check_project_uniqueness(path: Path, projects: list[Any]) -> list[_QualityE
     return errors
 
 
+def _check_project_entry_imports(
+    root: Path, projects: list[Any]
+) -> list[_QualityError]:
+    """Require LeanPool.lean to import every registered project entry module."""
+    index_path = root / "LeanPool.lean"
+    if not index_path.exists():
+        return []
+    imports = set(_parse_imports(index_path.read_text()))
+    entry_modules = {
+        project["entry_module"]
+        for project in projects
+        if isinstance(project, dict) and isinstance(project.get("entry_module"), str)
+    }
+    return [
+        _QualityError(
+            index_path,
+            1,
+            f"project entry module {module} is not imported by LeanPool.lean; "
+            "run `lake exe mk_all`",
+        )
+        for module in sorted(entry_modules - imports)
+    ]
+
+
 def _check_top_level_project_modules(
     root: Path, path: Path, projects: list[Any]
 ) -> list[_QualityError]:

python/tests/test_quality.py

@@ -267,6 +267,31 @@ def test_quality_check_rejects_unreachable_lean_file(tmp_path: Path) -> None:
     assert any("not reachable" in error.message for error in errors)
 
 
+def test_quality_check_requires_direct_project_entry_import(tmp_path: Path) -> None:
+    """Transitive reachability does not replace a root import for each project."""
+    _write_minimal_repo(tmp_path, "def baseHello := 1\n")
+    wrapper = tmp_path / "LeanPool" / "Wrapper"
+    wrapper.mkdir()
+    (tmp_path / "LeanPool.lean").write_text(
+        "import LeanPool.Basic\nimport LeanPool.Wrapper.Internal\n"
+    )
+    (wrapper / "Internal.lean").write_text(f"{HEADER}\nimport LeanPool.MyProj\n")
+    card = _project_card(_PROJECT_FIXTURE)
+    (tmp_path / "LeanPool" / "MyProj.lean").write_text(
+        f"{HEADER}\n\n{card}\n\ndef hello := 1\n"
+    )
+    _write_project_yaml(tmp_path, [{"slug": "p", "entry_module": "LeanPool.MyProj"}])
+
+    errors = run_checks(tmp_path, skip_lean_axioms=True)
+
+    assert not any("not reachable" in error.message for error in errors)
+    assert any(
+        "project entry module LeanPool.MyProj is not imported by LeanPool.lean"
+        in error.message
+        for error in errors
+    )
+
+
 def test_quality_check_rejects_missing_project_metadata(tmp_path: Path) -> None:
     """Project metadata is required even before there are projects."""
     _write_minimal_repo(tmp_path)