From b593edb0a2b2822606936fdccb0e5e89ed01b26f Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Wed, 14 Oct 2026 17:35:37 -0400 Subject: [PATCH] Preserve Lake declarations and traces when vendoring Vendoring must change dependency locations while retaining the declarations which consume them. Stop each TOML require block at the next table so that library and executable declarations survive. Add fixtures from the pinned aesop and importGraph packages to cover those boundaries. Reject symlinks outside the private archive roots before rewriting any file. Keep path components separate in trace matching so a long absolute path cannot trigger exponential regular-expression backtracking. These changes let native Lake traces remain usable after archive relocation. gherrit-pr-id: Gxizdpw52bljtxjfng3ervgk5xnca6mow Agent-authored-by: AI agent acting on joshlf's behalf --- anneal/rewrite-lake-vendor.py | 27 +++++- anneal/tests/fixtures/lake-vendor/README.md | 10 +++ anneal/tests/fixtures/lake-vendor/aesop.toml | 18 ++++ .../fixtures/lake-vendor/importGraph.toml | 33 +++++++ anneal/tests/test_rewrite_lake_vendor.py | 89 +++++++++++++++++++ 5 files changed, 175 insertions(+), 2 deletions(-) create mode 100644 anneal/tests/fixtures/lake-vendor/README.md create mode 100644 anneal/tests/fixtures/lake-vendor/aesop.toml create mode 100644 anneal/tests/fixtures/lake-vendor/importGraph.toml diff --git a/anneal/rewrite-lake-vendor.py b/anneal/rewrite-lake-vendor.py index e61fc99283..90788e342a 100755 --- a/anneal/rewrite-lake-vendor.py +++ b/anneal/rewrite-lake-vendor.py @@ -13,6 +13,26 @@ REMOTE_TOML_KEYS = {"git", "url", "rev", "scope", "subDir", "inputRev"} +def validate_vendoring_roots(root: Path, packages_dir: Path) -> None: + """Reject links that could route a private rewrite into another installation.""" + roots = [root.absolute(), packages_dir.absolute()] + for directory in roots: + if directory.is_symlink() or not directory.is_dir(): + raise ValueError(f"Vendoring root must be a physical directory: {directory}") + allowed = [directory.resolve() for directory in roots] + def fail_walk(error: OSError) -> None: + raise error + + for directory in roots: + for current, directories, files in os.walk(directory, followlinks=False, onerror=fail_walk): + for name in directories + files: + path = Path(current) / name + if path.is_symlink(): + target = path.resolve(strict=True) + if not any(target.is_relative_to(parent) for parent in allowed): + raise ValueError(f"Vendoring symlink leaves private roots: {path} -> {target}") + + def quote_name(name: str) -> str: if re.fullmatch(r"[A-Za-z_][A-Za-z0-9_']*", name): return name @@ -34,7 +54,9 @@ def package_dirs(packages_dir: Path) -> dict[str, Path]: def replace_require_toml_blocks(path: Path, packages: dict[str, Path]) -> bool: content = path.read_text() - block_re = re.compile(r"(?ms)^\s*\[\[require\]\]\s*\n(?:(?!^\s*\[\[).*\n?)*") + # Stop at every TOML table, including single-bracket option tables. A + # greedy dot with DOTALL would also consume later library/executable tables. + block_re = re.compile(r"(?ms)^[ \t]*\[\[require\]\][ \t]*\n.*?(?=^[ \t]*\[|\Z)") changed = False @@ -151,7 +173,7 @@ def rewrite_trace_prefixes( prefixes = trace_prefixes(root, packages_dir, packages, extra_prefixes) package_root_patterns = [ re.compile( - rf"(? None: ) args = parser.parse_args() + validate_vendoring_roots(args.root, args.packages_dir) root = args.root.resolve() packages_dir = args.packages_dir.resolve() packages = package_dirs(packages_dir) diff --git a/anneal/tests/fixtures/lake-vendor/README.md b/anneal/tests/fixtures/lake-vendor/README.md new file mode 100644 index 0000000000..2e02478a36 --- /dev/null +++ b/anneal/tests/fixtures/lake-vendor/README.md @@ -0,0 +1,10 @@ +These unmodified Lake configurations are regression inputs for vendoring, not +dependency pins. They come from the dependency revisions in Anneal's pinned +Aeneas archive: + +- `aesop.toml`: aesop `e3cb2f741431ce31bf73549fb52316a57368b06f`. +- `importGraph.toml`: import-graph `5c7542ed018c78194f1e2b903eaf6a792b74c03d`. + +Both projects distribute these files under Apache-2.0; see the repository's +`LICENSE-APACHE`. The regression checks that replacing a remote dependency does +not remove the library and executable declarations that follow it. diff --git a/anneal/tests/fixtures/lake-vendor/aesop.toml b/anneal/tests/fixtures/lake-vendor/aesop.toml new file mode 100644 index 0000000000..d14950574e --- /dev/null +++ b/anneal/tests/fixtures/lake-vendor/aesop.toml @@ -0,0 +1,18 @@ +name = "aesop" +defaultTargets = ["Aesop"] +testDriver = "AesopTest" +precompileModules = false # We would like to turn this on, but it breaks the Mathlib cache. +platformIndependent = true + +[[require]] +name = "batteries" +scope = "leanprover-community" +rev = "v4.31.0" + +[[lean_lib]] +name = "Aesop" + +[[lean_lib]] +name = "AesopTest" +globs = ["AesopTest.+"] +leanOptions = {linter.unusedVariables = false} diff --git a/anneal/tests/fixtures/lake-vendor/importGraph.toml b/anneal/tests/fixtures/lake-vendor/importGraph.toml new file mode 100644 index 0000000000..84f39a9169 --- /dev/null +++ b/anneal/tests/fixtures/lake-vendor/importGraph.toml @@ -0,0 +1,33 @@ +name = "importGraph" +description = "Tools to analyse and visualise the import structure of Lean packages and their files." +license = "Apache-2.0" +licenseFiles = ["LICENSE"] + +defaultTargets = ["ImportGraph", "graph"] +testRunner = "ImportGraphTest" + +[[require]] +name = "Cli" +scope = "leanprover" +rev = "v4.31.0" + +[[lean_lib]] +name = "ImportGraph" + +# `lake exe graph` constructs import graphs in `.dot` or graphical formats. +[[lean_exe]] +name = "graph" +root = "MainGraph" +# Enables the use of the Lean interpreter by the executable (e.g., `runFrontend`) +# at the expense of increased binary size on Linux. +# Remove this line if you do not need such functionality. +supportInterpreter = true + +# `lake exe unused_transitive_imports` prints unused transitive imports from amongst a given list of modules. +[[lean_exe]] +name = "unused_transitive_imports" +root = "MainUnusedTransitiveImports" +supportInterpreter = true + +[[lean_lib]] +name = "ImportGraphTest" diff --git a/anneal/tests/test_rewrite_lake_vendor.py b/anneal/tests/test_rewrite_lake_vendor.py index 380b6e763d..078ce3b7e8 100644 --- a/anneal/tests/test_rewrite_lake_vendor.py +++ b/anneal/tests/test_rewrite_lake_vendor.py @@ -14,6 +14,8 @@ import importlib.util import tempfile +import subprocess +import sys import unittest from pathlib import Path @@ -31,6 +33,93 @@ def write(path: Path, contents: str = "") -> None: class RewriteLakeVendorTests(unittest.TestCase): + def test_toml_require_rewrite_preserves_following_tables(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + lakefile = root / "lakefile.toml" + following = ('[[lean_lib]]\nname = "Library"\n\n' + '[[lean_exe]]\nname = "driver"\nroot = "Main"\n' + '[leanOptions]\nautoImplicit = false\n') + write(lakefile, 'name = "consumer"\n\n[[require]]\nname = "dep"\n' + 'scope = "owner"\nrev = "main"\n\n' + following) + self.assertTrue(rewrite_lake_vendor.replace_require_toml_blocks( + lakefile, {"dep": root / "packages/dep"})) + rewritten = lakefile.read_text() + self.assertTrue(rewritten.endswith(following)) + self.assertIn('path = "packages/dep"', rewritten) + self.assertNotIn('rev =', rewritten) + self.assertFalse(rewrite_lake_vendor.replace_require_toml_blocks( + lakefile, {"dep": root / "packages/dep"})) + + def test_toml_require_stops_before_single_bracket_table(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / 'lakefile.toml' + following = '[leanOptions]\nautoImplicit = false\n' + write(path, '[[require]]\nname = "dep"\nrev = "main"\n' + following) + rewrite_lake_vendor.replace_require_toml_blocks(path, {"dep": Path(tmp) / 'dep'}) + self.assertTrue(path.read_text().endswith(following)) + + def test_pinned_aesop_and_importgraph_keep_all_declared_targets(self) -> None: + fixtures = SCRIPT.parent / "tests/fixtures/lake-vendor" + for name, dependency in [("aesop", "batteries"), ("importGraph", "Cli")]: + with self.subTest(package=name), tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "lakefile.toml" + original = (fixtures / (name + ".toml")).read_text() + write(path, original) + following = original[original.index('[[lean_lib]]'):] + self.assertTrue(rewrite_lake_vendor.replace_require_toml_blocks( + path, {dependency: Path(tmp) / dependency})) + self.assertTrue(path.read_text().endswith(following)) + self.assertIn('path = "' + dependency + '"', path.read_text()) + + def test_external_symlink_rejected_before_any_rewrite(self) -> None: + for entry in [".lake", "lakefile.lean"]: + with self.subTest(entry=entry), tempfile.TemporaryDirectory() as tmp: + base = Path(tmp) + root, packages, shared = base / "private", base / "packages", base / "shared" + root.mkdir() + packages.mkdir() + shared.mkdir() + original = 'require dep from git "https://example.invalid/dep" @ "rev"\n' + write(root / "lakefile.lean", original) + write(shared / "lakefile.lean", original) + if entry == ".lake": + (root / entry).symlink_to(shared, target_is_directory=True) + else: + (root / entry).unlink() + (root / entry).symlink_to(shared / entry) + (packages / "dep").mkdir() + result = subprocess.run([sys.executable, str(SCRIPT), "--root", str(root), + "--packages-dir", str(packages)], + capture_output=True, text=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("symlink leaves private roots", result.stderr) + self.assertEqual((shared / "lakefile.lean").read_text(), original) + self.assertEqual((root / "lakefile.lean").read_text(), original) + + def test_internal_payload_links_are_allowed(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root, packages = Path(tmp) / "private", Path(tmp) / "packages" + root.mkdir() + packages.mkdir() + write(root / "real.lean", "def value := 1\n") + (root / "linked.lean").symlink_to("real.lean") + rewrite_lake_vendor.validate_vendoring_roots(root, packages) + + def test_long_unmatched_trace_path_does_not_backtrack_exponentially(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root, packages = Path(tmp) / 'root', Path(tmp) / 'packages' + root.mkdir() + (packages / 'mathlib').mkdir(parents=True) + unrelated = '/' + '/'.join(['longsegment'] * 80) + '/Unrelated.lean' + trace = root / 'Module.trace' + write(trace, unrelated + '\n/upstream/packages/mathlib/Mathlib.lean\n') + result = subprocess.run([sys.executable, str(SCRIPT), '--root', str(root), + '--packages-dir', str(packages), '--rewrite-traces'], + capture_output=True, text=True, timeout=5) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(trace.read_text(), unrelated + '\nMathlib.lean\n') + def test_rewrites_upstream_aeneas_backend_trace_prefix(self) -> None: with tempfile.TemporaryDirectory() as tmp: root = Path(tmp) / "aeneas" / "backends" / "lean"