fix: package templates and simplify setup cache modes

MANIFEST.in

@@ -0,0 +1 @@
+recursive-include leanup/templates *.tmpl

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/<version>/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 缓存

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/<version>/packages`
 - Linux 默认通常对应 `~/.cache/leanup/setup/mathlib/<version>/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 ...`
 

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 <version> [--name <name>] [--mathlib/--no-mathlib] [--dependency-mode symlink|build] [--force] [-i|-I]"
+    usage = "Usage: leanup setup [PATH] --lean-version <version> [--name <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.")

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():

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
+warn_no_return = True

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):