diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 48759ae..b7a7e16 100644 --- a/.github/workflows/ci.yaml +++ b/.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 diff --git a/README.md b/README.md index 24f1b3a..84717eb 100644 --- a/README.md +++ b/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//packages` +- 默认缓存目录为 `LEANUP_CACHE_DIR/mathlib/packages//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//packages 打包成 archives//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//packages`，再生成 `mathlib/archives//packages.tar.gz` +- `leanup cache pack` 会从 `mathlib/packages//packages` 生成 `mathlib/archives//packages.tar.gz` +- `leanup cache get` 会下载远端 `packages.tar.gz` 到 `mathlib/archives//packages.tar.gz`，并解压到 `mathlib/packages//packages` +- `leanup cache get` 和 `leanup cache pack` 都通过临时文件 / 临时目录完成后再原子替换，避免中途中断破坏缓存 +- `leanup cache serve` 使用 FastAPI/uvicorn 提供服务，并暴露 `/packages/mathlib/index.json` 让其他机器列出远端可用版本 ### 交互式安装 diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index ccd3243..e793bfc 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -38,31 +38,55 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib 说明： -- 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` -- Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` +- 共享缓存默认放在 `LEANUP_CACHE_DIR/mathlib/packages//packages` +- 归档缓存默认放在 `LEANUP_CACHE_DIR/mathlib/archives//packages.tar.gz` +- Linux 默认通常对应 `~/.cache/leanup/mathlib/packages//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//packages 打包成 archives//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//packages` 并生成 `mathlib/archives//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//packages` 生成 `mathlib/archives//packages.tar.gz` +- `leanup cache get` 从远端下载 `packages.tar.gz` 到 `mathlib/archives//packages.tar.gz`，并解压到 `mathlib/packages//packages` +- `leanup cache pack` 和 `leanup cache get` 都先写临时文件 / 临时目录，成功后再原子替换正式路径，避免中断损坏缓存 ### 仓库管理 diff --git a/docs/index.md b/docs/index.md index bbf4679..4cb4473 100644 --- a/docs/index.md +++ b/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 `：在临时目录创建某个 Lean 版本的 mathlib packages 缓存 +- `leanup cache pack `：将本地缓存里的 packages 目录打包为共享缓存归档 +- `leanup cache get `：从 LeanUp cache 服务下载 `packages.tar.gz` 并解压到本地缓存 +- `leanup cache serve`：提供 `.ltar` 兼容路由和 LeanUp packages 归档下载服务 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 - `leanup repo list`：查看已安装仓库 diff --git a/leanup/__init__.py b/leanup/__init__.py index d7b5f67..8877138 100644 --- a/leanup/__init__.py +++ b/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" ] diff --git a/leanup/cli/__init__.py b/leanup/cli/__init__.py index 568d605..70564eb 100644 --- a/leanup/cli/__init__.py +++ b/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) diff --git a/leanup/cli/cache_ops.py b/leanup/cli/cache_ops.py new file mode 100644 index 0000000..bff83dd --- /dev/null +++ b/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//packages and archives//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//packages into archives//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//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//packages and archives//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//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)) diff --git a/leanup/cli/elan_ops.py b/leanup/cli/elan_ops.py deleted file mode 100644 index d0478c3..0000000 --- a/leanup/cli/elan_ops.py +++ /dev/null @@ -1,55 +0,0 @@ -from __future__ import annotations - -import click - -from leanup.repo.elan import ElanManager - - -def ensure_elan_installed() -> ElanManager: - elan_manager = ElanManager() - if elan_manager.is_elan_installed(): - return elan_manager - - click.echo("Installing elan...") - if not elan_manager.install_elan(): - raise click.ClickException("Failed to install elan") - click.echo("✓ elan installed successfully") - return elan_manager - - -def init_elan() -> None: - elan_manager = ElanManager() - if elan_manager.is_elan_installed(): - click.echo("✓ elan is already installed") - return - click.echo("Installing elan...") - if not elan_manager.install_elan(): - raise click.ClickException("Failed to install elan") - click.echo("✓ elan installed successfully") - - -def install_lean_toolchain(version: str | None) -> None: - elan_manager = ensure_elan_installed() - requested = version or "stable" - if not elan_manager.install_lean(version): - raise click.ClickException(f"Failed to install Lean toolchain {requested}") - click.echo(f"✓ Lean toolchain {requested} installed") - - -def show_status() -> None: - elan_manager = ElanManager() - click.echo("=== LeanUp Status ===") - if not elan_manager.is_elan_installed(): - click.echo("elan: ✗ not installed") - return - version = elan_manager.get_elan_version() - click.echo(f"\nelan version: {version}") - click.echo("---------------------\n") - elan_manager.proxy_elan_command(["show"]) - - -def proxy_elan(args: list[str]) -> int: - elan_manager = ElanManager() - if not elan_manager.is_elan_installed(): - raise click.ClickException("elan is not installed. Run 'leanup init' first.") - return elan_manager.proxy_elan_command(list(args)) diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py deleted file mode 100644 index 75b0352..0000000 --- a/leanup/cli/mathlib.py +++ /dev/null @@ -1,69 +0,0 @@ -from __future__ import annotations - -from pathlib import Path - -import click - -from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version - - -@click.group() -def mathlib() -> None: - """Manage mathlib-specific helpers and caches.""" - - -@mathlib.group() -def cache() -> None: - """Manage reusable mathlib package caches.""" - - -@cache.command(name="list") -def list_cache() -> None: - """List available mathlib caches.""" - manager = MathlibCacheManager() - entries = manager.list_entries() - - if not entries: - click.echo("No mathlib caches found.") - return - - for entry in entries: - click.echo(entry.version) - - -@cache.command(name="pack") -@click.option( - "--repo-dir", - type=click.Path(path_type=Path, file_okay=False, dir_okay=True), - default=Path.cwd, - help="Lean repository directory containing .lake/packages.", -) -@click.option( - "--output-dir", - type=click.Path(path_type=Path, file_okay=False, dir_okay=True), - required=True, - help="Directory where /packages.tar.gz will be written.", -) -@click.option( - "--lean-version", - required=True, - help="Lean version like v4.22.0.", -) -@click.option( - "--pigz/--no-pigz", - default=True, - help="Use pigz for parallel compression when it is available.", -) -def pack_cache(repo_dir: Path, output_dir: Path, lean_version: str, pigz: bool) -> None: - """Pack current repository .lake/packages into a versioned cache archive.""" - manager = MathlibCacheManager() - version = normalize_lean_version(lean_version) - packages_dir = repo_dir / ".lake" / "packages" - archive = output_dir / version / "packages.tar.gz" - - 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)) diff --git a/leanup/repo/__init__.py b/leanup/repo/__init__.py index 4061622..3eebe85 100644 --- a/leanup/repo/__init__.py +++ b/leanup/repo/__init__.py @@ -3,13 +3,14 @@ from .manager import RepoManager, LeanRepo from .elan import ElanManager from .mathlib_cache import MathlibCacheManager -from .project_setup import LeanProjectSetup, SetupConfig, SetupResult +from .project_setup import CacheCreateResult, LeanProjectSetup, SetupConfig, SetupResult __all__ = [ 'RepoManager', 'ElanManager', 'MathlibCacheManager', 'LeanRepo', + 'CacheCreateResult', 'LeanProjectSetup', 'SetupConfig', 'SetupResult', diff --git a/leanup/repo/cache_server.py b/leanup/repo/cache_server.py new file mode 100644 index 0000000..52f22e8 --- /dev/null +++ b/leanup/repo/cache_server.py @@ -0,0 +1,65 @@ +from __future__ import annotations + +from pathlib import Path + +from fastapi import FastAPI, HTTPException +from fastapi.responses import FileResponse, JSONResponse, PlainTextResponse +import uvicorn + + +def create_cache_app(ltar_root: Path, packages_root: Path) -> FastAPI: + ltar_root = ltar_root.resolve() + packages_root = packages_root.resolve() + archives_root = packages_root / "archives" + + app = FastAPI(title="LeanUp Cache Server") + + @app.get("/healthz") + def healthz() -> PlainTextResponse: + return PlainTextResponse("ok\n") + + @app.get("/packages/mathlib/index.json") + def package_index() -> JSONResponse: + return JSONResponse({"versions": list_package_versions(archives_root)}) + + @app.get("/f/{filename:path}") + def ltar_file(filename: str) -> FileResponse: + file_path = resolve_ltar_path(ltar_root, filename) + return file_response(file_path) + + @app.get("/packages/mathlib/{version}/packages.tar.gz") + def package_archive(version: str) -> FileResponse: + return file_response(archives_root / version / "packages.tar.gz") + + return app + + +def run_cache_server(host: str, port: int, ltar_root: Path, packages_root: Path) -> None: + app = create_cache_app(ltar_root, packages_root) + uvicorn.run(app, host=host, port=port, log_level="info") + + +def list_package_versions(packages_root: Path) -> list[str]: + if not packages_root.exists(): + return [] + + versions: list[str] = [] + for child in sorted(packages_root.iterdir()): + if child.is_dir() and (child / "packages.tar.gz").exists(): + versions.append(child.name) + return versions + + +def resolve_ltar_path(ltar_root: Path, filename: str) -> Path: + parts = [part for part in filename.split("/") if part] + if len(parts) == 1 and parts[0].endswith(".ltar"): + return ltar_root / parts[0] + if len(parts) == 3 and parts[2].endswith(".ltar"): + return ltar_root / "repos" / parts[0] / parts[1] / parts[2] + raise HTTPException(status_code=404, detail="File not found") + + +def file_response(file_path: Path) -> FileResponse: + if not file_path.exists() or not file_path.is_file(): + raise HTTPException(status_code=404, detail="File not found") + return FileResponse(file_path) diff --git a/leanup/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py index 2983092..c328481 100644 --- a/leanup/repo/mathlib_cache.py +++ b/leanup/repo/mathlib_cache.py @@ -1,12 +1,16 @@ from __future__ import annotations from dataclasses import dataclass +import os from pathlib import Path import re import shutil import subprocess import tarfile import tempfile +from urllib.parse import urljoin + +import requests from leanup.const import LEANUP_CACHE_DIR from leanup.utils.custom_logger import setup_logger @@ -37,35 +41,68 @@ def remove_path(path: Path) -> None: @dataclass class CacheEntry: version: str - local_path: Path + packages_path: Path + archive_path: Path @property def local_available(self) -> bool: - return self.local_path.exists() + return self.packages_path.exists() or self.archive_path.exists() class MathlibCacheManager: def __init__(self, cache_root: Path | None = None): - self.cache_root = cache_root or (LEANUP_CACHE_DIR / "setup" / "mathlib") + self.cache_root = cache_root or (LEANUP_CACHE_DIR / "mathlib") + self.packages_root = self.cache_root / "packages" + self.archives_root = self.cache_root / "archives" def get_local_packages_dir(self, version: str) -> Path: - return self.cache_root / normalize_lean_version(version) / "packages" + return self.packages_root / normalize_lean_version(version) / "packages" + + def get_local_archive_path(self, version: str) -> Path: + return self.archives_root / normalize_lean_version(version) / "packages.tar.gz" def list_entries(self) -> list[CacheEntry]: versions = set() - if self.cache_root.exists(): - for child in self.cache_root.iterdir(): + for root in (self.packages_root, self.archives_root): + if not root.exists(): + continue + for child in root.iterdir(): if child.is_dir() and LEAN_VERSION_PATTERN.match(child.name): versions.add(normalize_lean_version(child.name)) return [ CacheEntry( version=version, - local_path=self.get_local_packages_dir(version), + packages_path=self.get_local_packages_dir(version), + archive_path=self.get_local_archive_path(version), ) for version in sorted(versions) ] + def list_remote_entries(self, base_url: str) -> list[CacheEntry]: + index_url = urljoin(base_url.rstrip("/") + "/", "packages/mathlib/index.json") + try: + response = requests.get(index_url, timeout=10) + response.raise_for_status() + payload = response.json() + except Exception: + return [] + + entries: list[CacheEntry] = [] + for version in payload.get("versions", []): + try: + normalized = normalize_lean_version(version) + except ValueError: + continue + entries.append( + CacheEntry( + version=normalized, + packages_path=self.get_local_packages_dir(normalized), + archive_path=self.get_local_archive_path(normalized), + ) + ) + return entries + def ensure_local_cache(self, version: str) -> Path | None: local_path = self.get_local_packages_dir(version) if local_path.exists(): @@ -74,7 +111,7 @@ def ensure_local_cache(self, version: str) -> Path | None: def refresh_local_cache(self, version: str, source_dir: Path, force: bool = True) -> Path: normalized = normalize_lean_version(version) - version_root = self.cache_root / normalized + version_root = self.packages_root / normalized packages_dir = version_root / "packages" if packages_dir.exists() and not force: return packages_dir @@ -120,6 +157,74 @@ def pack_packages_archive(self, packages_dir: Path, output_file: Path, use_pigz: logger.info(f"Packed {source_dir} -> {output_file}") return output_file + def build_archive_url(self, version: str, base_url: str) -> str: + normalized = normalize_lean_version(version) + return urljoin(base_url.rstrip("/") + "/", f"packages/mathlib/{normalized}/packages.tar.gz") + + def download_archive(self, version: str, url: str) -> Path: + output_file = self.get_local_archive_path(version) + output_file.parent.mkdir(parents=True, exist_ok=True) + + with tempfile.NamedTemporaryFile( + dir=output_file.parent, + prefix=f".{output_file.name}.", + suffix=".tmp", + delete=False, + ) as handle: + temp_output = Path(handle.name) + + try: + with requests.get(url, stream=True, timeout=120) as response: + response.raise_for_status() + with temp_output.open("wb") as output_handle: + for chunk in response.iter_content(chunk_size=1024 * 1024): + if chunk: + output_handle.write(chunk) + + remove_path(output_file) + temp_output.replace(output_file) + logger.info(f"Downloaded {url} -> {output_file}") + return output_file + except Exception: + remove_path(temp_output) + raise + + def extract_archive(self, archive_file: Path, target_packages_dir: Path) -> Path: + if not archive_file.exists() or not archive_file.is_file(): + raise ValueError(f"Archive not found: {archive_file}") + + parent_dir = target_packages_dir.parent + parent_dir.mkdir(parents=True, exist_ok=True) + temp_root = Path( + tempfile.mkdtemp(prefix=f".{target_packages_dir.name}.", suffix=".tmp", dir=parent_dir) + ) + + try: + with tarfile.open(archive_file, "r:gz") as tar: + self._safe_extract(tar, temp_root) + + extracted_packages_dir = temp_root / "packages" + if not extracted_packages_dir.exists() or not extracted_packages_dir.is_dir(): + raise ValueError(f"Archive does not contain top-level packages/ directory: {archive_file}") + + final_temp = parent_dir / f".{target_packages_dir.name}.replace-{os.getpid()}" + remove_path(final_temp) + extracted_packages_dir.replace(final_temp) + + remove_path(target_packages_dir) + final_temp.replace(target_packages_dir) + remove_path(temp_root) + + logger.info(f"Extracted {archive_file} -> {target_packages_dir}") + return target_packages_dir + except Exception: + remove_path(temp_root) + raise + + def fetch_packages(self, version: str, base_url: str) -> Path: + archive = self.download_archive(version, self.build_archive_url(version, base_url)) + return self.extract_archive(archive, self.get_local_packages_dir(version)) + def _pack_with_pigz(self, source_dir: Path, output_file: Path) -> None: logger.info(f"Streaming tar archive from {source_dir.parent} into pigz") transform = f"s,^{re.escape(source_dir.name)},packages," @@ -145,3 +250,14 @@ def _pack_with_pigz(self, source_dir: Path, output_file: Path) -> None: tar_returncode = tar_proc.wait() if tar_returncode != 0: raise subprocess.CalledProcessError(tar_returncode, tar_proc.args) + + def _safe_extract(self, tar: tarfile.TarFile, target_dir: Path) -> None: + target_dir = target_dir.resolve() + for member in tar.getmembers(): + member_path = (target_dir / member.name).resolve() + if not str(member_path).startswith(str(target_dir)): + raise ValueError(f"Archive contains unsafe path: {member.name}") + try: + tar.extractall(target_dir, filter="data") + except TypeError: + tar.extractall(target_dir) diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py index 56c426d..eea27a4 100644 --- a/leanup/repo/project_setup.py +++ b/leanup/repo/project_setup.py @@ -79,6 +79,13 @@ class SetupResult: used_cache: bool = False +@dataclass +class CacheCreateResult: + lean_version: str + cache_dir: Path + archive_path: Path + + class LeanProjectSetup: def __init__(self, elan_manager: ElanManager | None = None): self.elan_manager = elan_manager or ElanManager() @@ -139,6 +146,44 @@ def setup(self, config: SetupConfig) -> SetupResult: used_cache=used_cache, ) + def create_mathlib_cache(self, lean_version: str, use_pigz: bool = True) -> CacheCreateResult: + normalized = normalize_lean_version(lean_version) + config = SetupConfig( + target_dir=Path.cwd() / f"MathlibCacheCreate-{normalized}", + lean_version=normalized, + project_name="MathlibCacheCreate", + mathlib=True, + dependency_mode="copy", + ) + + self._ensure_toolchain(config.lean_version) + + with working_directory() as temp_dir: + project_dir = temp_dir / config.project_name + logger.info(f"Creating temporary mathlib cache project in {project_dir}") + self._render_mathlib_template(config, project_dir) + self._write_toolchain(project_dir, config.toolchain) + + project = LeanRepo(project_dir) + logger.info("Running lake update for cache creation") + self._run_lake_update(project) + logger.info("Running lake exe cache get for cache creation") + self._run_lake_cache_get(project) + + logger.info("Refreshing shared packages cache from temporary project") + self._refresh_mathlib_cache(config, project_dir) + + packages_dir = self.cache_manager.get_local_packages_dir(config.lean_version) + archive_path = self.cache_manager.get_local_archive_path(config.lean_version) + logger.info("Packing packages archive from refreshed shared cache") + self.cache_manager.pack_packages_archive(packages_dir, archive_path, use_pigz=use_pigz) + + return CacheCreateResult( + lean_version=config.lean_version, + cache_dir=self.cache_manager.get_local_packages_dir(config.lean_version), + archive_path=self.cache_manager.get_local_archive_path(config.lean_version), + ) + def _ensure_target_available(self, config: SetupConfig) -> None: target = config.target_dir if target.exists() or target.is_symlink(): diff --git a/setup.cfg b/setup.cfg index e00712e..d0cc19e 100644 --- a/setup.cfg +++ b/setup.cfg @@ -25,6 +25,8 @@ install_requires = loguru requests colorama + fastapi + uvicorn [options.packages.find] where = . diff --git a/tests/test_cli.py b/tests/test_cli.py index 25aa50f..01cdc30 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -1,9 +1,4 @@ -import pytest -import tempfile -from pathlib import Path -from unittest.mock import Mock, patch, MagicMock from click.testing import CliRunner -from leanup.const import OS_TYPE from leanup.cli import cli @@ -20,139 +15,12 @@ def test_cli_help(self): assert result.exit_code == 0 assert "LeanUp - Lean project management tool" in result.output - @patch("leanup.cli.elan_ops.ElanManager") - def test_init_command(self, mock_elan_manager): - """Test init command""" - # Mock elan manager - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = False - mock_elan.install_elan.return_value = True - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["init"]) - - if result.exit_code == 0: - "✓ elan installed successfully" in result.output - # mock_elan.install_elan.assert_called_once() - - @patch("leanup.cli.elan_ops.ElanManager") - def test_init_command_already_installed(self, mock_elan_manager): - """Test init command when elan is already installed""" - # Mock elan manager - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["init"]) - - assert result.exit_code == 0 - assert "✓ elan is already installed" in result.output - mock_elan.install_elan.assert_not_called() - - @patch("leanup.cli.elan_ops.ElanManager") - def test_install_command_latest(self, mock_elan_manager): - """Test install command for latest version""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan.proxy_elan_command.return_value = 0 - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["install"]) - - assert result.exit_code == 0 - - @patch("leanup.cli.elan_ops.ElanManager") - def test_install_command_specific_version(self, mock_elan_manager): - """Test install command for specific version""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan.proxy_elan_command.return_value = 0 - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["install", "v4.10.0"]) - - assert result.exit_code == 0 - - @patch("leanup.cli.elan_ops.ElanManager") - def test_install_command_with_force(self, mock_elan_manager): - """Test install command with force flag""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan.proxy_elan_command.return_value = 0 - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["install", "v4.10.0"]) - - assert result.exit_code == 0 - - @patch("leanup.cli.elan_ops.ElanManager") - def test_install_command_elan_not_installed(self, mock_elan_manager): - """Test install command when elan is not installed""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = False - mock_elan.install_elan.return_value = True - mock_elan.proxy_elan_command.return_value = 0 - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["install"]) + def test_cache_help_lists_top_level_commands(self): + result = self.runner.invoke(cli, ["cache", "--help"]) assert result.exit_code == 0 - assert "✓ elan installed successfully" in result.output - # assert 'Installing latest Lean toolchain...' in result.output - # mock_elan.install_elan.assert_called_once() - # mock_elan.proxy_elan_command.assert_called_once_with(['toolchain', 'install', 'stable']) - - @patch("leanup.cli.elan_ops.ElanManager") - def test_status_command(self, mock_elan_manager): - """Test status command""" - # Mock elan manager - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan.get_elan_version.return_value = "4.0.0" - mock_elan.get_installed_toolchains.return_value = [ - "leanprover/lean4:v4.10.0", - "leanprover/lean4:v4.9.0", - ] - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["status"]) - - assert result.exit_code == 0 - assert "=== LeanUp Status ===" in result.output - assert "elan " in result.output - - @patch("leanup.cli.elan_ops.ElanManager") - def test_status_command_elan_not_installed(self, mock_elan_manager): - """Test status command when elan is not installed""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = False - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["status"]) - - assert result.exit_code == 0 - assert "elan: ✗ not installed" in result.output - - @patch("leanup.cli.elan_ops.ElanManager") - def test_elan_proxy_command(self, mock_elan_manager): - """Test elan proxy command""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = True - mock_elan.proxy_elan_command.return_value = 0 - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["elan", "toolchain", "list"]) - - mock_elan.proxy_elan_command.assert_called_once_with(["toolchain", "list"]) - - @patch("leanup.cli.elan_ops.ElanManager") - def test_elan_proxy_command_not_installed(self, mock_elan_manager): - """Test elan proxy command when elan is not installed""" - mock_elan = Mock() - mock_elan.is_elan_installed.return_value = False - mock_elan_manager.return_value = mock_elan - - result = self.runner.invoke(cli, ["elan", "toolchain", "list"]) - - assert result.exit_code == 1 - assert "elan is not installed. Run 'leanup init' first." in result.output + assert "list" in result.output + assert "get" in result.output + assert "pack" in result.output + assert "serve" in result.output + assert "create" in result.output diff --git a/tests/test_mathlib_cache_cli.py b/tests/test_mathlib_cache_cli.py index a855393..a7a5ff7 100644 --- a/tests/test_mathlib_cache_cli.py +++ b/tests/test_mathlib_cache_cli.py @@ -1,36 +1,36 @@ +import os from pathlib import Path +import subprocess +import sys import tarfile +import time from click.testing import CliRunner - from leanup.cli import cli +from leanup.repo.cache_server import create_cache_app, list_package_versions, resolve_ltar_path from leanup.repo.mathlib_cache import MathlibCacheManager +from leanup.repo.project_setup import LeanProjectSetup def test_mathlib_cache_pack_archives_current_repo(tmp_path): runner = CliRunner() - repo_dir = tmp_path / "Demo" - packages_dir = repo_dir / ".lake" / "packages" / "mathlib" + cache_root = tmp_path / "cache" + packages_dir = cache_root / "packages" / "v4.22.0" / "packages" / "mathlib" packages_dir.mkdir(parents=True, exist_ok=True) (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") - output_dir = tmp_path / "cache" result = runner.invoke( cli, [ - "mathlib", "cache", "pack", - "--repo-dir", - str(repo_dir), - "--output-dir", - str(output_dir), - "--lean-version", "v4.22.0", + "--output-dir", + str(cache_root), ], ) - archive = output_dir / "v4.22.0" / "packages.tar.gz" + archive = cache_root / "archives" / "v4.22.0" / "packages.tar.gz" assert result.exit_code == 0 assert archive.exists() with tarfile.open(archive, "r:gz") as tar: @@ -38,34 +38,118 @@ def test_mathlib_cache_pack_archives_current_repo(tmp_path): assert "packages/mathlib/README.md" in names +def test_mathlib_subcommand_pack_defaults_to_mathlib_cache_root(tmp_path): + packages_dir = tmp_path / "custom-cache-root" / "mathlib" / "packages" / "v4.28.0" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") + + custom_cache_dir = tmp_path / "custom-cache-root" + env = os.environ.copy() + env["LEANUP_CACHE_DIR"] = str(custom_cache_dir) + + result = subprocess.run( + [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "pack", + "v4.28.0", + "--no-pigz", + ], + cwd=Path(__file__).resolve().parents[1], + env=env, + text=True, + capture_output=True, + check=False, + ) + + expected_archive = custom_cache_dir / "mathlib" / "archives" / "v4.28.0" / "packages.tar.gz" + assert result.returncode == 0, result.stderr + assert expected_archive.exists() + assert str(expected_archive) in result.stdout + + +def test_mathlib_pack_output_is_listable_via_server_url(tmp_path): + cache_root = tmp_path / "served-mathlib-cache" + packages_dir = cache_root / "packages" / "v4.28.0" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") + + runner = CliRunner() + pack_result = runner.invoke( + cli, + [ + "cache", + "pack", + "v4.28.0", + "--output-dir", + str(cache_root), + "--no-pigz", + ], + ) + assert pack_result.exit_code == 0 + assert (cache_root / "archives" / "v4.28.0" / "packages.tar.gz").exists() + + ltar_root = tmp_path / "isolated-mathlib4-cache" + ltar_root.mkdir(parents=True, exist_ok=True) + command = [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "serve", + "--host", + "127.0.0.1", + "--port", + "18083", + "--ltar-root", + str(ltar_root), + "--packages-root", + str(cache_root), + ] + proc = subprocess.Popen( + command, + cwd=Path(__file__).resolve().parents[1], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + try: + if proc.stdout: + proc.stdout.readline() + proc.stdout.readline() + proc.stdout.readline() + time.sleep(1) + base_url = "http://127.0.0.1:18083" + list_result = runner.invoke(cli, ["cache", "list", "--base-url", base_url]) + finally: + proc.terminate() + proc.wait(timeout=5) + + assert list_result.exit_code == 0 + assert f"v4.28.0 {base_url}/packages/mathlib/v4.28.0/packages.tar.gz" in list_result.output + + def test_mathlib_cache_pack_follows_root_packages_symlink(tmp_path): runner = CliRunner() - source_dir = tmp_path / "shared-packages" / "mathlib" + source_dir = tmp_path / "cache" / "packages" / "v4.29.0" / "packages" / "mathlib" source_dir.mkdir(parents=True, exist_ok=True) (source_dir / "README.md").write_text("cached\n", encoding="utf-8") - repo_dir = tmp_path / "Demo" - lake_dir = repo_dir / ".lake" - lake_dir.mkdir(parents=True, exist_ok=True) - (lake_dir / "packages").symlink_to(source_dir.parent, target_is_directory=True) - output_dir = tmp_path / "cache" result = runner.invoke( cli, [ - "mathlib", "cache", "pack", - "--repo-dir", - str(repo_dir), + "v4.29.0", "--output-dir", str(output_dir), - "--lean-version", - "v4.29.0", ], ) - archive = output_dir / "v4.29.0" / "packages.tar.gz" + archive = output_dir / "archives" / "v4.29.0" / "packages.tar.gz" assert result.exit_code == 0 with tarfile.open(archive, "r:gz") as tar: names = tar.getnames() @@ -74,11 +158,10 @@ def test_mathlib_cache_pack_follows_root_packages_symlink(tmp_path): def test_mathlib_cache_pack_passes_pigz_option(monkeypatch, tmp_path): runner = CliRunner() - repo_dir = tmp_path / "Demo" - packages_dir = repo_dir / ".lake" / "packages" / "mathlib" + output_dir = tmp_path / "cache" + packages_dir = output_dir / "packages" / "v4.22.0" / "packages" / "mathlib" packages_dir.mkdir(parents=True, exist_ok=True) (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") - output_dir = tmp_path / "cache" captured = {} @@ -95,32 +178,27 @@ def fake_pack(self, packages_dir, output_file, use_pigz=False): result = runner.invoke( cli, [ - "mathlib", "cache", "pack", - "--repo-dir", - str(repo_dir), + "v4.22.0", "--output-dir", str(output_dir), - "--lean-version", - "v4.22.0", "--pigz", ], ) assert result.exit_code == 0 - assert captured["packages_dir"] == repo_dir / ".lake" / "packages" - assert captured["output_file"] == output_dir / "v4.22.0" / "packages.tar.gz" + assert captured["packages_dir"] == output_dir / "packages" / "v4.22.0" / "packages" + assert captured["output_file"] == output_dir / "archives" / "v4.22.0" / "packages.tar.gz" assert captured["use_pigz"] is True def test_mathlib_cache_pack_uses_pigz_by_default(monkeypatch, tmp_path): runner = CliRunner() - repo_dir = tmp_path / "Demo" - packages_dir = repo_dir / ".lake" / "packages" / "mathlib" + output_dir = tmp_path / "cache" + packages_dir = output_dir / "packages" / "v4.22.0" / "packages" / "mathlib" packages_dir.mkdir(parents=True, exist_ok=True) (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") - output_dir = tmp_path / "cache" captured = {} @@ -135,17 +213,315 @@ def fake_pack(self, packages_dir, output_file, use_pigz=False): result = runner.invoke( cli, [ - "mathlib", "cache", "pack", - "--repo-dir", - str(repo_dir), + "v4.22.0", "--output-dir", str(output_dir), - "--lean-version", - "v4.22.0", ], ) assert result.exit_code == 0 assert captured["use_pigz"] is True + + +def test_mathlib_cache_list_prints_package_urls(monkeypatch, tmp_path): + runner = CliRunner() + monkeypatch.setattr( + MathlibCacheManager, + "list_remote_entries", + lambda self, base_url: [ + type("Entry", (), {"version": "v4.22.0"})(), + type("Entry", (), {"version": "v4.27.0"})(), + ], + ) + + result = runner.invoke( + cli, + [ + "cache", + "list", + "--base-url", + "http://127.0.0.1:8000/", + ], + ) + + assert result.exit_code == 0 + assert "v4.22.0 http://127.0.0.1:8000/packages/mathlib/v4.22.0/packages.tar.gz" in result.output + assert "v4.27.0 http://127.0.0.1:8000/packages/mathlib/v4.27.0/packages.tar.gz" in result.output + + +def test_mathlib_cache_list_reads_remote_index(tmp_path): + runner = CliRunner() + packages_root = tmp_path / "packages-cache" + (packages_root / "archives" / "v4.22.0").mkdir(parents=True, exist_ok=True) + (packages_root / "archives" / "v4.22.0" / "packages.tar.gz").write_bytes(b"ok") + (packages_root / "archives" / "v4.27.0").mkdir(parents=True, exist_ok=True) + (packages_root / "archives" / "v4.27.0" / "packages.tar.gz").write_bytes(b"ok") + + ltar_root = tmp_path / "isolated-mathlib4-cache" + ltar_root.mkdir(parents=True, exist_ok=True) + + command = [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "serve", + "--host", + "127.0.0.1", + "--port", + "18081", + "--ltar-root", + str(ltar_root), + "--packages-root", + str(packages_root), + ] + proc = subprocess.Popen( + command, + cwd=Path(__file__).resolve().parents[1], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + try: + if proc.stdout: + proc.stdout.readline() + proc.stdout.readline() + proc.stdout.readline() + time.sleep(1) + base_url = "http://127.0.0.1:18081" + result = runner.invoke( + cli, + ["cache", "list", "--base-url", base_url], + ) + finally: + proc.terminate() + proc.wait(timeout=5) + + assert result.exit_code == 0 + assert f"v4.22.0 {base_url}/packages/mathlib/v4.22.0/packages.tar.gz" in result.output + assert f"v4.27.0 {base_url}/packages/mathlib/v4.27.0/packages.tar.gz" in result.output + + +def test_mathlib_cache_list_with_base_url_does_not_fallback_to_local(monkeypatch, tmp_path): + runner = CliRunner() + cache_root = tmp_path / "cache" + (cache_root / "v4.22.0" / "packages").mkdir(parents=True) + + original_init = MathlibCacheManager.__init__ + + def fake_cache_init(self, cache_root_arg=None): + original_init(self, cache_root=cache_root) + + monkeypatch.setattr(MathlibCacheManager, "__init__", fake_cache_init) + monkeypatch.setattr(MathlibCacheManager, "list_remote_entries", lambda self, base_url: []) + + result = runner.invoke( + cli, + ["cache", "list", "--base-url", "http://127.0.0.1:8000"], + ) + + assert result.exit_code == 0 + assert result.output.strip() == "No mathlib caches found." + + +def test_cache_pack_reports_missing_project_packages(tmp_path): + runner = CliRunner() + + result = runner.invoke(cli, ["cache", "pack", "v4.28.0", "--output-dir", str(tmp_path)]) + + assert result.exit_code == 1 + assert "Run 'leanup cache create v4.28.0' or 'leanup cache get v4.28.0 --base-url ...' first." in result.output + + +def test_cache_get_downloads_and_extracts_packages_archive(tmp_path): + runner = CliRunner() + packages_root = tmp_path / "packages-cache" + archive_dir = packages_root / "archives" / "v4.22.0" + archive_dir.mkdir(parents=True, exist_ok=True) + + source_packages = tmp_path / "source-packages" / "mathlib" + source_packages.mkdir(parents=True, exist_ok=True) + (source_packages / "README.md").write_text("cached\n", encoding="utf-8") + + archive = archive_dir / "packages.tar.gz" + MathlibCacheManager().pack_packages_archive(source_packages.parent, archive) + + stale_packages = tmp_path / "local-cache" / "packages" / "v4.22.0" / "packages" + stale_packages.mkdir(parents=True, exist_ok=True) + (stale_packages / "STALE.txt").write_text("stale\n", encoding="utf-8") + + ltar_root = tmp_path / "isolated-mathlib4-cache" + ltar_root.mkdir(parents=True, exist_ok=True) + command = [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "serve", + "--host", + "127.0.0.1", + "--port", + "18082", + "--ltar-root", + str(ltar_root), + "--packages-root", + str(packages_root), + ] + proc = subprocess.Popen( + command, + cwd=Path(__file__).resolve().parents[1], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + try: + if proc.stdout: + proc.stdout.readline() + proc.stdout.readline() + proc.stdout.readline() + time.sleep(1) + result = runner.invoke( + cli, + [ + "cache", + "get", + "v4.22.0", + "--base-url", + "http://127.0.0.1:18082", + "--cache-dir", + str(tmp_path / "local-cache"), + ], + ) + finally: + proc.terminate() + proc.wait(timeout=5) + + installed_readme = tmp_path / "local-cache" / "packages" / "v4.22.0" / "packages" / "mathlib" / "README.md" + assert result.exit_code == 0 + assert installed_readme.read_text(encoding="utf-8") == "cached\n" + assert not (tmp_path / "local-cache" / "packages" / "v4.22.0" / "packages" / "STALE.txt").exists() + + +def test_cache_server_resolves_ltar_and_packages_routes(tmp_path): + packages_root = tmp_path / "packages-root" + ltar_root = tmp_path / "isolated-mathlib4-cache" + (packages_root / "v4.22.0").mkdir(parents=True, exist_ok=True) + (ltar_root / "repos" / "owner" / "repo").mkdir(parents=True, exist_ok=True) + + assert resolve_ltar_path(ltar_root.resolve(), "abc.ltar") == ltar_root.resolve() / "abc.ltar" + assert resolve_ltar_path(ltar_root.resolve(), "owner/repo/abc.ltar") == ltar_root.resolve() / "repos" / "owner" / "repo" / "abc.ltar" + assert list_package_versions(packages_root.resolve()) == [] + + +def test_cache_pack_honors_cleanup_cache_dir_env_in_subprocess(tmp_path): + packages_dir = tmp_path / "custom-cache-root" / "mathlib" / "packages" / "v4.22.0" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") + + custom_cache_dir = tmp_path / "custom-cache-root" + env = os.environ.copy() + env["LEANUP_CACHE_DIR"] = str(custom_cache_dir) + + command = [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "pack", + "v4.22.0", + "--no-pigz", + ] + result = subprocess.run( + command, + cwd=Path(__file__).resolve().parents[1], + env=env, + text=True, + capture_output=True, + check=False, + ) + + expected_archive = custom_cache_dir / "mathlib" / "archives" / "v4.22.0" / "packages.tar.gz" + assert result.returncode == 0, result.stderr + assert expected_archive.exists() + assert str(expected_archive) in result.stdout + + +def test_cache_serve_honors_explicit_roots_in_subprocess(tmp_path): + ltar_root = tmp_path / "isolated-mathlib4-cache" + packages_root = tmp_path / "isolated-leanup-cache" + ltar_root.mkdir(parents=True, exist_ok=True) + packages_root.mkdir(parents=True, exist_ok=True) + + command = [ + sys.executable, + "-c", + "from leanup.cli import cli; cli()", + "cache", + "serve", + "--host", + "127.0.0.1", + "--port", + "18080", + "--ltar-root", + str(ltar_root), + "--packages-root", + str(packages_root), + ] + proc = subprocess.Popen( + command, + cwd=Path(__file__).resolve().parents[1], + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + try: + stdout_line_1 = proc.stdout.readline().strip() if proc.stdout else "" + stdout_line_2 = proc.stdout.readline().strip() if proc.stdout else "" + stdout_line_3 = proc.stdout.readline().strip() if proc.stdout else "" + time.sleep(1) + finally: + proc.terminate() + proc.wait(timeout=5) + + assert "Serving cache on http://127.0.0.1:18080" in stdout_line_1 + assert str(ltar_root) in stdout_line_2 + assert str(packages_root) in stdout_line_3 + + +def test_cache_create_refreshes_shared_cache_and_archive(monkeypatch, tmp_path): + runner = CliRunner() + custom_cache_root = tmp_path / "leanup-cache" + + def fake_ensure_toolchain(self, version): + return None + + def fake_run_lake_update(self, repo): + packages_dir = repo.cwd / ".lake" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") + + def fake_run_lake_cache_get(self, repo): + return None + + monkeypatch.setattr(LeanProjectSetup, "_ensure_toolchain", fake_ensure_toolchain) + monkeypatch.setattr(LeanProjectSetup, "_run_lake_update", fake_run_lake_update) + monkeypatch.setattr(LeanProjectSetup, "_run_lake_cache_get", fake_run_lake_cache_get) + + original_init = MathlibCacheManager.__init__ + + def fake_cache_init(self, cache_root=None): + original_init(self, cache_root=custom_cache_root) + + monkeypatch.setattr(MathlibCacheManager, "__init__", fake_cache_init) + + result = runner.invoke(cli, ["cache", "create", "v4.22.0", "--no-pigz"]) + + expected_packages = custom_cache_root / "packages" / "v4.22.0" / "packages" + expected_archive = custom_cache_root / "archives" / "v4.22.0" / "packages.tar.gz" + assert result.exit_code == 0 + assert expected_packages.exists() + assert expected_archive.exists() + assert str(expected_packages) in result.output + assert str(expected_archive) in result.output diff --git a/tests/test_setup.py b/tests/test_setup.py index 6e9d860..32d0156 100644 --- a/tests/test_setup.py +++ b/tests/test_setup.py @@ -328,7 +328,7 @@ def fake_lake(self, args): LeanRepo.lake_env_lean = fake_lake_env_lean LeanRepo.lake = fake_lake - cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.27.0" / "packages" / "mathlib" + cached_packages = cache_module.LEANUP_CACHE_DIR / "mathlib" / "packages" / "v4.27.0" / "packages" / "mathlib" _init_fake_package_repo(cached_packages) manager = LeanProjectSetup(elan_manager=FakeElanManager()) @@ -393,7 +393,7 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): 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" + cached_packages = cache_module.LEANUP_CACHE_DIR / "mathlib" / "packages" / "v4.22.0" / "packages" / "mathlib" _init_fake_package_repo(cached_packages) manager = LeanProjectSetup(elan_manager=FakeElanManager()) @@ -449,7 +449,7 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): original_lake_env_lean = LeanRepo.lake_env_lean try: - cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" / "mathlib" + cached_packages = cache_module.LEANUP_CACHE_DIR / "mathlib" / "packages" / "v4.22.0" / "packages" / "mathlib" _init_fake_package_repo(cached_packages) LeanRepo.lake_update = fake_lake_update @@ -538,9 +538,9 @@ def fake_lake(self, args): assert '"inputRev": "v4.22.0"' in manifest_text assert '"name": "BundledDemo"' in manifest_text assert '"rev": "' in manifest_text - assert (cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages").exists() + assert (cache_module.LEANUP_CACHE_DIR / "mathlib" / "packages" / "v4.22.0" / "packages").exists() assert ( - cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" / "mathlib" / "README.md" + cache_module.LEANUP_CACHE_DIR / "mathlib" / "packages" / "v4.22.0" / "packages" / "mathlib" / "README.md" ).read_text(encoding="utf-8").strip() == "cached from cache get" finally: cache_module.LEANUP_CACHE_DIR = original_cache_dir