From 9cb5ef72ad9a20b8358d89529c3c3084a9a57ceb Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 1 Oct 2026 16:14:43 +0000 Subject: [PATCH] Require complete project-root indexes in module-system packages --- python/lean_pool/indexes.py | 4 ++-- python/tests/test_rebase_fastpath.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/python/lean_pool/indexes.py b/python/lean_pool/indexes.py index 6b5c9dfb14..66c7459182 100644 --- a/python/lean_pool/indexes.py +++ b/python/lean_pool/indexes.py @@ -18,8 +18,8 @@ "Released under Apache 2.0 license as described in the file LICENSE.\n" "Authors: Lean Pool contributors\n-/\n" + MODULE_HEADER + GENERATED_MARKER ) -# Removed after the separate content migration has landed. -REQUIRE_PROJECT_ROOTS = False +# Production module-system packages must never revert to a flat index. +REQUIRE_PROJECT_ROOTS = True def project_modules(root: Path) -> dict[str, list[str]]: diff --git a/python/tests/test_rebase_fastpath.py b/python/tests/test_rebase_fastpath.py index b3a87cd3db..2aa9cfb04f 100644 --- a/python/tests/test_rebase_fastpath.py +++ b/python/tests/test_rebase_fastpath.py @@ -48,7 +48,7 @@ def rebased(tmp_path: Path) -> tuple[Path, str, str, str, str]: (root / "LeanPool/A.lean").write_text("module\n") (root / "LeanPool/projects.yml").write_text("projects:\n - slug: a\n") for name in rebase_fastpath.PINNED_INPUTS: - (root / name).write_text(name) + (root / name).write_text('name = "test"\n' if name == "lakefile.toml" else name) _index(root) old_base = _commit(root, "base")