feat: add cache service and package archive flows

.github/workflows/ci.yaml

@@ -35,8 +35,7 @@ jobs:
       run: |
         # Test basic CLI commands
         leanup --help
-        leanup init
-        leanup status
+        leanup cache --help
         leanup repo --help
         leanup repo install lean-zh/leanup
         leanup repo install lean-zh/repl

README.md

@@ -24,7 +24,6 @@
 - **⚡ 项目初始化**: 快速创建固定 Lean 版本的项目，并复用同版本 mathlib 缓存
 - **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows
 - **📦 简单易用**: 通过 `pip install leanup` 快速安装
-- **🔄 命令代理**: 透明代理所有 elan 命令，无缝体验
 
 ## 🚀 快速开始
 
@@ -49,8 +48,6 @@ leanup --help
 # 快速初始化一个 Lean + mathlib 项目
 leanup setup ./Demo --lean-version v4.27.0
 
-# 如需手动透传 elan，也可以继续使用
-leanup elan toolchain list
 ```
 
 ## 📖 详细使用指南
@@ -113,7 +110,7 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force
 规则说明：
 
 - `--dependency-mode` 支持 `symlink` 和 `copy`
-- 默认缓存目录为 `LEANUP_CACHE_DIR/setup/mathlib/<version>/packages`
+- 默认缓存目录为 `LEANUP_CACHE_DIR/mathlib/packages/<version>/packages`
 - 如果已有 `packages` 缓存，则按 `symlink` 或 `copy` 的方式放进项目
 - 如果缓存不存在，则会自动执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存
 - `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装
@@ -122,19 +119,44 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force
 
 ```bash
 # 查看 LeanUp 已有缓存版本
-leanup mathlib cache list
+leanup cache list
 
-# 进入一个 Lean 仓库后，把当前仓库的 .lake/packages 打包到指定目录
-cd /path/to/repo
-leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache
+# 查看远端服务已有缓存版本和下载 URL
+leanup cache list --base-url http://127.0.0.1:8000
+
+# 在临时目录创建某个 Lean 版本对应的共享 mathlib packages 缓存
+leanup cache create v4.22.0
+
+# 将本地缓存里的 packages/<version>/packages 打包成 archives/<version>/packages.tar.gz
+leanup cache pack v4.22.0
+
+# 或者使用指定缓存根
+leanup cache pack v4.22.0 --output-dir /path/to/cache
+
+# 从 LeanUp cache 服务下载 packages.tar.gz，并解压到本地缓存根
+leanup cache get v4.22.0 --base-url http://127.0.0.1:8000
+
+# 启动本地缓存服务：
+# - /f/... 路由给 lake exe cache get 使用
+# - /packages/... 路由给 leanup cache get 使用
+leanup cache serve
+
+# 让 mathlib 官方 cache client 改走 LeanUp 服务
+export MATHLIB_CACHE_GET_URL=http://127.0.0.1:8000
+lake exe cache get
 
 # 如需关闭并发压缩，可以显式禁用 pigz
-leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --no-pigz
+leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
 ```
 
 - 默认会在本机存在 `pigz` 时启用并发压缩
 - 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包
 - `--no-pigz` 可显式关闭并发压缩
+- `leanup cache create` 会在 `tempfile` 临时工作目录中执行 `lake update` 和 `lake exe cache get`，然后把 `.lake/packages` 回填到 `mathlib/packages/<version>/packages`，再生成 `mathlib/archives/<version>/packages.tar.gz`
+- `leanup cache pack` 会从 `mathlib/packages/<version>/packages` 生成 `mathlib/archives/<version>/packages.tar.gz`
+- `leanup cache get` 会下载远端 `packages.tar.gz` 到 `mathlib/archives/<version>/packages.tar.gz`，并解压到 `mathlib/packages/<version>/packages`
+- `leanup cache get` 和 `leanup cache pack` 都通过临时文件 / 临时目录完成后再原子替换，避免中途中断破坏缓存
+- `leanup cache serve` 使用 FastAPI/uvicorn 提供服务，并暴露 `/packages/mathlib/index.json` 让其他机器列出远端可用版本
 
 ### 交互式安装
 

docs/getting-started/quickstart.md

@@ -38,31 +38,55 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
 
 说明：
 
-- 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib/<version>/packages`
-- Linux 默认通常对应 `~/.cache/leanup/setup/mathlib/<version>/packages`
+- 共享缓存默认放在 `LEANUP_CACHE_DIR/mathlib/packages/<version>/packages`
+- 归档缓存默认放在 `LEANUP_CACHE_DIR/mathlib/archives/<version>/packages.tar.gz`
+- Linux 默认通常对应 `~/.cache/leanup/mathlib/packages/<version>/packages`
 - `--dependency-mode` 支持 `symlink` 和 `copy`
 - 如果已有 `packages` 缓存，则按 `symlink` 或 `copy` 的方式放进项目
 - 如果缓存不存在，则会自动执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存
 - `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装
-- 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...`
 
 ### 管理 mathlib 缓存
 
 ```bash
 # 查看 LeanUp 已有缓存版本
-leanup mathlib cache list
+leanup cache list
 
-# 进入当前仓库后，打包本仓库的 .lake/packages 到指定目录
-cd /path/to/repo
-leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache
+# 查看远端服务已有缓存版本和下载 URL
+leanup cache list --base-url http://127.0.0.1:8000
+
+# 在 tempfile 临时工作目录中创建某个 Lean 版本的共享 mathlib packages 缓存
+leanup cache create v4.22.0
+
+# 将本地缓存里的 packages/<version>/packages 打包成 archives/<version>/packages.tar.gz
+leanup cache pack v4.22.0
+
+# 或者使用指定缓存根
+leanup cache pack v4.22.0 --output-dir /path/to/cache
+
+# 启动缓存服务：/f/... 给 lake exe cache get，/packages/... 给 leanup cache get
+leanup cache serve
+
+# 让 mathlib 官方 cache client 改走 LeanUp 服务
+export MATHLIB_CACHE_GET_URL=http://127.0.0.1:8000
+lake exe cache get
+
+# 从 LeanUp cache 服务下载 packages.tar.gz，并解压到本地缓存根
+leanup cache get v4.22.0 --base-url http://127.0.0.1:8000
 
 # 如需关闭并发压缩，可以显式禁用 pigz
-leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --no-pigz
+leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
 ```
 
 - 默认会在本机存在 `pigz` 时启用并发压缩
 - 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包
 - `--no-pigz` 可显式关闭并发压缩
+- `leanup cache create` 会在临时目录中执行 `lake update` 和 `lake exe cache get`，再把 `.lake/packages` 回填到 `mathlib/packages/<version>/packages` 并生成 `mathlib/archives/<version>/packages.tar.gz`
+- `leanup cache serve` 的 `.ltar` 路由只做 mathlib 兼容分发；`packages.tar.gz` 是 LeanUp 自定义缓存格式
+- `leanup cache serve` 使用 FastAPI/uvicorn，并提供 `/packages/mathlib/index.json` 供其他机器列出远端可用版本
+- `leanup cache pack` 从 `mathlib/packages/<version>/packages` 生成 `mathlib/archives/<version>/packages.tar.gz`
+- `leanup cache get` 从远端下载 `packages.tar.gz` 到 `mathlib/archives/<version>/packages.tar.gz`，并解压到 `mathlib/packages/<version>/packages`
+- `leanup cache pack` 和 `leanup cache get` 都先写临时文件 / 临时目录，成功后再原子替换正式路径，避免中断损坏缓存
 
 ### 仓库管理
 

docs/index.md

@@ -5,8 +5,11 @@
 ## 功能特性
 
 - `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存
-- `leanup mathlib cache list`：查看本地 mathlib 共享缓存版本
-- `leanup mathlib cache pack`：将当前仓库的 `.lake/packages` 打包为共享缓存归档
+- `leanup cache list`：查看本地或远端 mathlib 共享缓存版本
+- `leanup cache create <version>`：在临时目录创建某个 Lean 版本的 mathlib packages 缓存
+- `leanup cache pack <version>`：将本地缓存里的 packages 目录打包为共享缓存归档
+- `leanup cache get <version>`：从 LeanUp cache 服务下载 `packages.tar.gz` 并解压到本地缓存
+- `leanup cache serve`：提供 `.ltar` 兼容路由和 LeanUp packages 归档下载服务
 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参
 - `leanup repo list`：查看已安装仓库
 

leanup/__init__.py

@@ -2,13 +2,14 @@
 
 __author__ = """Lean-zh Community"""
 __email__ = 'leanprover@outlook.com'
-__version__ = '0.2.1'
+__version__ = '0.2.2'
 
 from .repo import (
     RepoManager,
     ElanManager,
     MathlibCacheManager,
     LeanRepo,
+    CacheCreateResult,
     LeanProjectSetup,
     SetupConfig,
     SetupResult,
@@ -17,6 +18,6 @@
 
 __all__ = [
     'RepoManager', 'ElanManager', 'MathlibCacheManager', 'LeanRepo',
-    'LeanProjectSetup', 'SetupConfig', 'SetupResult',
+    'CacheCreateResult', 'LeanProjectSetup', 'SetupConfig', 'SetupResult',
     "setup_logger", "execute_command", "working_directory"
 ]

leanup/cli/__init__.py

@@ -1,16 +1,9 @@
 import click
-import sys
 
-from leanup.utils.custom_logger import setup_logger
-from leanup.cli.mathlib import mathlib
+from leanup.cli.cache_ops import create_cache, get_cache, list_cache, pack_cache, serve_cache
 from leanup.cli.repo import repo
 from leanup.cli.setup import setup_project
-from leanup.cli.elan_ops import (
-    init_elan,
-    install_lean_toolchain,
-    proxy_elan,
-    show_status,
-)
+from leanup.utils.custom_logger import setup_logger
 
 logger = setup_logger("leanup_cli")
 
@@ -23,39 +16,20 @@ def cli(ctx):
     ctx.ensure_object(dict)
 
 
-@cli.command()
-def init():
-    """Install latest elan"""
-    init_elan()
-
-
-@cli.command()
-@click.argument("version", required=False)
-def install(version):
-    """Install Lean toolchain version via elan"""
-    install_lean_toolchain(version)
+@click.group()
+def cache() -> None:
+    """Manage reusable caches."""
 
 
-@cli.command()
-def status():
-    """Show status information"""
-    show_status()
+cache.add_command(serve_cache)
+cache.add_command(pack_cache)
+cache.add_command(list_cache)
+cache.add_command(get_cache)
+cache.add_command(create_cache)
 
 
 cli.add_command(setup_project)
-cli.add_command(mathlib)
-
-
-@cli.command(context_settings=dict(ignore_unknown_options=True))
-@click.argument("args", nargs=-1, type=click.UNPROCESSED)
-def elan(args):
-    """Proxy elan commands"""
-    try:
-        result = proxy_elan(list(args))
-        sys.exit(result)
-    except KeyboardInterrupt:
-        click.echo("\nInterrupted", err=True)
-        sys.exit(1)
+cli.add_command(cache)
 
 
 cli.add_command(repo)

leanup/cli/cache_ops.py

@@ -0,0 +1,134 @@
+from __future__ import annotations
+
+from pathlib import Path
+
+import click
+import requests
+
+from leanup.const import LEANUP_CACHE_DIR
+from leanup.repo.cache_server import run_cache_server
+from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version
+from leanup.repo.project_setup import LeanProjectSetup
+
+
+PACKAGES_CACHE_ROOT = LEANUP_CACHE_DIR / "mathlib"
+
+
+@click.command(name="pack")
+@click.argument("lean_version")
+@click.option(
+    "--output-dir",
+    type=click.Path(path_type=Path, file_okay=False, dir_okay=True),
+    default=PACKAGES_CACHE_ROOT,
+    help="Mathlib cache root containing packages/<version>/packages and archives/<version>/packages.tar.gz.",
+)
+@click.option(
+    "--pigz/--no-pigz",
+    default=True,
+    help="Use pigz for parallel compression when it is available.",
+)
+def pack_cache(lean_version: str, output_dir: Path, pigz: bool) -> None:
+    """Pack cached packages/<version>/packages into archives/<version>/packages.tar.gz."""
+    manager = MathlibCacheManager(cache_root=output_dir)
+    version = normalize_lean_version(lean_version)
+    packages_dir = manager.ensure_local_cache(version)
+    archive = manager.get_local_archive_path(version)
+
+    if packages_dir is None:
+        raise click.ClickException(
+            f"Packages cache not found: {manager.get_local_packages_dir(version)}. Run 'leanup cache create {version}' or 'leanup cache get {version} --base-url ...' first."
+        )
+
+    try:
+        packed = manager.pack_packages_archive(packages_dir, archive, use_pigz=pigz)
+    except ValueError as exc:
+        raise click.ClickException(str(exc)) from exc
+
+    click.echo(str(packed))
+
+
+@click.command(name="list")
+@click.option(
+    "--base-url",
+    help="Print packages.tar.gz URLs using this base URL, for example http://127.0.0.1:8000.",
+)
+def list_cache(base_url: str | None) -> None:
+    """List available mathlib package caches."""
+    manager = MathlibCacheManager()
+    entries = manager.list_remote_entries(base_url) if base_url else manager.list_entries()
+
+    if not entries:
+        click.echo("No mathlib caches found.")
+        return
+
+    for entry in entries:
+        if base_url:
+            click.echo(f"{entry.version} {manager.build_archive_url(entry.version, base_url)}")
+        else:
+            click.echo(entry.version)
+
+
+@click.command(name="get")
+@click.argument("lean_version")
+@click.option("--base-url", required=True, help="Base URL serving /packages/mathlib/<version>/packages.tar.gz.")
+@click.option(
+    "--cache-dir",
+    type=click.Path(path_type=Path, file_okay=False, dir_okay=True),
+    default=PACKAGES_CACHE_ROOT,
+    help="Mathlib cache root containing packages/<version>/packages and archives/<version>/packages.tar.gz.",
+)
+def get_cache(lean_version: str, base_url: str, cache_dir: Path) -> None:
+    """Download packages.tar.gz into local cache and extract packages/<version>/packages."""
+    manager = MathlibCacheManager(cache_root=cache_dir)
+
+    try:
+        packages_dir = manager.fetch_packages(lean_version, base_url)
+    except (ValueError, requests.RequestException) as exc:
+        raise click.ClickException(str(exc)) from exc
+
+    click.echo(str(packages_dir))
+
+
+@click.command(name="serve")
+@click.option("--host", default="127.0.0.1", show_default=True, help="Host to bind.")
+@click.option("--port", default=8000, show_default=True, type=int, help="Port to bind.")
+@click.option(
+    "--ltar-root",
+    type=click.Path(path_type=Path, file_okay=False, dir_okay=True),
+    default=Path.home() / ".cache" / "mathlib",
+    help="Directory serving raw .ltar files for /f/... routes.",
+)
+@click.option(
+    "--packages-root",
+    type=click.Path(path_type=Path, file_okay=False, dir_okay=True),
+    default=PACKAGES_CACHE_ROOT,
+    help="Mathlib cache root containing packages/ and archives/ subdirectories.",
+)
+def serve_cache(host: str, port: int, ltar_root: Path, packages_root: Path) -> None:
+    """Serve .ltar and packages.tar.gz cache files."""
+    click.echo(f"Serving cache on http://{host}:{port}")
+    click.echo(f"  ltar root: {ltar_root}")
+    click.echo(f"  packages root: {packages_root}")
+    try:
+        run_cache_server(host, port, ltar_root, packages_root)
+    except KeyboardInterrupt:
+        click.echo("\nStopped.", err=True)
+
+
+@click.command(name="create")
+@click.argument("lean_version")
+@click.option(
+    "--pigz/--no-pigz",
+    default=True,
+    help="Use pigz for parallel compression when it is available.",
+)
+def create_cache(lean_version: str, pigz: bool) -> None:
+    """Create shared mathlib cache in a temporary workspace."""
+    setup = LeanProjectSetup()
+    try:
+        result = setup.create_mathlib_cache(lean_version, use_pigz=pigz)
+    except (ValueError, RuntimeError) as exc:
+        raise click.ClickException(str(exc)) from exc
+
+    click.echo(str(result.cache_dir))
+    click.echo(str(result.archive_path))