feat: add mathlib and toolchains cache commands

.github/workflows/ci.yaml

@@ -35,7 +35,9 @@ jobs:
       run: |
         # Test basic CLI commands
         leanup --help
-        leanup cache --help
+        leanup mathlib --help
+        leanup serve --help
+        leanup toolchains --help
         leanup repo --help
         leanup repo install lean-zh/leanup
         leanup repo install lean-zh/repl

README.md

@@ -88,23 +88,23 @@ leanup repo list -n mathlib
 
 ### 快速初始化项目
 
-`leanup setup` 用于快速创建一个固定 Lean 版本的项目，并按需要为 `mathlib` 依赖准备共享缓存。
+`leanup mathlib setup` 用于快速创建一个固定 Lean 版本的项目，并按需要为 `mathlib` 依赖准备共享缓存。
 
 ```bash
 # 创建一个带 mathlib 的项目，默认有缓存就复用，没有缓存就自动准备缓存
-leanup setup ./Demo --lean-version v4.27.0
+leanup mathlib setup ./Demo --lean-version v4.27.0
 
 # 使用 copy 模式，把共享缓存复制到项目里
-leanup setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy
+leanup mathlib setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy
 
 # 后续同版本项目可直接软链接复用缓存
-leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink
+leanup mathlib setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink
 
 # 创建不带 mathlib 的纯 Lean 项目
-leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
+leanup mathlib setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
 
 # 指定 Lake 项目名，并覆盖已存在目录
-leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force
+leanup mathlib setup ./Demo --lean-version v4.27.0 --name MyDemo --force
 ```
 
 规则说明：
@@ -119,34 +119,37 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force
 
 ```bash
 # 查看 LeanUp 已有缓存版本
-leanup cache list
+leanup mathlib list --local
 
 # 查看远端服务已有缓存版本和下载 URL
-leanup cache list --base-url http://127.0.0.1:8000
+leanup mathlib list --remote http://127.0.0.1:8000
 
 # 在临时目录创建某个 Lean 版本对应的共享 mathlib packages 缓存
-leanup cache create v4.22.0
+leanup mathlib create v4.22.0
 
 # 将本地缓存里的 packages/<version>/packages 打包成 archives/<version>/packages.tar.gz
-leanup cache pack v4.22.0
+leanup mathlib pack v4.22.0
+
+# 将本地 archive 解压回 packages 目录
+leanup mathlib unpack v4.22.0
 
 # 或者使用指定缓存根
-leanup cache pack v4.22.0 --output-dir /path/to/cache
+leanup mathlib 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
+leanup mathlib get v4.22.0 --remote http://127.0.0.1:8000
 
 # 启动本地缓存服务：
 # - /f/... 路由给 lake exe cache get 使用
 # - /packages/... 路由给 leanup cache get 使用
-leanup cache serve
+leanup serve
 
 # 让 mathlib 官方 cache client 改走 LeanUp 服务
 export MATHLIB_CACHE_GET_URL=http://127.0.0.1:8000
 lake exe cache get
 
 # 如需关闭并发压缩，可以显式禁用 pigz
-leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
+leanup mathlib pack v4.22.0 --output-dir /path/to/cache --no-pigz
 ```
 
 - 默认会在本机存在 `pigz` 时启用并发压缩
@@ -158,6 +161,36 @@ leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
 - `leanup cache get` 和 `leanup cache pack` 都通过临时文件 / 临时目录完成后再原子替换，避免中途中断破坏缓存
 - `leanup cache serve` 使用 FastAPI/uvicorn 提供服务，并暴露 `/packages/mathlib/index.json` 让其他机器列出远端可用版本
 
+### 管理 toolchains 缓存
+
+```bash
+# 查看本地 toolchain 归档
+leanup toolchains list --local
+
+# 查看远端 toolchain 归档
+leanup toolchains list --remote http://127.0.0.1:8000
+
+# 不指定版本时，打包裸的 .elan 基础目录，不包含 toolchains/
+leanup toolchains pack
+
+# 指定版本时，打包 .elan/toolchains 中对应的 Lean toolchain
+leanup toolchains pack v4.28.0
+
+# 从本地归档解压 toolchain 到 .elan/toolchains
+leanup toolchains unpack v4.28.0
+
+# 初始化 .elan：不加 url 时走官方 elan 安装；加 url 时下载 base .elan 归档
+leanup toolchains init
+leanup toolchains init --url http://127.0.0.1:8000
+
+# 从远端下载并解压指定 toolchain
+leanup toolchains get v4.28.0 --remote http://127.0.0.1:8000
+```
+
+- toolchain archives 单独存储在 `LEANUP_CACHE_DIR/toolchains/archives`
+- 解压后的目录语义沿用 `.elan/`
+- 所有下载、压缩、解压都先写临时文件 / 临时目录，成功后再原子替换正式路径
+
 ### 交互式安装
 
 使用 `leanup repo install -i` 时，您可以配置：

docs/getting-started/quickstart.md

@@ -24,16 +24,16 @@ leanup --help
 
 ```bash
 # 创建一个带 mathlib 的 Lean 项目，默认有缓存就复用，没有缓存就自动准备缓存
-leanup setup ./Demo --lean-version v4.27.0
+leanup mathlib setup ./Demo --lean-version v4.27.0
 
 # 使用 copy 模式，把共享缓存复制到项目里
-leanup setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy
+leanup mathlib setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy
 
 # 后续项目直接复用共享依赖缓存
-leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink
+leanup mathlib setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink
 
 # 创建不依赖 mathlib 的纯 Lean 项目
-leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
+leanup mathlib setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
 ```
 
 说明：
@@ -50,32 +50,35 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib
 
 ```bash
 # 查看 LeanUp 已有缓存版本
-leanup cache list
+leanup mathlib list --local
 
 # 查看远端服务已有缓存版本和下载 URL
-leanup cache list --base-url http://127.0.0.1:8000
+leanup mathlib list --remote http://127.0.0.1:8000
 
 # 在 tempfile 临时工作目录中创建某个 Lean 版本的共享 mathlib packages 缓存
-leanup cache create v4.22.0
+leanup mathlib create v4.22.0
 
 # 将本地缓存里的 packages/<version>/packages 打包成 archives/<version>/packages.tar.gz
-leanup cache pack v4.22.0
+leanup mathlib pack v4.22.0
+
+# 将本地 archive 解压回 packages 目录
+leanup mathlib unpack v4.22.0
 
 # 或者使用指定缓存根
-leanup cache pack v4.22.0 --output-dir /path/to/cache
+leanup mathlib pack v4.22.0 --output-dir /path/to/cache
 
 # 启动缓存服务：/f/... 给 lake exe cache get，/packages/... 给 leanup cache get
-leanup cache serve
+leanup 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
+leanup mathlib get v4.22.0 --remote http://127.0.0.1:8000
 
 # 如需关闭并发压缩，可以显式禁用 pigz
-leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
+leanup mathlib pack v4.22.0 --output-dir /path/to/cache --no-pigz
 ```
 
 - 默认会在本机存在 `pigz` 时启用并发压缩
@@ -88,6 +91,30 @@ leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
 - `leanup cache get` 从远端下载 `packages.tar.gz` 到 `mathlib/archives/<version>/packages.tar.gz`，并解压到 `mathlib/packages/<version>/packages`
 - `leanup cache pack` 和 `leanup cache get` 都先写临时文件 / 临时目录，成功后再原子替换正式路径，避免中断损坏缓存
 
+### 管理 toolchains 缓存
+
+```bash
+# 查看本地和远端 toolchain 归档
+leanup toolchains list --local
+leanup toolchains list --remote http://127.0.0.1:8000
+
+# 打包裸的 .elan 基础目录，不包含 toolchains/
+leanup toolchains pack
+
+# 打包、解压、下载具体 Lean toolchain
+leanup toolchains pack v4.28.0
+leanup toolchains unpack v4.28.0
+leanup toolchains get v4.28.0 --remote http://127.0.0.1:8000
+
+# 初始化 .elan：默认走官方 elan；加 url 时下载 base .elan 归档
+leanup toolchains init
+leanup toolchains init --url http://127.0.0.1:8000
+```
+
+- toolchain archives 单独存储在 `LEANUP_CACHE_DIR/toolchains/archives`
+- 解压后的目录语义沿用 `.elan/`
+- 所有下载、压缩、解压都先写临时文件 / 临时目录，成功后再原子替换正式路径
+
 ### 仓库管理
 
 ```bash

docs/index.md

@@ -4,12 +4,14 @@
 
 ## 功能特性
 
-- `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存
-- `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 mathlib setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存
+- `leanup mathlib list`：查看本地或远端 mathlib 共享缓存版本
+- `leanup mathlib create <version>`：在临时目录创建某个 Lean 版本的 mathlib packages 缓存
+- `leanup mathlib pack <version>`：将本地缓存里的 packages 目录打包为共享缓存归档
+- `leanup mathlib unpack <version>`：从本地 archive 解压回 packages 目录
+- `leanup mathlib get <version>`：从 LeanUp 服务下载 `packages.tar.gz` 并解压到本地缓存
+- `leanup serve`：提供 `.ltar` 兼容路由和 LeanUp packages 归档下载服务
+- `leanup toolchains`：管理 `.elan` 基础包和 Lean toolchain 归档
 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参
 - `leanup repo list`：查看已安装仓库
 

leanup/__init__.py

@@ -2,7 +2,7 @@
 
 __author__ = """Lean-zh Community"""
 __email__ = 'leanprover@outlook.com'
-__version__ = '0.2.2'
+__version__ = '0.2.3'
 
 from .repo import (
     RepoManager,

leanup/cli/__init__.py

@@ -1,8 +1,9 @@
 import click
 
-from leanup.cli.cache_ops import create_cache, get_cache, list_cache, pack_cache, serve_cache
+from leanup.cli.cache_ops import create_cache, get_cache, list_cache, pack_cache, serve_cache, unpack_cache
 from leanup.cli.repo import repo
 from leanup.cli.setup import setup_project
+from leanup.cli.toolchains import toolchains
 from leanup.utils.custom_logger import setup_logger
 
 logger = setup_logger("leanup_cli")
@@ -17,19 +18,22 @@ def cli(ctx):
 
 
 @click.group()
-def cache() -> None:
-    """Manage reusable caches."""
+def mathlib() -> None:
+    """Manage mathlib projects and package caches."""
 
 
-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)
+mathlib.add_command(setup_project)
+mathlib.add_command(pack_cache)
+mathlib.add_command(unpack_cache)
+mathlib.add_command(list_cache)
+mathlib.add_command(get_cache)
+mathlib.add_command(create_cache)
 
 
 cli.add_command(setup_project)
-cli.add_command(cache)
+cli.add_command(mathlib)
+cli.add_command(serve_cache)
+cli.add_command(toolchains)
 
 
 cli.add_command(repo)

leanup/cli/cache_ops.py

@@ -47,42 +47,72 @@ def pack_cache(lean_version: str, output_dir: Path, pigz: bool) -> None:
     click.echo(str(packed))
 
 
+@click.command(name="unpack")
+@click.argument("lean_version")
+@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 unpack_cache(lean_version: str, cache_dir: Path) -> None:
+    """Unpack archives/<version>/packages.tar.gz into packages/<version>/packages."""
+    manager = MathlibCacheManager(cache_root=cache_dir)
+    version = normalize_lean_version(lean_version)
+    archive = manager.get_local_archive_path(version)
+
+    try:
+        packages_dir = manager.extract_archive(archive, manager.get_local_packages_dir(version))
+    except ValueError as exc:
+        raise click.ClickException(str(exc)) from exc
+
+    click.echo(str(packages_dir))
+
+
 @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.",
+    "--local",
+    "source",
+    flag_value="local",
+    default=True,
+    help="List local mathlib package caches.",
+)
+@click.option(
+    "--remote",
+    "remote_url",
+    help="List remote mathlib package caches using this base URL.",
 )
-def list_cache(base_url: str | None) -> None:
+def list_cache(source: str, remote_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()
+    entries = manager.list_remote_entries(remote_url) if remote_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)}")
+        if remote_url:
+            click.echo(f"{entry.version} {manager.build_archive_url(entry.version, remote_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("--remote", "remote_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:
+def get_cache(lean_version: str, remote_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)
+        packages_dir = manager.fetch_packages(lean_version, remote_url)
     except (ValueError, requests.RequestException) as exc:
         raise click.ClickException(str(exc)) from exc