From a478d921a3c368ef9f8422152e214e379f2d8a45 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 11 Sep 2026 00:34:55 -0700 Subject: [PATCH 1/3] fix: preserve module exports when rebasing import PRs --- python/lean_pool/rebase.py | 14 +++++++++++++- python/tests/test_rebase.py | 30 ++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+), 1 deletion(-) diff --git a/python/lean_pool/rebase.py b/python/lean_pool/rebase.py index 47b6baa14c..2abe3a90c4 100644 --- a/python/lean_pool/rebase.py +++ b/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" @@ -45,7 +48,16 @@ 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 = code_view(index.read_text()) if index.exists() else "" + # During a rebase the index may still contain conflict markers. Preserve + # module style if either side has adopted it, matching mk_all's output. + uses_modules = re.search(r"^\s*module(?:\s|$)", existing, re.MULTILINE) + 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]]]: diff --git a/python/tests/test_rebase.py b/python/tests/test_rebase.py index 4b719d14d0..5e34a45cc5 100644 --- a/python/tests/test_rebase.py +++ b/python/tests/test_rebase.py @@ -78,6 +78,36 @@ 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" + + # --------------------------------------------------------------------------- # # Registry merging # --------------------------------------------------------------------------- # From 7e36c12fcfdfc86edc2d01887bdb8085cffd4e7a Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Tue, 15 Sep 2026 10:22:31 -0700 Subject: [PATCH 2/3] Preserve module exports across independent conflict sides --- python/lean_pool/rebase.py | 26 ++++++++++++++++++++++---- python/tests/test_rebase.py | 37 +++++++++++++++++++++++++++++++++++++ 2 files changed, 59 insertions(+), 4 deletions(-) diff --git a/python/lean_pool/rebase.py b/python/lean_pool/rebase.py index 2abe3a90c4..602bbadd18 100644 --- a/python/lean_pool/rebase.py +++ b/python/lean_pool/rebase.py @@ -40,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.*?)" + r"(?:^\|{7}[^\n]*\n.*?)?^=======\n" + r"(?P.*?)^>>>>>>>[^\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" @@ -49,10 +69,8 @@ def render_index(root: Path) -> str: for path in pool.rglob("*.lean") ) index = root / INDEX - existing = code_view(index.read_text()) if index.exists() else "" - # During a rebase the index may still contain conflict markers. Preserve - # module style if either side has adopted it, matching mk_all's output. - uses_modules = re.search(r"^\s*module(?:\s|$)", existing, re.MULTILINE) + 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( diff --git a/python/tests/test_rebase.py b/python/tests/test_rebase.py index 5e34a45cc5..cebda23e24 100644 --- a/python/tests/test_rebase.py +++ b/python/tests/test_rebase.py @@ -4,6 +4,8 @@ from pathlib import Path +import pytest + from lean_pool.rebase import ( main, merge_registry, @@ -108,6 +110,41 @@ def test_render_index_ignores_module_inside_comments(tmp_path: Path) -> None: 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 # --------------------------------------------------------------------------- # From 826e8d6f1cbd1f5aba7feaa3eaa300a00a6f5231 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 21 Sep 2026 05:33:39 +0000 Subject: [PATCH 3/3] Document import rebase behavior and module exports --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index a099a7f109..1cb68f353b 100644 --- a/README.md +++ b/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).