diff --git a/MANIFEST.in b/MANIFEST.in new file mode 100644 index 0000000..f12587e --- /dev/null +++ b/MANIFEST.in @@ -0,0 +1 @@ +recursive-include leanup/templates *.tmpl diff --git a/README.md b/README.md index 51eb441..24f1b3a 100644 --- a/README.md +++ b/README.md @@ -94,11 +94,11 @@ leanup repo list -n mathlib `leanup setup` 用于快速创建一个固定 Lean 版本的项目，并按需要为 `mathlib` 依赖准备共享缓存。 ```bash -# 创建一个带 mathlib 的项目，默认有缓存就复用，没有缓存就构建 +# 创建一个带 mathlib 的项目，默认有缓存就复用，没有缓存就自动准备缓存 leanup setup ./Demo --lean-version v4.27.0 -# 首次为某个版本准备依赖缓存时，从头构建一次 -leanup setup ./DemoBuild --lean-version v4.27.0 --dependency-mode build +# 使用 copy 模式，把共享缓存复制到项目里 +leanup setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy # 后续同版本项目可直接软链接复用缓存 leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink @@ -112,9 +112,10 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force 规则说明： -- `--dependency-mode symlink` 只在启用 `mathlib` 时可用 +- `--dependency-mode` 支持 `symlink` 和 `copy` - 默认缓存目录为 `LEANUP_CACHE_DIR/setup/mathlib//packages` -- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 +- 如果已有 `packages` 缓存，则按 `symlink` 或 `copy` 的方式放进项目 +- 如果缓存不存在，则会自动执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 - `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装 ### 管理 mathlib 缓存 diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index a51dfe6..ccd3243 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -23,11 +23,11 @@ leanup --help ### 快速创建项目 ```bash -# 创建一个带 mathlib 的 Lean 项目，默认有缓存就复用，没有缓存就构建 +# 创建一个带 mathlib 的 Lean 项目，默认有缓存就复用，没有缓存就自动准备缓存 leanup setup ./Demo --lean-version v4.27.0 -# 首次为某个版本准备缓存时，从头构建依赖 -leanup setup ./DemoBuild --lean-version v4.27.0 --dependency-mode build +# 使用 copy 模式，把共享缓存复制到项目里 +leanup setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy # 后续项目直接复用共享依赖缓存 leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink @@ -40,8 +40,9 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib - 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` - Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` -- `symlink` 模式只对 `mathlib` 项目开放 -- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 +- `--dependency-mode` 支持 `symlink` 和 `copy` +- 如果已有 `packages` 缓存，则按 `symlink` 或 `copy` 的方式放进项目 +- 如果缓存不存在，则会自动执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 - `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装 - 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...` diff --git a/leanup/cli/setup.py b/leanup/cli/setup.py index fe4ffa7..b30a4ff 100644 --- a/leanup/cli/setup.py +++ b/leanup/cli/setup.py @@ -37,9 +37,9 @@ def _require_non_empty(value: str, field_name: str) -> str: @click.option( "--dependency-mode", "-m", - type=click.Choice(["symlink", "build"]), + type=click.Choice(["symlink", "copy"]), default=None, - help="Use cached mathlib packages via symlink, or build dependencies from scratch.", + help="Attach cached mathlib packages via symlink, or copy them into the project.", ) @click.option("--force", "-f", is_flag=True, help="Replace the target directory if it exists.") @click.option( @@ -58,7 +58,7 @@ def setup_project( interactive: bool | None, ) -> None: """Create a Lean project with a pinned toolchain and optional mathlib cache reuse.""" - usage = "Usage: leanup setup [PATH] --lean-version [--name ] [--mathlib/--no-mathlib] [--dependency-mode symlink|build] [--force] [-i|-I]" + usage = "Usage: leanup setup [PATH] --lean-version [--name ] [--mathlib/--no-mathlib] [--dependency-mode symlink|copy] [--force] [-i|-I]" missing_required = path is None or not lean_version interactive, can_prompt, force_interactive, _, need_prompt = ( resolve_interactive_mode( @@ -105,15 +105,15 @@ def setup_project( except ValueError: preview_mode = dependency_mode - default_mode = preview_mode or dependency_mode or ("build" if not mathlib else "symlink") + default_mode = preview_mode or dependency_mode or ("copy" if not mathlib else "symlink") if mathlib: dependency_mode = ask_text( - "Dependency mode (symlink/build)", + "Dependency mode (symlink/copy)", default=default_mode, ).strip() or default_mode else: - dependency_mode = "build" + dependency_mode = "copy" force = ask_confirm("Replace the target directory if it exists?", default=force) @@ -138,7 +138,7 @@ def setup_project( click.echo(f" Dependency mode: {result.dependency_mode}") if result.cache_dir: click.echo(f" Cache dir: {result.cache_dir}") - if result.used_cache: - click.echo(" Reused cached mathlib packages via symlink.") - else: - click.echo(" Refreshed the shared mathlib package cache for this Lean version.") + if result.used_cache: + click.echo(f" Reused cached mathlib packages via {result.dependency_mode}.") + else: + click.echo(" Refreshed the shared mathlib package cache for this Lean version.") diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py index 9d17a17..56c426d 100644 --- a/leanup/repo/project_setup.py +++ b/leanup/repo/project_setup.py @@ -51,7 +51,7 @@ def resolved_dependency_mode(self) -> str: if self.dependency_mode: return self.dependency_mode if not self.mathlib: - return "build" + return "copy" return "symlink" @property @@ -63,8 +63,8 @@ def mathlib_cache_dir(self) -> Path: return MathlibCacheManager().get_local_packages_dir(self.lean_version) def validate(self) -> None: - if self.resolved_dependency_mode not in {"symlink", "build"}: - raise ValueError("Dependency mode must be either 'symlink' or 'build'.") + if self.resolved_dependency_mode not in {"symlink", "copy"}: + raise ValueError("Dependency mode must be either 'symlink' or 'copy'.") if self.resolved_dependency_mode == "symlink" and not self.mathlib: raise ValueError("Dependency symlink mode is only available when mathlib is enabled.") @@ -100,7 +100,7 @@ def setup(self, config: SetupConfig) -> SetupResult: used_cache = False cache_dir = config.mathlib_cache_dir if config.mathlib else None - if config.mathlib and config.resolved_dependency_mode == "symlink": + if config.mathlib and config.resolved_dependency_mode in {"symlink", "copy"}: logger.info("Checking reusable mathlib package cache") used_cache = self._prepare_mathlib_cache(config, project_dir) if used_cache: @@ -119,6 +119,9 @@ def setup(self, config: SetupConfig) -> SetupResult: logger.info("Linking shared packages cache into project") self._link_mathlib_cache(config, project_dir) used_cache = True + elif config.resolved_dependency_mode == "copy": + logger.info("Copying shared packages cache into project") + self._copy_mathlib_cache(config, project_dir) logger.info("Running lake build") self._run_lake_build(project) @@ -322,7 +325,10 @@ def _prepare_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> bool if not cache_dir: return False - self._link_mathlib_cache(config, project_dir) + if config.resolved_dependency_mode == "symlink": + self._link_mathlib_cache(config, project_dir) + elif config.resolved_dependency_mode == "copy": + self._copy_mathlib_cache(config, project_dir) return True def _link_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: @@ -337,6 +343,13 @@ def _link_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: except OSError as exc: raise RuntimeError(f"Failed to create dependency symlink: {exc}") from exc + def _copy_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: + cache_dir = self.cache_manager.get_local_packages_dir(config.lean_version) + packages_dir = project_dir / ".lake" / "packages" + packages_dir.parent.mkdir(parents=True, exist_ok=True) + remove_path(packages_dir) + shutil.copytree(cache_dir, packages_dir, symlinks=True) + def _refresh_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: source_dir = project_dir / ".lake" / "packages" if not source_dir.exists(): diff --git a/setup.cfg b/setup.cfg index 50adf51..e00712e 100644 --- a/setup.cfg +++ b/setup.cfg @@ -30,7 +30,8 @@ install_requires = where = . [options.package_data] -* = *.* +leanup = + templates/mathlib/*.tmpl [options.extras_require] dev = @@ -52,4 +53,4 @@ console_scripts = files = . strict = True warn_unreachable = True -warn_no_return = True \ No newline at end of file +warn_no_return = True diff --git a/tests/test_setup.py b/tests/test_setup.py index b8aa82e..6e9d860 100644 --- a/tests/test_setup.py +++ b/tests/test_setup.py @@ -176,7 +176,7 @@ def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): cache_module.LEANUP_CACHE_DIR = original_cache_dir -def test_setup_build_mode_populates_shared_cache(tmp_path): +def test_setup_copy_mode_populates_shared_cache(tmp_path): class FakeElanManager: def is_elan_installed(self): return True @@ -244,7 +244,7 @@ def fake_lake(self, args): config = SetupConfig( target_dir=target, lean_version="v4.27.0", - dependency_mode="build", + dependency_mode="copy", ) result = manager.setup(config) @@ -254,6 +254,8 @@ def fake_lake(self, args): assert (target / "lakefile.lean").read_text(encoding="utf-8").find('require mathlib from git') >= 0 assert (target / "BuildDemo.lean").exists() assert (target / "BuildDemo" / "Basic.lean").exists() + assert (target / ".lake" / "packages").exists() + assert not (target / ".lake" / "packages").is_symlink() assert config.mathlib_cache_dir.exists() assert (config.mathlib_cache_dir / "mathlib" / "README.md").exists() finally: @@ -352,6 +354,66 @@ def fake_lake(self, args): LeanRepo.lake = original_lake +def test_setup_copy_mode_reuses_shared_cache(tmp_path): + class FakeElanManager: + def is_elan_installed(self): + return True + + def install_elan(self): + return True + + def install_lean(self, version): + return True + + def fake_lake_init(self, name, template=None): + project_dir = self.cwd / name + project_dir.mkdir(parents=True) + (project_dir / "lakefile.lean").write_text(f"template={template}\n", encoding="utf-8") + return "", "", 0 + + def fake_lake_build(self): + return "", "", 0 + + def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): + assert Path(filepath).suffix == ".lean" + return "4.22.0\n", "", 0 + + from leanup.repo import mathlib_cache as cache_module + + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + from leanup.repo.manager import LeanRepo + + original_lake_init = LeanRepo.lake_init + original_lake_build = LeanRepo.lake_build + original_lake_env_lean = LeanRepo.lake_env_lean + LeanRepo.lake_init = fake_lake_init + LeanRepo.lake_build = fake_lake_build + LeanRepo.lake_env_lean = fake_lake_env_lean + + cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" / "mathlib" + _init_fake_package_repo(cached_packages) + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + target = tmp_path / "CopyDemo" + config = SetupConfig(target_dir=target, lean_version="v4.22.0", dependency_mode="copy") + + result = manager.setup(config) + + packages_dir = target / ".lake" / "packages" + assert result.used_cache is True + assert packages_dir.exists() + assert not packages_dir.is_symlink() + assert (packages_dir / "mathlib" / "README.md").exists() + finally: + cache_module.LEANUP_CACHE_DIR = original_cache_dir + LeanRepo.lake_init = original_lake_init + LeanRepo.lake_build = original_lake_build + LeanRepo.lake_env_lean = original_lake_env_lean + + def test_setup_symlink_mode_skips_lake_update_when_manifest_exists(tmp_path): class FakeElanManager: def is_elan_installed(self):