From 5fa8d10d75d2fa5e18621ef14cf9df6bbbf8b041 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 19:08:58 -0400 Subject: [PATCH 1/2] feat(dev): add source-only worktree creation Add --source-only to skip initial cache, package-source and package-control copies while retaining isolation checks and cache bootstrap. Reject copy-flag combinations and guard package-local cache directory symlinks before either mode bootstraps. Real temporary-repository regressions cover both creation modes, copied outputs and dependency controls, bootstrap selection and opt-out, takeover tracking, and existing or checked-out cache symlinks reaching the primary fixture. Document download and disk costs. AI assistance: Codex implemented and self-reviewed this bounded filesystem workflow for #1675. Focused 35-test and full 400-test script suites pass (1 and 8 unsupported-feature skips respectively); required Lean gates follow on this revision. --- CONTRIBUTING.md | 4 +- scripts/cache/README.md | 22 +++++- scripts/test_worktree.py | 152 ++++++++++++++++++++++++++++++++++++++- scripts/worktree.sh | 46 ++++++++---- 4 files changed, 207 insertions(+), 17 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9448410f9..400207a8b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -149,7 +149,9 @@ defaults to the number of logical processors and is not a hard process or memory observed concurrency and memory use. Keep mutable build outputs separate between worktrees (for example with `scripts/worktree.sh create [dir_name]`, which seeds `.lake/build` from the root checkout and, when `` exists only on `origin`, checks it out tracking -`origin/`). Run `python3 scripts/check_hygiene.py` to audit `-- upstream:` markers, +`origin/`). Pass `--source-only` to skip the initial copy; the +[cache guide](scripts/cache/README.md#automatic-restoration) explains bootstrap and dependency costs. +Run `python3 scripts/check_hygiene.py` to audit `-- upstream:` markers, forbidden proof tokens, `set_option` justifications, the key order of `references.bib` and that every docstring citation key has an entry there (pass `--check-simp` to also run the heuristic check for non-terminal bare `simp` calls in diff --git a/scripts/cache/README.md b/scripts/cache/README.md index 4c4bcffcc..c79b133c3 100644 --- a/scripts/cache/README.md +++ b/scripts/cache/README.md @@ -107,13 +107,29 @@ the explicit, unstamped fetch command. Cache misses and download failures are op compile what is missing, and the bootstrap never claims that all requested artifacts were available. -`scripts/worktree.sh create` and `scripts/worktree.sh seed` run `scripts/cache/ensure.sh` in the -worktree after seeding `.lake` caches. The helper never points a worktree at the primary checkout, -refuses targets or destination cache symlinks that do, isolates dependency `.git` directories and +By default, `scripts/worktree.sh create` and `scripts/worktree.sh seed` run +`scripts/cache/ensure.sh` in the worktree after seeding `.lake` caches. The helper never points a +worktree at the primary checkout, refuses targets or destination cache symlinks that do, +isolates dependency `.git` directories and `gitdir:` pointer files so Git operations in a worktree cannot modify the primary checkout's `HEAD` or `index`, and dereferences any package symlink whose target is absolute or escapes the package directory. Pass `--copy-cslib` or `--copy-packages` when package sources must change. +When the primary checkout's outputs are changing or use different pins, create a worktree without +copying its initial `.lake` contents: + +```bash +scripts/worktree.sh create feature/example example origin/main --source-only +``` + +`--source-only` skips initial root and dependency outputs, package sources and package Git controls. +The same target and cache isolation checks still run before bootstrap. Bootstrap remains automatic +unless `COMPLEXITYLIB_WORKTREE_SKIP_CACHE_BOOTSTRAP=1` or the usual cache opt-out is set; it may +populate the new checkout with independently materialized dependencies and restored outputs. +Lake can reuse its immutable artifact cache, but expect dependency downloads and disk use for +independent package checkouts, and compilation when outputs are unavailable. This option cannot +be combined with `--copy-cslib` or `--copy-packages`; the default seeded behavior is unchanged. + ## Trust and privacy Downloaded `.olean` files are trusted by Lean: imported modules are not re-checked by the diff --git a/scripts/test_worktree.py b/scripts/test_worktree.py index 2ef67c03a..6b2acbdf9 100644 --- a/scripts/test_worktree.py +++ b/scripts/test_worktree.py @@ -98,6 +98,36 @@ def upstream(self, wt: pathlib.Path) -> str | None: ) return proc.stdout.strip() if proc.returncode == 0 else None + def bootstrap_probe(self) -> dict[str, str]: + ensure = self.work / "scripts/cache/ensure.sh" + ensure.parent.mkdir(parents=True, exist_ok=True) + ensure.write_text( + '#!/usr/bin/env bash\nset -eu\n' + 'printf "%s\\n" "$PWD" >> "$BOOTSTRAP_LOG"\n' + 'printf "%s\\n" "$0" > .bootstrap-script\n' + 'if [ -e .lake ]; then printf seeded; else printf empty; fi > .bootstrap-entry\n' + 'mkdir -p .lake/build\n' + 'printf fetched > .lake/build/bootstrap-artifact\n', + encoding="utf-8", + ) + ensure.chmod(0o755) + return {**GIT_ENV, "COMPLEXITYLIB_WORKTREE_SKIP_CACHE_BOOTSTRAP": "0", + "BOOTSTRAP_LOG": str(self.tmp / "bootstrap.log")} + + def primary_caches(self) -> pathlib.Path: + package = self.work / ".lake/packages/cslib" + package.mkdir(parents=True) + git(package, "init", "--quiet", "-b", "main") + (package / "Source.lean").write_text("package source\n", encoding="utf-8") + git(package, "add", "Source.lean") + git(package, "commit", "--quiet", "-m", "dependency") + for path in (".lake/build/root-output", ".lake/config/lakefile.olean", + ".lake/packages/cslib/.lake/build/dependency-output"): + target = self.work / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("primary output\n", encoding="utf-8") + return package + def test_remote_only_branch_tracks_origin(self) -> None: proc = self.create("feature/takeover", "takeover") self.assertEqual(proc.returncode, 0, proc.stderr) @@ -133,6 +163,125 @@ def test_conflicting_copy_flags_are_refused(self) -> None: self.assertIn("mutually exclusive", proc.stderr) self.assertFalse((self.work / ".worktrees/fresh").exists()) + def test_source_only_conflicts_with_copy_flags_in_either_order(self) -> None: + for flag in ("--copy-cslib", "--copy-packages"): + for flags in (("--source-only", flag), (flag, "--source-only")): + with self.subTest(flags=flags): + proc = self.create("feature/fresh", "fresh", *flags) + self.assertNotEqual(proc.returncode, 0) + self.assertIn("cannot be combined", proc.stderr) + self.assertFalse((self.work / ".worktrees/fresh").exists()) + self.assertEqual(git(self.work, "branch", "--list", "feature/fresh"), "") + + def test_source_only_bootstraps_without_copying_sources_outputs_or_controls(self) -> None: + package = self.primary_caches() + before_head = (package / ".git/HEAD").read_bytes() + env = self.bootstrap_probe() + git(self.work, "add", "scripts/cache/ensure.sh") + git(self.work, "commit", "--quiet", "-m", "fixture bootstrap") + result = self.create("feature/source-only", "--source-only", "source-only", "HEAD", env=env) + self.assertEqual(result.returncode, 0, result.stderr) + wt = self.work / ".worktrees/source-only" + self.assertEqual((wt / ".bootstrap-entry").read_text(), "empty") + self.assertEqual((wt / ".lake/build/bootstrap-artifact").read_text(), "fetched") + self.assertFalse((wt / ".lake/packages").exists()) + self.assertFalse((wt / ".lake/config").exists()) + self.assertFalse((wt / ".lake/build/root-output").exists()) + script = pathlib.Path((wt / ".bootstrap-script").read_text().strip()) + if not script.is_absolute(): + script = wt / script + self.assertEqual(script.resolve(), wt / "scripts/cache/ensure.sh") + self.assertEqual((package / ".git/HEAD").read_bytes(), before_head) + for path in (".lake/build/root-output", ".lake/config/lakefile.olean", + ".lake/packages/cslib/.lake/build/dependency-output"): + self.assertEqual((self.work / path).read_text(), "primary output\n") + self.assertFalse((self.work / ".lake/build/bootstrap-artifact").exists()) + self.assertEqual(pathlib.Path(self.tmp / "bootstrap.log").read_text().strip(), str(wt)) + + def test_default_create_still_seeds_before_bootstrap(self) -> None: + package = self.primary_caches() + env = self.bootstrap_probe() + result = self.create("feature/seeded", "seeded", env=env) + self.assertEqual(result.returncode, 0, result.stderr) + wt = self.work / ".worktrees/seeded" + self.assertEqual((wt / ".bootstrap-entry").read_text(), "seeded") + for path in (".lake/build/root-output", ".lake/config/lakefile.olean", + ".lake/packages/cslib/.lake/build/dependency-output"): + primary, copied = self.work / path, wt / path + self.assertEqual(copied.read_bytes(), primary.read_bytes()) + self.assertFalse(os.path.samefile(primary, copied)) + copied_package = wt / ".lake/packages/cslib" + self.assertTrue(os.path.samefile(package / "Source.lean", copied_package / "Source.lean")) + self.assertNotEqual(git(package, "rev-parse", "--absolute-git-dir"), + git(copied_package, "rev-parse", "--absolute-git-dir")) + self.assertFalse((self.work / ".lake/build/bootstrap-artifact").exists()) + + def test_source_only_respects_explicit_bootstrap_opt_out(self) -> None: + self.primary_caches() + env = {**self.bootstrap_probe(), "COMPLEXITYLIB_WORKTREE_SKIP_CACHE_BOOTSTRAP": "1"} + result = self.create("feature/no-bootstrap", "no-bootstrap", "--source-only", env=env) + self.assertEqual(result.returncode, 0, result.stderr) + wt = self.work / ".worktrees/no-bootstrap" + self.assertFalse((wt / ".lake").exists()) + self.assertFalse((self.tmp / "bootstrap.log").exists()) + + def test_source_only_takeover_tracks_origin_without_initial_copies(self) -> None: + self.primary_caches() + result = self.create("feature/takeover", "takeover", "--source-only") + self.assertEqual(result.returncode, 0, result.stderr) + wt = self.work / ".worktrees/takeover" + self.assertEqual(git(wt, "rev-parse", "HEAD"), self.feature_sha) + self.assertEqual(self.upstream(wt), "origin/feature/takeover") + self.assertFalse((wt / ".lake").exists()) + + def test_both_create_modes_refuse_existing_target_and_cache_symlinks_before_bootstrap(self) -> None: + env = self.bootstrap_probe() + protected = self.work / "protected" + protected.mkdir() + sentinel = protected / "sentinel" + sentinel.write_text("primary content\n", encoding="utf-8") + for mode in ((), ("--source-only",)): + for path in (".", ".lake", ".lake/packages", ".lake/build", ".lake/config", + ".lake/packages/cslib", ".lake/packages/cslib/.lake", + ".lake/packages/cslib/.lake/build", ".lake/packages/cslib/.lake/config"): + with self.subTest(mode=mode, path=path): + name = f"existing-{len(mode)}-{path.replace('/', '-')}" + wt = self.work / ".worktrees" / name + link = wt if path == "." else wt / path + link.parent.mkdir(parents=True, exist_ok=True) + link.symlink_to(protected, target_is_directory=True) + before = git(self.work, "worktree", "list", "--porcelain") + result = self.create(f"feature/{name}", name, *mode, env=env) + self.assertNotEqual(result.returncode, 0) + self.assertIn("primary checkout" if path == "." else "symlink", result.stderr) + self.assertEqual(git(self.work, "worktree", "list", "--porcelain"), before) + self.assertFalse((self.tmp / "bootstrap.log").exists()) + self.assertEqual(sentinel.read_text(), "primary content\n") + + def test_both_create_modes_refuse_checked_out_cache_symlinks_before_bootstrap(self) -> None: + env = self.bootstrap_probe() + protected = self.work / "protected" + protected.mkdir() + sentinel = protected / "sentinel" + sentinel.write_text("primary content\n", encoding="utf-8") + for index, path in enumerate((".lake/build", ".lake/packages/cslib/.lake/build")): + link = self.work / path + link.parent.mkdir(parents=True, exist_ok=True) + link.symlink_to(protected, target_is_directory=True) + git(self.work, "add", path) + git(self.work, "commit", "--quiet", "-m", "fixture with unsafe cache link") + for mode in ((), ("--source-only",)): + with self.subTest(path=path, mode=mode): + name = f"checked-out-{index}-{len(mode)}" + result = self.create(f"feature/{name}", name, "HEAD", *mode, env=env) + self.assertNotEqual(result.returncode, 0) + self.assertIn("destination cache symlink", result.stderr) + self.assertTrue((self.work / ".worktrees" / name / path).is_symlink()) + self.assertFalse((self.tmp / "bootstrap.log").exists()) + self.assertEqual(sentinel.read_text(), "primary content\n") + git(self.work, "rm", "--quiet", path) + git(self.work, "commit", "--quiet", "-m", "remove unsafe fixture cache link") + def test_create_isolates_seeded_dependency_caches(self) -> None: paths = [pathlib.Path(".lake/packages/cslib/.lake") / part for part in ("build/trace", "config/lakefile.olean")] @@ -291,7 +440,8 @@ def test_existing_cache_is_preserved_on_repeated_seed(self) -> None: def test_destination_cache_symlinks_are_refused_before_writing(self) -> None: for path in (".lake", ".lake/packages", ".lake/build", ".lake/config", - ".lake/packages/cslib"): + ".lake/packages/cslib", ".lake/packages/cslib/.lake", + ".lake/packages/cslib/.lake/build", ".lake/packages/cslib/.lake/config"): with self.subTest(path=path): target = self.tmp / path.replace("/", "-") external = self.tmp / (target.name + "-external") diff --git a/scripts/worktree.sh b/scripts/worktree.sh index 4c761006b..d0442bb8b 100755 --- a/scripts/worktree.sh +++ b/scripts/worktree.sh @@ -1,9 +1,9 @@ #!/usr/bin/env bash -# Manage isolated git worktrees under .worktrees/ with pre-seeded .lake caches. +# Manage isolated git worktrees under .worktrees/, optionally seeding .lake caches. # # Usage: -# scripts/worktree.sh create [dir_name] [base_ref] [--copy-cslib | --copy-packages] -# [--force-reset] +# scripts/worktree.sh create [dir_name] [base_ref] +# [--copy-cslib | --copy-packages | --source-only] [--force-reset] # scripts/worktree.sh seed [--copy-cslib | --copy-packages] # scripts/worktree.sh list # scripts/worktree.sh prune-merged [base_ref] [--dry-run] @@ -30,6 +30,10 @@ # worktree unless `COMPLEXITYLIB_WORKTREE_SKIP_CACHE_BOOTSTRAP=1` is set. # Do not edit shared package sources. `--copy-cslib` also copies cslib's sources # (for upstream edits or a pin bump); `--copy-packages` copies every package's sources. +# `create --source-only` skips all initial .lake copies, including package sources and Git +# controls; Lake materializes dependencies normally and may reuse its immutable artifact cache. +# It still checks isolation and bootstraps, unless bootstrap is explicitly disabled as above. +# It cannot be combined with either --copy-* flag. # Seeding refuses the primary checkout and skips existing destination caches. # # Pruning considers registered worktrees directly under `.worktrees/`, retaining locked, @@ -305,15 +309,26 @@ refuse_primary_or_symlink_target() { echo "Refusing to seed through destination package symlink: $pkg_entry" >&2 return 1 fi + for path in "$pkg_entry/.lake" "$pkg_entry/.lake/build" "$pkg_entry/.lake/config"; do + if [ -L "$path" ]; then + echo "Refusing to seed through destination cache symlink: $path" >&2 + return 1 + fi + done done fi } -# seed_lake , where copy_mode is `none`, `cslib` or `all`. -seed_lake() { +# prepare_lake [source_only], where copy_mode is `none`, `cslib` or `all`. +prepare_lake() { local wt_path="$1" local copy_mode="${2:-none}" + local source_only="${3:-false}" refuse_primary_or_symlink_target "$wt_path" "seed" + if [ "$source_only" = "true" ]; then + bootstrap_worktree_cache "$wt_path" + return 0 + fi if [ ! -d "$ROOT/.lake" ]; then echo "No root .lake directory found at $ROOT/.lake; skipping cache seed." bootstrap_worktree_cache "$wt_path" @@ -361,15 +376,18 @@ shift || true case "$cmd" in create) - branch="${1:?Usage: scripts/worktree.sh create [dir_name] [base_ref] [--copy-cslib | --copy-packages] [--force-reset]}" + branch="${1:?Usage: scripts/worktree.sh create [dir_name] [base_ref] [--copy-cslib | --copy-packages | --source-only] [--force-reset]}" shift dir_name="" base_ref="" copy_mode="none" + source_only="false" force_reset="false" for arg in "$@"; do if [ "$arg" = "--copy-cslib" ] || [ "$arg" = "--copy-packages" ]; then copy_mode="$(copy_mode_flag "$copy_mode" "$arg")" + elif [ "$arg" = "--source-only" ]; then + source_only="true" elif [ "$arg" = "--force-reset" ]; then force_reset="true" elif [ -z "$dir_name" ]; then @@ -381,6 +399,10 @@ case "$cmd" in exit 1 fi done + if [ "$source_only" = "true" ] && [ "$copy_mode" != "none" ]; then + echo "--source-only cannot be combined with --copy-cslib or --copy-packages." >&2 + exit 1 + fi if [ -z "$dir_name" ]; then dir_name="${branch//\//-}" fi @@ -390,7 +412,7 @@ case "$cmd" in if [ "$force_reset" = "true" ]; then effective_base="${base_ref:-origin/main}" git worktree add -B "$branch" "$wt_path" "$effective_base" - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" "$source_only" echo "Ready: $wt_path (branch $branch reset to $effective_base)" else if [ -n "$base_ref" ]; then @@ -398,7 +420,7 @@ case "$cmd" in exit 1 fi git worktree add "$wt_path" "$branch" - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" "$source_only" echo "Ready: $wt_path (existing branch $branch)" fi else @@ -413,17 +435,17 @@ case "$cmd" in fi if [ -n "$base_ref" ]; then git worktree add --no-track -b "$branch" "$wt_path" "$base_ref" - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" "$source_only" echo "Ready: $wt_path (new branch $branch from $base_ref; origin/$branch ignored by --force-reset)" else git worktree add --track -b "$branch" "$wt_path" "origin/$branch" - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" "$source_only" echo "Ready: $wt_path (branch $branch tracking origin/$branch)" fi else effective_base="${base_ref:-origin/main}" git worktree add --no-track -b "$branch" "$wt_path" "$effective_base" - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" "$source_only" echo "Ready: $wt_path (new branch $branch from $effective_base)" fi fi @@ -440,7 +462,7 @@ case "$cmd" in exit 1 fi done - seed_lake "$wt_path" "$copy_mode" + prepare_lake "$wt_path" "$copy_mode" echo "Seeded .lake cache in $wt_path" ;; list) From 57b790ae2213276f93371db7f21a01656a9ef6b3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 19:16:23 -0400 Subject: [PATCH 2/2] fix(dev): reject nested destination cache symlinks Scan root cache trees and dependency .lake trees without following links before seeding or source-only bootstrap. Leave package source and Git-control trees outside this check, and fail on unreadable cache traversal. The new real-repository write probe reproduced bootstrap writes through nested root and package build/lib/lean links in both creation modes before this fix. It now requires rejection before bootstrap and unchanged primary-fixture sentinels. Existing-target coverage includes the same nested paths. AI assistance: Codex implemented this bounded follow-up for #1675 after coordinator review found the bypass. Focused 36-test worktree suite passes (one unsupported-reftable skip); full final validation follows on this source. No Lean, curated abstract, or PDF-rendering changes. --- scripts/cache/README.md | 4 +++- scripts/test_worktree.py | 32 +++++++++++++++++++++++++++- scripts/worktree.sh | 46 ++++++++++++++++++++++++++-------------- 3 files changed, 64 insertions(+), 18 deletions(-) diff --git a/scripts/cache/README.md b/scripts/cache/README.md index c79b133c3..6bd4aa3f5 100644 --- a/scripts/cache/README.md +++ b/scripts/cache/README.md @@ -123,7 +123,9 @@ scripts/worktree.sh create feature/example example origin/main --source-only ``` `--source-only` skips initial root and dependency outputs, package sources and package Git controls. -The same target and cache isolation checks still run before bootstrap. Bootstrap remains automatic +The same target and cache isolation checks still run before bootstrap. Both modes refuse existing +symlinks anywhere in root cache trees or dependency `.lake` trees, including nested output paths; +package source and Git-control trees are not traversed by this check. Bootstrap remains automatic unless `COMPLEXITYLIB_WORKTREE_SKIP_CACHE_BOOTSTRAP=1` or the usual cache opt-out is set; it may populate the new checkout with independently materialized dependencies and restored outputs. Lake can reuse its immutable artifact cache, but expect dependency downloads and disk use for diff --git a/scripts/test_worktree.py b/scripts/test_worktree.py index 6b2acbdf9..afe66ab90 100644 --- a/scripts/test_worktree.py +++ b/scripts/test_worktree.py @@ -243,7 +243,8 @@ def test_both_create_modes_refuse_existing_target_and_cache_symlinks_before_boot for mode in ((), ("--source-only",)): for path in (".", ".lake", ".lake/packages", ".lake/build", ".lake/config", ".lake/packages/cslib", ".lake/packages/cslib/.lake", - ".lake/packages/cslib/.lake/build", ".lake/packages/cslib/.lake/config"): + ".lake/packages/cslib/.lake/build", ".lake/packages/cslib/.lake/config", + ".lake/build/lib/lean", ".lake/packages/cslib/.lake/build/lib/lean"): with self.subTest(mode=mode, path=path): name = f"existing-{len(mode)}-{path.replace('/', '-')}" wt = self.work / ".worktrees" / name @@ -282,6 +283,35 @@ def test_both_create_modes_refuse_checked_out_cache_symlinks_before_bootstrap(se git(self.work, "rm", "--quiet", path) git(self.work, "commit", "--quiet", "-m", "remove unsafe fixture cache link") + def test_nested_cache_links_cannot_redirect_bootstrap_writes_to_primary(self) -> None: + env = self.bootstrap_probe() + ensure = self.work / "scripts/cache/ensure.sh" + with ensure.open("a", encoding="utf-8") as stream: + stream.write('printf altered > "$BOOTSTRAP_WRITE_PATH/sentinel"\n') + protected = self.work / "protected" + protected.mkdir() + sentinel = protected / "sentinel" + for index, path in enumerate((".lake/build/lib/lean", + ".lake/packages/cslib/.lake/build/lib/lean")): + link = self.work / path + link.parent.mkdir(parents=True, exist_ok=True) + link.symlink_to(protected, target_is_directory=True) + git(self.work, "add", path) + git(self.work, "commit", "--quiet", "-m", "fixture with nested cache link") + for mode in ((), ("--source-only",)): + with self.subTest(path=path, mode=mode): + sentinel.write_text("primary content\n", encoding="utf-8") + log = self.tmp / "bootstrap.log" + log.unlink(missing_ok=True) + name = f"nested-{index}-{len(mode)}" + result = self.create(f"feature/{name}", name, "HEAD", *mode, + env={**env, "BOOTSTRAP_WRITE_PATH": path}) + self.assertEqual((result.returncode != 0, log.exists(), sentinel.read_text()), + (True, False, "primary content\n"), result.stderr) + self.assertIn("destination cache symlink", result.stderr) + git(self.work, "rm", "--quiet", path) + git(self.work, "commit", "--quiet", "-m", "remove nested fixture cache link") + def test_create_isolates_seeded_dependency_caches(self) -> None: paths = [pathlib.Path(".lake/packages/cslib/.lake") / part for part in ("build/trace", "config/lakefile.olean")] diff --git a/scripts/worktree.sh b/scripts/worktree.sh index d0442bb8b..af8cf49de 100755 --- a/scripts/worktree.sh +++ b/scripts/worktree.sh @@ -301,22 +301,36 @@ refuse_primary_or_symlink_target() { esac fi done - if [ -d "$wt_path/.lake/packages" ]; then - local pkg_entry - shopt -s dotglob nullglob - for pkg_entry in "$wt_path/.lake/packages"/*; do - if [ -L "$pkg_entry" ]; then - echo "Refusing to seed through destination package symlink: $pkg_entry" >&2 - return 1 - fi - for path in "$pkg_entry/.lake" "$pkg_entry/.lake/build" "$pkg_entry/.lake/config"; do - if [ -L "$path" ]; then - echo "Refusing to seed through destination cache symlink: $path" >&2 - return 1 - fi - done - done - fi + # Check nested cache links without traversing package source or Git-control trees. Checking + # only build/config themselves misses links such as .lake/build/lib/lean before bootstrap. + python3 - "$wt_path/.lake" <<'PY' +import os, pathlib, sys + +def refuse_link(path: pathlib.Path, kind: str = "cache") -> None: + if path.is_symlink(): + raise SystemExit(f"Refusing to seed through destination {kind} symlink: {path}") + +def fail_walk(error: OSError) -> None: + raise error + +def check_cache(root: pathlib.Path, skip_packages: bool = False) -> None: + refuse_link(root) + for directory, dirs, files in os.walk(root, followlinks=False, onerror=fail_walk): + for name in dirs + files: + refuse_link(pathlib.Path(directory) / name) + if skip_packages and pathlib.Path(directory) == root: + dirs[:] = [name for name in dirs if name != "packages"] + +cache = pathlib.Path(sys.argv[1]) +if cache.exists(): + check_cache(cache, skip_packages=True) + packages = cache / "packages" + if packages.is_dir(): + for package in packages.iterdir(): + refuse_link(package, "package") + if (package / ".lake").exists() or (package / ".lake").is_symlink(): + check_cache(package / ".lake") +PY } # prepare_lake [source_only], where copy_mode is `none`, `cslib` or `all`.