fix: preserve module exports when rebasing import PRs

README.md

@@ -58,6 +58,11 @@ See [Challenge mode](CONTRIBUTING.md#challenge-mode) in `CONTRIBUTING.md`.
 
 See [`CONTRIBUTING.md`](CONTRIBUTING.md).
 
+Import PRs can be refreshed automatically after other projects merge. The
+[rebase helper](python/lean_pool/rebase.py) resolves conflicts in the project registry
+and generated index, preserving module headers and public imports when the index uses them.
+Conflicts in proof files require a manual rebase.
+
 ### Credits
 
 Created as part of the [UW Lean Hackathon](https://uw2026leanhackathon.github.io/) by [Vasily Ilin](https://github.com/Vilin97) and [Justin Asher](https://github.com/justincasher).

python/lean_pool/rebase.py

@@ -25,9 +25,12 @@
 
 import argparse
 import logging
+import re
 import sys
 from pathlib import Path
 
+from lean_pool.exposition.source_text import code_view
+
 logger = logging.getLogger(__name__)
 
 REGISTRY = "LeanPool/projects.yml"
@@ -37,6 +40,26 @@
 RESOLVABLE = frozenset({INDEX, REGISTRY})
 
 
+def _uses_module_system(source: str) -> bool:
+    """Detect a module header in either current version of a conflicted index."""
+    conflict = re.compile(
+        r"^<<<<<<<[^\n]*\n(?P<ours>.*?)"
+        r"(?:^\|{7}[^\n]*\n.*?)?^=======\n"
+        r"(?P<theirs>.*?)^>>>>>>>[^\n]*(?:\n|$)",
+        re.MULTILINE | re.DOTALL,
+    )
+    # Keep shared text in both versions so comments spanning a conflict remain
+    # comments, while a malformed comment on one side cannot mask the other.
+    return any(
+        re.search(
+            r"^\s*module(?:\s|$)",
+            code_view(conflict.sub(lambda match: match[side], source)),
+            re.MULTILINE,
+        )
+        for side in ("ours", "theirs")
+    )
+
+
 def render_index(root: Path) -> str:
     """Regenerate the ``mk_all`` index from the Lean files on disk."""
     pool = root / "LeanPool"
@@ -45,7 +68,14 @@ def render_index(root: Path) -> str:
         + str(path.relative_to(pool)).removesuffix(".lean").replace("/", ".")
         for path in pool.rglob("*.lean")
     )
-    return "".join(f"import {module}\n" for module in modules)
+    index = root / INDEX
+    existing = index.read_text(encoding="utf-8") if index.exists() else ""
+    uses_modules = _uses_module_system(existing)
+    header = "module  -- shake: keep-all --deprecated_module: ignore\n\n"
+    prefix = "public " if uses_modules else ""
+    return (header if uses_modules else "") + "".join(
+        f"{prefix}import {module}\n" for module in modules
+    )
 
 
 def split_cards(text: str) -> tuple[str, list[tuple[str, str]]]:

python/tests/test_rebase.py

@@ -4,6 +4,8 @@
 
 from pathlib import Path
 
+import pytest
+
 from lean_pool.rebase import (
     main,
     merge_registry,
@@ -78,6 +80,71 @@ def test_render_index_reproduces_the_committed_index() -> None:
     assert render_index(root) == (root / "LeanPool.lean").read_text(encoding="utf-8")
 
 
+def test_render_index_preserves_module_exports_during_conflicts(tmp_path: Path) -> None:
+    """A conflicting import PR cannot revert the library to plain imports."""
+    pool = tmp_path / "LeanPool"
+    pool.mkdir()
+    (pool / "Alpha.lean").touch()
+    (pool / "Beta.lean").touch()
+    (tmp_path / "LeanPool.lean").write_text(
+        "<<<<<<< HEAD\nmodule  -- shake: keep-all --deprecated_module: ignore\n\n"
+        "public import LeanPool.Alpha\n=======\n"
+        "import LeanPool.Beta\n>>>>>>> incoming\n"
+    )
+    expected = (
+        "module  -- shake: keep-all --deprecated_module: ignore\n\n"
+        "public import LeanPool.Alpha\npublic import LeanPool.Beta\n"
+    )
+    assert render_index(tmp_path) == expected
+    (tmp_path / "LeanPool.lean").write_text(expected)
+    assert render_index(tmp_path) == expected
+
+
+def test_render_index_ignores_module_inside_comments(tmp_path: Path) -> None:
+    """Documentation cannot accidentally opt an index into the module system."""
+    (tmp_path / "LeanPool").mkdir()
+    (tmp_path / "LeanPool" / "Alpha.lean").touch()
+    (tmp_path / "LeanPool.lean").write_text(
+        "/-\nmodule\n/- nested -/\n-/\nimport LeanPool.Alpha\n"
+    )
+    assert render_index(tmp_path) == "import LeanPool.Alpha\n"
+
+
+@pytest.mark.parametrize("unfinished", ["/- unclosed comment", '"unclosed string'])
+def test_render_index_scans_conflict_sides_independently(
+    tmp_path: Path, unfinished: str
+) -> None:
+    """Lexical state on one conflict side cannot hide the other side's header."""
+    (tmp_path / "LeanPool").mkdir()
+    (tmp_path / "LeanPool" / "Alpha.lean").touch()
+    (tmp_path / "LeanPool.lean").write_text(
+        f"<<<<<<< HEAD\n{unfinished}\n=======\nmodule\n>>>>>>> incoming\n"
+    )
+    assert render_index(tmp_path) == (
+        "module  -- shake: keep-all --deprecated_module: ignore\n\n"
+        "public import LeanPool.Alpha\n"
+    )
+
+
+@pytest.mark.parametrize(
+    "source",
+    [
+        "/- shared comment\n<<<<<<< HEAD\nmodule\n=======\nmodule\n"
+        ">>>>>>> incoming\n-/\nimport LeanPool.Alpha\n",
+        "<<<<<<< HEAD\nimport LeanPool.Alpha\n||||||| base\nmodule\n"
+        "=======\nimport LeanPool.Alpha\n>>>>>>> incoming\n",
+    ],
+)
+def test_render_index_ignores_noncode_and_base_conflict_headers(
+    tmp_path: Path, source: str
+) -> None:
+    """Only a code header in a current side can opt into the module system."""
+    (tmp_path / "LeanPool").mkdir()
+    (tmp_path / "LeanPool" / "Alpha.lean").touch()
+    (tmp_path / "LeanPool.lean").write_text(source)
+    assert render_index(tmp_path) == "import LeanPool.Alpha\n"
+
+
 # --------------------------------------------------------------------------- #
 # Registry merging
 # --------------------------------------------------------------------------- #