From b355f8f3784882c4a44d2658a6ceda6e45efbf73 Mon Sep 17 00:00:00 2001 From: rexwzh <1073853456@qq.com> Date: Tue, 7 Apr 2026 06:40:07 +0800 Subject: [PATCH 1/8] refactor: align leanup cli and docs --- AGENTS.md | 46 ++++ CONTRIBUTING.md | 104 ++++---- DEVELOP.md | 34 +++ README-en.md | 270 --------------------- README.md | 27 ++- docs/en/getting-started/quickstart.md | 181 -------------- docs/en/index.md | 67 ------ docs/getting-started/quickstart.md | 106 ++++---- docs/getting-started/quickstart.zh.md | 181 -------------- docs/index.md | 22 ++ docs/zh/getting-started/quickstart.md | 181 -------------- docs/zh/index.md | 67 ------ leanup/cli/__init__.py | 70 ++---- leanup/cli/elan_ops.py | 55 +++++ leanup/cli/interaction.py | 69 ++++++ leanup/cli/repo.py | 165 +++++++++---- leanup/repo/elan.py | 136 ++++++----- leanup/repo/manager.py | 334 ++++++++++++++------------ leanup/utils/config.py | 42 ++-- mkdocs.yml | 41 +--- tests/test_cli.py | 132 +++++----- tests/test_repo_cli.py | 82 +++++++ 22 files changed, 909 insertions(+), 1503 deletions(-) create mode 100644 AGENTS.md create mode 100644 DEVELOP.md delete mode 100644 README-en.md delete mode 100644 docs/en/getting-started/quickstart.md delete mode 100644 docs/en/index.md delete mode 100644 docs/getting-started/quickstart.zh.md create mode 100644 docs/index.md delete mode 100644 docs/zh/getting-started/quickstart.md delete mode 100644 docs/zh/index.md create mode 100644 leanup/cli/elan_ops.py create mode 100644 leanup/cli/interaction.py create mode 100644 tests/test_repo_cli.py diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..9287754 --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,46 @@ +# LeanUp Agent Notes + +## 项目信息 + +- 主语言：Python +- CLI 入口：`leanup` +- 代码路径：`leanup/` +- 文档：`README.md`、`docs/` + +## 目录边界 + +```text +leanup/ +├── cli/ # CLI 入口与编排 +├── repo/ # Lean / elan / repo 相关核心逻辑 +├── utils/ # 通用工具与配置能力 +└── const.py # 常量定义 +``` + +## 开发规范 + +### CLI + +- 命令优先，交互兜底。 +- 缺必要参数时自动进入 interactive；`-i` 强制交互，`-I` 禁止交互。 +- interactive 展示的默认值必须和最终实际执行一致。 +- 新交互统一收敛到共享 interaction 层，不在命令文件里重复写 `click.prompt` / `click.confirm` 流程。 +- CLI 文件只做接入、参数编排和输出组织，不承载主要业务实现。 + +### 代码结构 + +- `cli/` 负责入口编排。 +- `repo/` 负责 Lean / elan / 仓库相关核心逻辑。 +- `utils/` 只放真正通用的工具能力，不把业务逻辑塞进去。 +- 相同行为优先复用，不重复实现。 + +### 文档 + +- 当前以中文主文档为准，不继续维护英文平行文档。 +- 功能变更同步更新 `README.md` 和 `docs/`。 + +### 测试 + +- 先保证最小可运行测试覆盖。 +- 与 CLI 行为强相关的改动，测试要同步更新。 +- 新测试优先保持意图清晰、边界明确，不继续扩散历史风格。 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 05c4e5d..dc63fd4 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,20 +1,18 @@ -# 贡献指南 / Contributing Guide +# 贡献指南 -感谢您对 LeanUp 项目的关注！我们欢迎各种形式的贡献。 +感谢您对 LeanUp 项目的关注！欢迎各种形式的贡献。 -Thank you for your interest in contributing to LeanUp! We welcome all kinds of contributions. +## 🚀 快速开始 -## 🚀 快速开始 / Quick Start +### 环境准备 -### 环境准备 / Environment Setup - -1. Fork 并克隆仓库 / Fork and clone the repository: +1. Fork 并克隆仓库： ```bash git clone https://github.com/yourusername/LeanUp.git cd LeanUp ``` -2. 创建虚拟环境 / Create virtual environment: +2. 创建虚拟环境： ```bash python -m venv venv source venv/bin/activate # Linux/macOS @@ -22,101 +20,99 @@ source venv/bin/activate # Linux/macOS venv\Scripts\activate # Windows ``` -3. 安装依赖 / Install dependencies: +3. 安装依赖： ```bash pip install -e . pip install -r requirements_dev.txt ``` -## 🧪 测试 / Testing +## 🧪 测试 -运行测试确保一切正常 / Run tests to ensure everything works: +运行测试确保一切正常： ```bash -# 运行所有测试 / Run all tests +# 运行所有测试 pytest tests/ -v -# 运行测试并生成覆盖率报告 / Run tests with coverage +# 运行测试并生成覆盖率报告 coverage run -m pytest tests/ coverage report -m -# 代码风格检查 / Code style check +# 代码风格检查 ruff check . -# 类型检查 / Type checking +# 类型检查 mypy . ``` -## 📝 代码规范 / Code Standards +## 📝 代码规范 -- 使用 Python 3.9+ / Use Python 3.9+ -- 遵循 PEP 8 代码风格 / Follow PEP 8 style guide -- 添加适当的类型注解 / Add appropriate type hints -- 为新功能编写测试 / Write tests for new features -- 保持代码覆盖率 > 85% / Maintain code coverage > 85% +- 使用 Python 3.9+ +- 遵循 PEP 8 代码风格 +- 添加适当的类型注解 +- 为新功能编写测试 +- 保持代码覆盖率 > 85% +- 具体开发约束以 `AGENTS.md` 和 `DEVELOP.md` 为准 -## 🔄 提交流程 / Submission Process +## 🔄 提交流程 -1. 创建功能分支 / Create feature branch: +1. 创建功能分支： ```bash git checkout -b feature/your-feature-name ``` -2. 进行更改并提交 / Make changes and commit: +2. 进行更改并提交： ```bash git add . git commit -m "描述你的更改 / Describe your changes" ``` -3. 推送到你的 fork / Push to your fork: +3. 推送到你的 fork： ```bash git push origin feature/your-feature-name ``` -4. 创建 Pull Request / Create Pull Request +4. 创建 Pull Request -## 📋 提交信息格式 / Commit Message Format +## 📋 提交信息格式 ``` 类型(scope): 简短描述 详细描述（可选） -类型 / Type: -- feat: 新功能 / new feature -- fix: 修复 bug / bug fix -- docs: 文档更新 / documentation update -- style: 代码格式化 / code formatting -- refactor: 代码重构 / code refactoring -- test: 测试相关 / test related -- chore: 构建/工具相关 / build/tooling related +类型： +- feat: 新功能 +- fix: 修复 bug +- docs: 文档更新 +- style: 代码格式化 +- refactor: 代码重构 +- test: 测试相关 +- chore: 构建/工具相关 ``` -## 🐛 报告问题 / Reporting Issues +## 🐛 报告问题 报告 bug 或提出功能请求时，请提供： -When reporting bugs or requesting features, please provide: -- 操作系统和版本 / Operating system and version -- Python 版本 / Python version -- LeanUp 版本 / LeanUp version -- 重现步骤 / Steps to reproduce -- 期望行为 / Expected behavior -- 实际行为 / Actual behavior +- 操作系统和版本 +- Python 版本 +- LeanUp 版本 +- 重现步骤 +- 期望行为 +- 实际行为 -## 💡 功能请求 / Feature Requests +## 💡 功能请求 -我们欢迎新功能的建议！请确保： -We welcome suggestions for new features! Please ensure: +欢迎新功能建议，请尽量确保： -- 功能与项目目标一致 / Feature aligns with project goals -- 提供清晰的用例 / Provide clear use cases -- 考虑向后兼容性 / Consider backward compatibility +- 功能与项目目标一致 +- 提供清晰的用例 +- 考虑向后兼容性 -## 📞 联系我们 / Contact Us +## 📞 联系方式 -- 通过 GitHub Issues 讨论 / Discuss via GitHub Issues -- 邮箱 / Email: leanprover@outlook.com +- 通过 GitHub Issues 讨论 +- 邮箱：leanprover@outlook.com -感谢您的贡献！🎉 -Thank you for your contributions! 🎉 +感谢您的贡献！ diff --git a/DEVELOP.md b/DEVELOP.md new file mode 100644 index 0000000..a45ceb5 --- /dev/null +++ b/DEVELOP.md @@ -0,0 +1,34 @@ +# LeanUp 开发简版指南 + +## 目标 + +LeanUp 当前对齐 ChatTool 的开发方向： + +- CLI 风格统一 +- 入口和逻辑分层 +- 文档以中文主版本为准 +- 测试随行为变化同步更新 + +## CLI 规范 + +- 默认遵循：命令优先，交互兜底。 +- 缺必要参数时进入 interactive。 +- `-i` 强制 interactive。 +- `-I` 禁止 interactive，参数不足时直接报错。 +- prompt 默认值必须与最终执行值一致。 + +## 代码规范 + +- `leanup/cli/` 只保留命令入口和编排。 +- 具体逻辑下沉到 `repo/` 或 `utils/`。 +- 避免 CLI 文件不断膨胀成“命令 + 业务 + 交互 + 配置解析”四合一。 + +## 文档规范 + +- 主文档使用中文。 +- 清理重复文档和英文平行版本。 + +## 测试规范 + +- 改行为就改测试。 +- 优先修正现有测试到当前设计，不为旧接口加兼容层。 diff --git a/README-en.md b/README-en.md deleted file mode 100644 index 0f1abdd..0000000 --- a/README-en.md +++ /dev/null @@ -1,270 +0,0 @@ -# LeanUp - -
- - PyPI version - - - Tests - - - Coverage - -
- -
- -**A Python tool for managing Lean mathematical proof language environments** - -[English](README-en.md) | [简体中文](README.md) - -
- -## 🎯 Features - -- **📦 Repository Management**: Install and manage Lean repositories with interactive configuration -- **🌍 Cross-platform Support**: Works on Linux, macOS, and Windows -- **📦 Easy Installation**: Quick setup via `pip install leanup` -- **🔄 Command Proxy**: Transparent proxy for all elan commands with seamless experience - -## 🚀 Quick Start - -### Installation - -```bash -# Install from PyPI -pip install leanup - -# Or clone the repository and install -git clone https://github.com/Lean-zh/LeanUp.git -cd LeanUp -pip install -e . -``` - -### Basic Usage - -```bash -# View help -leanup --help - -# Install elan and initialize configuration -leanup init - -# Install latest stable version -leanup install - -# View status -leanup status - -# Proxy execute elan commands -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable -``` - -## 📖 Detailed Usage Guide - -### Managing Lean Toolchains - -After installing elan, you can use `leanup elan` commands to manage Lean toolchains: - -```bash -# List all available toolchains -leanup elan toolchain list - -# Install stable toolchain -leanup elan toolchain install stable - -# Install nightly build -leanup elan toolchain install leanprover/lean4:nightly - -# Set default toolchain -leanup elan default stable - -# Update all toolchains -leanup elan update - -# Show current active toolchain -leanup elan show -``` - -### Repository Management - -```bash -# Install Mathlib -leanup repo install leanprover-community/mathlib4 - -# Install specific branch or tag -leanup repo install leanprover-community/mathlib4 -b v4.14.0 - -# Install to custom directory -leanup repo install Lean-zh/leanup -d /path/to/custom/dir - -# Control build options -leanup repo install leanprover-community/mathlib4 --lake-build - -# Interactive mode -leanup repo install leanprover-community/mathlib4 -i - -# Specify packages to build -leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" - -# List installed repositories -leanup repo list - -# Search repositories in specified directory -leanup repo list --search-dir /path/to/repos - -# Filter repositories by name -leanup repo list -n mathlib -``` - -### Interactive Installation - -When using `--interactive` flag with `leanup repo install`, you can configure: - -- Repository name (required) -- Base URL for repository sources -- Branch or tag -- Destination directory for storing repositories -- Custom destination name -- Whether to run `lake update` after cloning -- Whether to run `lake build` after cloning -- Specific build packages to compile -- Whether to override existing directories - -### Programming Interface - -#### Using InstallConfig - -```python -from leanup.repo.manager import InstallConfig - -# Create installation configuration -config = InstallConfig( - suffix="leanprover-community/mathlib4", - source="https://github.com", - branch="main", - dest_dir=Path("/path/to/repos"), - dest_name="mathlib4_main", - lake_update=True, - lake_build=True, - build_packages=["REPL", "REPL.Main"], - override=False -) - -# Execute installation -config.install() -``` - -#### Using RepoManager - -```python -from leanup.repo.manager import RepoManager - -# Create repository manager -repo = RepoManager("/path/to/directory") - -# Clone repository -repo.clone_from("https://github.com/owner/repo.git", branch="main") - -# File operations -repo.write_file("test.txt", "Hello world") -content = repo.read_file("test.txt") -repo.edit_file("test.txt", "world", "universe") - -# List files and directories -files = repo.list_files("*.lean") -dirs = repo.list_dirs() -``` - -#### Using LeanRepo - -```python -from leanup.repo.manager import LeanRepo - -# Create Lean repository manager -lean_repo = LeanRepo("/path/to/lean/project") - -# Get project information -info = lean_repo.get_project_info() -print(f"Lean version: {info['lean_version']}") -print(f"Has lakefile: {info['has_lakefile_toml']}") - -# Lake operations -stdout, stderr, returncode = lean_repo.lake_init("my_project", "std") -stdout, stderr, returncode = lean_repo.lake_update() -stdout, stderr, returncode = lean_repo.lake_build() -stdout, stderr, returncode = lean_repo.lake_env_lean("Main.lean") -``` - -## 🛠️ Development - -### Environment Setup - -```bash -# Clone repository -git clone https://github.com/Lean-zh/LeanUp.git -cd LeanUp - -# Install development dependencies -pip install -e ".[dev]" - -# Install project (editable mode) -pip install -e . -``` - -### Running Tests - -```bash -# Run all tests -pytest tests/ -v - -# Run tests with coverage report -coverage run -m pytest tests/ -coverage report -m -``` - -## ⚙️ Configuration - -LeanUp uses a configuration file located at `~/.leanup/config.toml`. You can customize: - -- Default repository source -- Cache directory for repositories -- Auto-installation settings for elan -- Repository prefixes and base URLs - -## 🌍 Cross-platform Support - -LeanUp is tested on the following platforms: - -- **Linux**: Ubuntu 20.04+, CentOS 7+, Debian 10+ -- **macOS**: macOS 10.15+ (Intel and Apple Silicon) -- **Windows**: Windows 10+ - -## 📊 Project Status - -| Feature | Status | Description | -|---------|--------|-------------| -| elan Installation | ✅ | Supports automatic platform and version detection | -| Command Proxy | ✅ | Transparent forwarding of all elan commands | -| Repository Management | ✅ | Install and manage Lean repositories | -| Interactive Configuration | ✅ | User-friendly setup process | -| Cross-platform Support | ✅ | Linux/macOS/Windows | -| Unit Tests | ✅ | Coverage > 85% | -| CI/CD | ✅ | GitHub Actions multi-platform testing | - -## 🤝 Contributing - -Contributions are welcome! Please see the [Contributing Guide](CONTRIBUTING.md) for details. - -## 📝 License - -This project is licensed under the MIT License. See the [LICENSE](LICENSE) file for details. - -## 🔗 Related Links - -- [Lean Official Website](https://leanprover.github.io/) -- [Lean Community Documentation](https://leanprover-community.github.io/) -- [elan Toolchain Manager](https://github.com/leanprover/elan) \ No newline at end of file diff --git a/README.md b/README.md index 6efe600..cc6a3d7 100644 --- a/README.md +++ b/README.md @@ -16,13 +16,11 @@ **一个用于管理 Lean 数学证明语言环境的 Python 工具** -[English](README-en.md) | [简体中文](README.md) - ## 🎯 功能特性 -- **📦 仓库管理**: 安装和管理 Lean 仓库，支持交互式配置 +- **📦 仓库管理**: 安装和管理 Lean 仓库，支持命令优先、交互兜底的配置流程 - **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows - **📦 简单易用**: 通过 `pip install leanup` 快速安装 - **🔄 命令代理**: 透明代理所有 elan 命令，无缝体验 @@ -104,9 +102,12 @@ leanup repo install Lean-zh/leanup -d /path/to/custom/dir # 控制构建选项 leanup repo install leanprover-community/mathlib4 --lake-build -# 交互式 +# 交互式补参 leanup repo install leanprover-community/mathlib4 -i +# 禁止交互，参数不足时直接报错 +leanup repo install -I leanprover-community/mathlib4 + # 指定要构建的包 leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" @@ -122,7 +123,7 @@ leanup repo list -n mathlib ### 交互式安装 -使用 `leanup repo install` 的 `--interactive` 标志时，您可以配置： +使用 `leanup repo install -i` 时，您可以配置： - 仓库名称（必需） - 仓库源的基础 URL @@ -134,6 +135,13 @@ leanup repo list -n mathlib - 要编译的特定构建包 - 是否覆盖现有目录 +默认规则： + +- 命令优先，交互兜底 +- 缺必要参数时自动进入交互 +- `-i` 强制交互 +- `-I` 禁止交互，参数不足时直接报错 + ### 编程接口 #### 使用 InstallConfig @@ -201,6 +209,11 @@ stdout, stderr, returncode = lean_repo.lake_env_lean("Main.lean") ## 🛠️ 开发 +仓库级开发规范见： + +- `AGENTS.md` +- `DEVELOP.md` + ### 环境设置 ```bash @@ -228,7 +241,7 @@ coverage report -m ## ⚙️ 配置 -LeanUp 使用位于 `~/.leanup/config.toml` 的配置文件。您可以自定义： +LeanUp 使用位于 `~/.leanup/config.yaml` 的配置文件。您可以自定义： - 默认仓库源 - 仓库缓存目录 @@ -267,4 +280,4 @@ LeanUp 在以下平台上经过测试： - [Lean 官方网站](https://leanprover.github.io/) - [Lean 社区文档](https://leanprover-community.github.io/) -- [elan 工具链管理器](https://github.com/leanprover/elan) \ No newline at end of file +- [elan 工具链管理器](https://github.com/leanprover/elan) diff --git a/docs/en/getting-started/quickstart.md b/docs/en/getting-started/quickstart.md deleted file mode 100644 index 2eec021..0000000 --- a/docs/en/getting-started/quickstart.md +++ /dev/null @@ -1,181 +0,0 @@ -# Quick Start - -## Installation - -```bash -# Install from PyPI -pip install leanup - -# Or clone the repository and install -git clone https://github.com/Lean-zh/LeanUp.git -cd LeanUp -pip install -e . -``` - -## Basic Usage - -### Initialize elan - -```bash -# View help -leanup --help - -# Install elan -leanup init - -# View current status -leanup status -``` - -### Install Lean Toolchain - -```bash -# Install latest stable Lean toolchain -leanup install - -# Install specific Lean toolchain version -leanup install v4.14.0 -``` - -### Manage Toolchains - -```bash -# Proxy execute elan commands -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable -``` - -### Repository Management - -```bash -# Install Mathlib -leanup repo install leanprover-community/mathlib4 - -# Install specific branch or tag -leanup repo install leanprover-community/mathlib4 -b v4.14.0 - -# Install to custom directory -leanup repo install Lean-zh/leanup -d /path/to/custom/dir - -# Control build options -leanup repo install leanprover-community/mathlib4 --lake-build - -# Interactive mode -leanup repo install leanprover-community/mathlib4 -i - -# Specify packages to build -leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" - -# List installed repositories -leanup repo list - -# Search repositories in specified directory -leanup repo list --search-dir /path/to/repos - -# Filter repositories by name -leanup repo list -n mathlib -``` - -## Using InstallConfig - -The `InstallConfig` class provides a programmatic way to configure repository installations: - -```python -from pathlib import Path -from leanup.repo.manager import InstallConfig - -# Create installation configuration -config = InstallConfig( - suffix="leanprover-community/mathlib4", - source="https://github.com", - branch="main", - dest_dir=Path("/path/to/repos"), - dest_name="mathlib4_main", - lake_update=True, - lake_build=True, - build_packages=["REPL", "REPL.Main"], - override=False -) - -# Check if configuration is valid -if config.is_valid: - print(f"Will install to: {config.dest_path}") - -# Execute installation -config.install() - -# Update configuration -new_config = config.update(branch="v4.3.0", override=True) -``` - -## Using the RepoManager - -The `RepoManager` class provides functionality for managing directories and git repositories: - -```python -from leanup.repo.manager import RepoManager - -# Create a repo manager -repo = RepoManager("/path/to/your/directory") - -# Check if it's a git repository -if repo.is_gitrepo: - print("This is a git repository") - status = repo.git_status() - print(f"Current branch: {status['branch']}") - print(f"Is dirty: {status['is_dirty']}") - -# Clone a repository -success = repo.clone_from( - "https://github.com/owner/repo.git", - branch="main", - depth=1 -) - -# File operations -repo.write_file("test.txt", "Hello world") -content = repo.read_file("test.txt") -repo.edit_file("test.txt", "world", "universe", use_regex=False) - -# List files and directories -files = repo.list_files("*.lean") -dirs = repo.list_dirs() - -# Execute commands -stdout, stderr, returncode = repo.execute_command(["ls", "-la"]) -``` - -## Using LeanRepo for Lean Projects - -```python -from leanup.repo.manager import LeanRepo - -# Create a Lean repo manager -lean_repo = LeanRepo("/path/to/lean/project") - -# Get project information -info = lean_repo.get_project_info() -print(f"Lean version: {info['lean_version']}") -print(f"Has lakefile.toml: {info['has_lakefile_toml']}") -print(f"Has lakefile.lean: {info['has_lakefile_lean']}") -print(f"Has lake-manifest.json: {info['has_lake_manifest']}") -print(f"Build directory exists: {info['build_dir_exists']}") - -# Lake operations -lean_repo.lake_init("my_project", "std", "lean") -lean_repo.lake_update() -lean_repo.lake_build("MyTarget") -lean_repo.lake_env_lean("Main.lean", json=True) -lean_repo.lake_clean() -lean_repo.lake_test() - -# Install using configuration -config = InstallConfig( - suffix="leanprover-community/mathlib4", - lake_update=True, - lake_build=False -) -lean_repo.install(config) -``` \ No newline at end of file diff --git a/docs/en/index.md b/docs/en/index.md deleted file mode 100644 index 247588e..0000000 --- a/docs/en/index.md +++ /dev/null @@ -1,67 +0,0 @@ -# LeanUp - -A Python package for managing Lean mathematical proof language environments. - -## Features - -- **🔧 elan Management**: Install and manage the Lean toolchain manager elan with a single command -- **📦 Repository Management**: Install and manage Lean repositories with advanced configuration options -- **🌍 Cross-platform Support**: Works on Linux, macOS, and Windows -- **📦 Easy Installation**: Quick setup via `pip install leanup` - -## Quick Start - -Check the [Quick Start](getting-started/quickstart.md) guide to begin using LeanUp. - -## Command Line Interface - -LeanUp provides a comprehensive CLI with the following commands: - -### Main Commands - -- `leanup init` - Initialize elan installation -- `leanup install [version]` - Install Lean toolchain version via elan -- `leanup status` - Show current status and installed toolchains -- `leanup elan ` - Proxy elan commands - -### Repository Management - -- `leanup repo install ` - Install Lean repositories with flexible configuration -- `leanup repo list` - List installed repositories with filtering options - -#### Repository Install Options - -- `--source` - Repository source URL (default: https://github.com) -- `--branch` - Branch or tag to clone -- `--force` - Replace existing directory -- `--dest-dir` - Destination directory -- `--dest-name` - Custom destination name -- `--interactive` - Interactive configuration mode -- `--lake-update` - Run lake update after cloning (default: true) -- `--lake-build` - Run lake build after cloning (default: true) -- `--build-packages` - Specific packages to build - -## Modules - -### CLI Module - -The `leanup.cli` module provides the command-line interface: - -- **Main CLI**: Core commands for elan management and status monitoring -- **Repository CLI**: Commands for managing Lean repositories with advanced options - -### Utils Module - -The `leanup.utils` module provides utility functions for the package: - -- `execute_command`: Execute shell commands with proper error handling and cross-platform support -- `setup_logger`: Configure a logger with customizable output formats and color support - -### Repo Module - -The `leanup.repo` module provides repository management functionality: - -- `InstallConfig`: Configuration class for repository installation with validation -- `RepoManager`: Base class for directory and git operations -- `LeanRepo`: Specialized class for Lean project management with lake support -- `ElanManager`: Manage elan installation and toolchain operations \ No newline at end of file diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 2eec021..3aadb80 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -1,92 +1,92 @@ -# Quick Start +# 快速开始 -## Installation +## 安装 ```bash -# Install from PyPI +# 从 PyPI 安装 pip install leanup -# Or clone the repository and install +# 或者克隆仓库后安装 git clone https://github.com/Lean-zh/LeanUp.git cd LeanUp pip install -e . ``` -## Basic Usage +## 基础使用 -### Initialize elan +### 初始化 elan ```bash -# View help +# 查看帮助 leanup --help -# Install elan +# 安装 elan leanup init -# View current status +# 查看当前状态 leanup status ``` -### Install Lean Toolchain +### 安装 Lean 工具链 ```bash -# Install latest stable Lean toolchain +# 安装最新稳定版 Lean 工具链 leanup install -# Install specific Lean toolchain version +# 安装特定版本的 Lean 工具链 leanup install v4.14.0 ``` -### Manage Toolchains +### 管理工具链 ```bash -# Proxy execute elan commands +# 代理执行 elan 命令 leanup elan --help leanup elan toolchain list leanup elan toolchain install stable leanup elan default stable ``` -### Repository Management +### 仓库管理 ```bash -# Install Mathlib +# 安装 Mathlib leanup repo install leanprover-community/mathlib4 -# Install specific branch or tag +# 安装特定分支或标签 leanup repo install leanprover-community/mathlib4 -b v4.14.0 -# Install to custom directory +# 安装到自定义目录 leanup repo install Lean-zh/leanup -d /path/to/custom/dir -# Control build options +# 控制构建选项 leanup repo install leanprover-community/mathlib4 --lake-build -# Interactive mode +# 交互式 leanup repo install leanprover-community/mathlib4 -i -# Specify packages to build +# 指定要构建的包 leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" -# List installed repositories +# 列出已安装的仓库 leanup repo list -# Search repositories in specified directory +# 在指定目录中搜索仓库 leanup repo list --search-dir /path/to/repos -# Filter repositories by name +# 按名称过滤仓库 leanup repo list -n mathlib ``` -## Using InstallConfig +## 使用 InstallConfig -The `InstallConfig` class provides a programmatic way to configure repository installations: +`InstallConfig` 类提供了编程方式配置仓库安装： ```python from pathlib import Path from leanup.repo.manager import InstallConfig -# Create installation configuration +# 创建安装配置 config = InstallConfig( suffix="leanprover-community/mathlib4", source="https://github.com", @@ -99,71 +99,71 @@ config = InstallConfig( override=False ) -# Check if configuration is valid +# 检查配置是否有效 if config.is_valid: - print(f"Will install to: {config.dest_path}") + print(f"将安装到: {config.dest_path}") -# Execute installation +# 执行安装 config.install() -# Update configuration +# 更新配置 new_config = config.update(branch="v4.3.0", override=True) ``` -## Using the RepoManager +## 使用 RepoManager -The `RepoManager` class provides functionality for managing directories and git repositories: +`RepoManager` 类提供了管理目录和 git 仓库的功能： ```python from leanup.repo.manager import RepoManager -# Create a repo manager +# 创建仓库管理器 repo = RepoManager("/path/to/your/directory") -# Check if it's a git repository +# 检查是否为 git 仓库 if repo.is_gitrepo: - print("This is a git repository") + print("这是一个 git 仓库") status = repo.git_status() - print(f"Current branch: {status['branch']}") - print(f"Is dirty: {status['is_dirty']}") + print(f"当前分支: {status['branch']}") + print(f"是否有修改: {status['is_dirty']}") -# Clone a repository +# 克隆仓库 success = repo.clone_from( "https://github.com/owner/repo.git", branch="main", depth=1 ) -# File operations +# 文件操作 repo.write_file("test.txt", "Hello world") content = repo.read_file("test.txt") repo.edit_file("test.txt", "world", "universe", use_regex=False) -# List files and directories +# 列出文件和目录 files = repo.list_files("*.lean") dirs = repo.list_dirs() -# Execute commands +# 执行命令 stdout, stderr, returncode = repo.execute_command(["ls", "-la"]) ``` -## Using LeanRepo for Lean Projects +## 使用 LeanRepo 管理 Lean 项目 ```python from leanup.repo.manager import LeanRepo -# Create a Lean repo manager +# 创建 Lean 仓库管理器 lean_repo = LeanRepo("/path/to/lean/project") -# Get project information +# 获取项目信息 info = lean_repo.get_project_info() -print(f"Lean version: {info['lean_version']}") -print(f"Has lakefile.toml: {info['has_lakefile_toml']}") -print(f"Has lakefile.lean: {info['has_lakefile_lean']}") -print(f"Has lake-manifest.json: {info['has_lake_manifest']}") -print(f"Build directory exists: {info['build_dir_exists']}") +print(f"Lean 版本: {info['lean_version']}") +print(f"有 lakefile.toml: {info['has_lakefile_toml']}") +print(f"有 lakefile.lean: {info['has_lakefile_lean']}") +print(f"有 lake-manifest.json: {info['has_lake_manifest']}") +print(f"构建目录存在: {info['build_dir_exists']}") -# Lake operations +# Lake 操作 lean_repo.lake_init("my_project", "std", "lean") lean_repo.lake_update() lean_repo.lake_build("MyTarget") @@ -171,11 +171,11 @@ lean_repo.lake_env_lean("Main.lean", json=True) lean_repo.lake_clean() lean_repo.lake_test() -# Install using configuration +# 使用配置安装 config = InstallConfig( suffix="leanprover-community/mathlib4", lake_update=True, lake_build=False ) lean_repo.install(config) -``` \ No newline at end of file +``` diff --git a/docs/getting-started/quickstart.zh.md b/docs/getting-started/quickstart.zh.md deleted file mode 100644 index c21de39..0000000 --- a/docs/getting-started/quickstart.zh.md +++ /dev/null @@ -1,181 +0,0 @@ -# 快速开始 - -## 安装 - -```bash -# 从 PyPI 安装 -pip install leanup - -# 或者克隆仓库后安装 -git clone https://github.com/Lean-zh/LeanUp.git -cd LeanUp -pip install -e . -``` - -## 基础使用 - -### 初始化 elan - -```bash -# 查看帮助 -leanup --help - -# 安装 elan -leanup init - -# 查看当前状态 -leanup status -``` - -### 安装 Lean 工具链 - -```bash -# 安装最新稳定版 Lean 工具链 -leanup install - -# 安装特定版本的 Lean 工具链 -leanup install v4.14.0 -``` - -### 管理工具链 - -```bash -# 代理执行 elan 命令 -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable -``` - -### 仓库管理 - -```bash -# 安装 Mathlib -leanup repo install leanprover-community/mathlib4 - -# 安装特定分支或标签 -leanup repo install leanprover-community/mathlib4 -b v4.14.0 - -# 安装到自定义目录 -leanup repo install Lean-zh/leanup -d /path/to/custom/dir - -# 控制构建选项 -leanup repo install leanprover-community/mathlib4 --lake-build - -# 交互式 -leanup repo install leanprover-community/mathlib4 -i - -# 指定要构建的包 -leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" - -# 列出已安装的仓库 -leanup repo list - -# 在指定目录中搜索仓库 -leanup repo list --search-dir /path/to/repos - -# 按名称过滤仓库 -leanup repo list -n mathlib -``` - -## 使用 InstallConfig - -`InstallConfig` 类提供了编程方式配置仓库安装： - -```python -from pathlib import Path -from leanup.repo.manager import InstallConfig - -# 创建安装配置 -config = InstallConfig( - suffix="leanprover-community/mathlib4", - source="https://github.com", - branch="main", - dest_dir=Path("/path/to/repos"), - dest_name="mathlib4_main", - lake_update=True, - lake_build=True, - build_packages=["REPL", "REPL.Main"], - override=False -) - -# 检查配置是否有效 -if config.is_valid: - print(f"将安装到: {config.dest_path}") - -# 执行安装 -config.install() - -# 更新配置 -new_config = config.update(branch="v4.3.0", override=True) -``` - -## 使用 RepoManager - -`RepoManager` 类提供了管理目录和 git 仓库的功能： - -```python -from leanup.repo.manager import RepoManager - -# 创建仓库管理器 -repo = RepoManager("/path/to/your/directory") - -# 检查是否为 git 仓库 -if repo.is_gitrepo: - print("这是一个 git 仓库") - status = repo.git_status() - print(f"当前分支: {status['branch']}") - print(f"是否有修改: {status['is_dirty']}") - -# 克隆仓库 -success = repo.clone_from( - "https://github.com/owner/repo.git", - branch="main", - depth=1 -) - -# 文件操作 -repo.write_file("test.txt", "Hello world") -content = repo.read_file("test.txt") -repo.edit_file("test.txt", "world", "universe", use_regex=False) - -# 列出文件和目录 -files = repo.list_files("*.lean") -dirs = repo.list_dirs() - -# 执行命令 -stdout, stderr, returncode = repo.execute_command(["ls", "-la"]) -``` - -## 使用 LeanRepo 管理 Lean 项目 - -```python -from leanup.repo.manager import LeanRepo - -# 创建 Lean 仓库管理器 -lean_repo = LeanRepo("/path/to/lean/project") - -# 获取项目信息 -info = lean_repo.get_project_info() -print(f"Lean 版本: {info['lean_version']}") -print(f"有 lakefile.toml: {info['has_lakefile_toml']}") -print(f"有 lakefile.lean: {info['has_lakefile_lean']}") -print(f"有 lake-manifest.json: {info['has_lake_manifest']}") -print(f"构建目录存在: {info['build_dir_exists']}") - -# Lake 操作 -lean_repo.lake_init("my_project", "std", "lean") -lean_repo.lake_update() -lean_repo.lake_build("MyTarget") -lean_repo.lake_env_lean("Main.lean", json=True) -lean_repo.lake_clean() -lean_repo.lake_test() - -# 使用配置安装 -config = InstallConfig( - suffix="leanprover-community/mathlib4", - lake_update=True, - lake_build=False -) -lean_repo.install(config) -``` \ No newline at end of file diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..a47c53f --- /dev/null +++ b/docs/index.md @@ -0,0 +1,22 @@ +# LeanUp + +一个用于管理 Lean 数学证明语言环境的 Python 工具。 + +## 功能特性 + +- `leanup init`：安装并初始化 elan +- `leanup install [version]`：通过 elan 安装 Lean 工具链 +- `leanup status`：查看当前 elan / toolchain 状态 +- `leanup elan `：透明代理 elan 命令 +- `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 +- `leanup repo list`：查看已安装仓库 + +## 快速开始 + +查看[快速开始](getting-started/quickstart.md)开始使用 LeanUp。 + +## 开发说明 + +- 仓库级开发规范见 `AGENTS.md` 与 `DEVELOP.md` +- 当前以中文主文档为准，不继续维护英文平行版本 +- `repo install` 当前遵循：缺必要参数自动进入交互，`-i` 强制交互，`-I` 禁止交互 diff --git a/docs/zh/getting-started/quickstart.md b/docs/zh/getting-started/quickstart.md deleted file mode 100644 index c21de39..0000000 --- a/docs/zh/getting-started/quickstart.md +++ /dev/null @@ -1,181 +0,0 @@ -# 快速开始 - -## 安装 - -```bash -# 从 PyPI 安装 -pip install leanup - -# 或者克隆仓库后安装 -git clone https://github.com/Lean-zh/LeanUp.git -cd LeanUp -pip install -e . -``` - -## 基础使用 - -### 初始化 elan - -```bash -# 查看帮助 -leanup --help - -# 安装 elan -leanup init - -# 查看当前状态 -leanup status -``` - -### 安装 Lean 工具链 - -```bash -# 安装最新稳定版 Lean 工具链 -leanup install - -# 安装特定版本的 Lean 工具链 -leanup install v4.14.0 -``` - -### 管理工具链 - -```bash -# 代理执行 elan 命令 -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable -``` - -### 仓库管理 - -```bash -# 安装 Mathlib -leanup repo install leanprover-community/mathlib4 - -# 安装特定分支或标签 -leanup repo install leanprover-community/mathlib4 -b v4.14.0 - -# 安装到自定义目录 -leanup repo install Lean-zh/leanup -d /path/to/custom/dir - -# 控制构建选项 -leanup repo install leanprover-community/mathlib4 --lake-build - -# 交互式 -leanup repo install leanprover-community/mathlib4 -i - -# 指定要构建的包 -leanup repo install Lean-zh/repl --build-packages "REPL,REPL.Main" - -# 列出已安装的仓库 -leanup repo list - -# 在指定目录中搜索仓库 -leanup repo list --search-dir /path/to/repos - -# 按名称过滤仓库 -leanup repo list -n mathlib -``` - -## 使用 InstallConfig - -`InstallConfig` 类提供了编程方式配置仓库安装： - -```python -from pathlib import Path -from leanup.repo.manager import InstallConfig - -# 创建安装配置 -config = InstallConfig( - suffix="leanprover-community/mathlib4", - source="https://github.com", - branch="main", - dest_dir=Path("/path/to/repos"), - dest_name="mathlib4_main", - lake_update=True, - lake_build=True, - build_packages=["REPL", "REPL.Main"], - override=False -) - -# 检查配置是否有效 -if config.is_valid: - print(f"将安装到: {config.dest_path}") - -# 执行安装 -config.install() - -# 更新配置 -new_config = config.update(branch="v4.3.0", override=True) -``` - -## 使用 RepoManager - -`RepoManager` 类提供了管理目录和 git 仓库的功能： - -```python -from leanup.repo.manager import RepoManager - -# 创建仓库管理器 -repo = RepoManager("/path/to/your/directory") - -# 检查是否为 git 仓库 -if repo.is_gitrepo: - print("这是一个 git 仓库") - status = repo.git_status() - print(f"当前分支: {status['branch']}") - print(f"是否有修改: {status['is_dirty']}") - -# 克隆仓库 -success = repo.clone_from( - "https://github.com/owner/repo.git", - branch="main", - depth=1 -) - -# 文件操作 -repo.write_file("test.txt", "Hello world") -content = repo.read_file("test.txt") -repo.edit_file("test.txt", "world", "universe", use_regex=False) - -# 列出文件和目录 -files = repo.list_files("*.lean") -dirs = repo.list_dirs() - -# 执行命令 -stdout, stderr, returncode = repo.execute_command(["ls", "-la"]) -``` - -## 使用 LeanRepo 管理 Lean 项目 - -```python -from leanup.repo.manager import LeanRepo - -# 创建 Lean 仓库管理器 -lean_repo = LeanRepo("/path/to/lean/project") - -# 获取项目信息 -info = lean_repo.get_project_info() -print(f"Lean 版本: {info['lean_version']}") -print(f"有 lakefile.toml: {info['has_lakefile_toml']}") -print(f"有 lakefile.lean: {info['has_lakefile_lean']}") -print(f"有 lake-manifest.json: {info['has_lake_manifest']}") -print(f"构建目录存在: {info['build_dir_exists']}") - -# Lake 操作 -lean_repo.lake_init("my_project", "std", "lean") -lean_repo.lake_update() -lean_repo.lake_build("MyTarget") -lean_repo.lake_env_lean("Main.lean", json=True) -lean_repo.lake_clean() -lean_repo.lake_test() - -# 使用配置安装 -config = InstallConfig( - suffix="leanprover-community/mathlib4", - lake_update=True, - lake_build=False -) -lean_repo.install(config) -``` \ No newline at end of file diff --git a/docs/zh/index.md b/docs/zh/index.md deleted file mode 100644 index 83a40c7..0000000 --- a/docs/zh/index.md +++ /dev/null @@ -1,67 +0,0 @@ -# LeanUp - -一个用于管理 Lean 数学证明语言环境的 Python 工具。 - -## 功能特性 - -- **🔧 elan 管理**: 安装和管理 Lean 工具链管理器 elan -- **📦 仓库管理**: 安装和管理 Lean 仓库，支持高级配置选项 -- **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows -- **📦 简单易用**: 通过 `pip install leanup` 快速安装 - -## 快速开始 - -查看[快速开始](getting-started/quickstart.md)指南，开始使用 LeanUp。 - -## 命令行界面 - -LeanUp 提供了完整的 CLI，包含以下命令： - -### 主要命令 - -- `leanup init` - 初始化 elan 安装 -- `leanup install [version]` - 安装 Lean 工具链版本（通过 elan） -- `leanup status` - 显示当前状态和已安装工具链 -- `leanup elan ` - 代理 elan 命令 - -### 仓库管理 - -- `leanup repo install ` - 安装 Lean 仓库，支持灵活配置 -- `leanup repo list` - 列出已安装的仓库，支持过滤选项 - -#### 仓库安装选项 - -- `--source` - 仓库源 URL（默认：https://github.com） -- `--branch` - 要克隆的分支或标签 -- `--force` - 替换现有目录 -- `--dest-dir` - 目标目录 -- `--dest-name` - 自定义目标名称 -- `--interactive` - 交互式配置模式 -- `--lake-update` - 克隆后运行 lake update（默认：true） -- `--lake-build` - 克隆后运行 lake build（默认：true） -- `--build-packages` - 要构建的特定包 - -## 模块 - -### CLI 模块 - -`leanup.cli` 模块提供了命令行界面： - -- **主 CLI**: elan 管理和状态监控的核心命令 -- **仓库 CLI**: 管理 Lean 仓库的命令，支持高级选项 - -### Utils 模块 - -`leanup.utils` 模块提供了包的实用函数： - -- `execute_command`: 执行 shell 命令，具有适当的错误处理和跨平台支持 -- `setup_logger`: 配置日志记录器，支持自定义输出格式和颜色 - -### Repo 模块 - -`leanup.repo` 模块提供了仓库管理功能： - -- `InstallConfig`: 仓库安装的配置类，支持验证 -- `RepoManager`: 目录和 git 操作的基础类 -- `LeanRepo`: 专门用于 Lean 项目管理的类，支持 lake 操作 -- `ElanManager`: 管理 elan 安装和工具链操作 \ No newline at end of file diff --git a/leanup/cli/__init__.py b/leanup/cli/__init__.py index 177effa..7e8c12e 100644 --- a/leanup/cli/__init__.py +++ b/leanup/cli/__init__.py @@ -1,11 +1,14 @@ import click import sys -from pathlib import Path -from typing import Optional -from leanup.repo.elan import ElanManager from leanup.utils.custom_logger import setup_logger from leanup.cli.repo import repo +from leanup.cli.elan_ops import ( + init_elan, + install_lean_toolchain, + proxy_elan, + show_status, +) logger = setup_logger("leanup_cli") @@ -21,77 +24,32 @@ def cli(ctx): @cli.command() def init(): """Install latest elan""" - # Install elan - elan_manager = ElanManager() - if not elan_manager.is_elan_installed(): - click.echo("Installing elan...") - if elan_manager.install_elan(): - click.echo("✓ elan installed successfully") - else: - click.echo("✗ Failed to install elan", err=True) - sys.exit(1) - else: - click.echo("✓ elan is already installed") + init_elan() @cli.command() -@click.argument('version', required=False) -def install(version: Optional[str]): +@click.argument("version", required=False) +def install(version): """Install Lean toolchain version via elan""" - elan_manager = ElanManager() - - if not elan_manager.is_elan_installed(): - click.echo("✗ elan is not installed, trying to install...") - if not elan_manager.install_elan(): - click.echo("✗ Failed to install elan", err=True) - sys.exit(1) - click.echo("✓ elan installed successfully") - - if not elan_manager.install_lean(version): - click.echo(f"✗ Failed to install Lean toolchain {version}", err=True) - sys.exit(1) - - click.echo(f"✓ Lean toolchain {version} installed") + install_lean_toolchain(version) @cli.command() def status(): """Show status information""" - elan_manager = ElanManager() - - click.echo("=== LeanUp Status ===") - - # elan status - if elan_manager.is_elan_installed(): - version = elan_manager.get_elan_version() - click.echo(f"\nelan version: {version}") - click.echo("---------------------\n") - - # Show toolchains - elan_manager.proxy_elan_command(['show']) - else: - click.echo("elan: ✗ not installed") + show_status() @cli.command(context_settings=dict(ignore_unknown_options=True)) -@click.argument('args', nargs=-1, type=click.UNPROCESSED) +@click.argument("args", nargs=-1, type=click.UNPROCESSED) def elan(args): """Proxy elan commands""" - elan_manager = ElanManager() - - if not elan_manager.is_elan_installed(): - click.echo("elan is not installed. Run 'leanup init' first.", err=True) - sys.exit(1) - - # Execute elan command try: - result = elan_manager.proxy_elan_command(list(args)) + result = proxy_elan(list(args)) sys.exit(result) except KeyboardInterrupt: click.echo("\nInterrupted", err=True) sys.exit(1) -cli.add_command(repo) -if __name__ == '__main__': - cli() \ No newline at end of file +cli.add_command(repo) diff --git a/leanup/cli/elan_ops.py b/leanup/cli/elan_ops.py new file mode 100644 index 0000000..d0478c3 --- /dev/null +++ b/leanup/cli/elan_ops.py @@ -0,0 +1,55 @@ +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/interaction.py b/leanup/cli/interaction.py new file mode 100644 index 0000000..3aca7d4 --- /dev/null +++ b/leanup/cli/interaction.py @@ -0,0 +1,69 @@ +from __future__ import annotations + +from typing import Any + +import click + + +def normalize_interactive(interactive): + ctx = click.get_current_context(silent=True) + if ctx: + try: + if ( + ctx.get_parameter_source("interactive") + == click.core.ParameterSource.DEFAULT + ): + return None + except Exception: + pass + return interactive + + +def is_interactive_available() -> bool: + return ( + click.get_text_stream("stdin").isatty() + and click.get_text_stream("stdout").isatty() + ) + + +def resolve_interactive_mode(interactive, auto_prompt_condition: bool): + interactive = normalize_interactive(interactive) + can_prompt = is_interactive_available() + force_interactive = interactive is True + auto_interactive = interactive is None and can_prompt and auto_prompt_condition + need_prompt = force_interactive or auto_interactive + return interactive, can_prompt, force_interactive, auto_interactive, need_prompt + + +def abort_if_force_without_tty(force_interactive, can_prompt, usage): + if force_interactive and not can_prompt: + click.echo("Interactive mode was requested, but no TTY is available.", err=True) + click.echo(usage, err=True) + raise click.Abort() + + +def abort_if_missing_without_tty( + missing_required, interactive, can_prompt, message, usage +): + if missing_required and interactive is None and not can_prompt: + click.echo(message, err=True) + click.echo(usage, err=True) + raise click.Abort() + + +def resolve_value(*candidates: Any) -> Any: + for candidate in candidates: + if candidate is None: + continue + if isinstance(candidate, str) and not candidate.strip(): + continue + return candidate + return None + + +def ask_text(message: str, default: str = "") -> str: + return click.prompt(message, default=default, show_default=bool(default), err=True) + + +def ask_confirm(message: str, default: bool = True) -> bool: + return click.confirm(message, default=default, err=True) diff --git a/leanup/cli/repo.py b/leanup/cli/repo.py index 35f45ff..238c65c 100644 --- a/leanup/cli/repo.py +++ b/leanup/cli/repo.py @@ -1,16 +1,21 @@ import click -import shutil -import sys from pathlib import Path from typing import Optional -from urllib.parse import urlparse from leanup.const import LEANUP_CACHE_DIR -from leanup.repo.manager import RepoManager, LeanRepo, InstallConfig +from leanup.repo.manager import InstallConfig +from leanup.cli.interaction import ( + abort_if_force_without_tty, + abort_if_missing_without_tty, + ask_confirm, + ask_text, + resolve_interactive_mode, +) from leanup.utils.custom_logger import setup_logger logger = setup_logger("repo_cli") + @click.group() def repo(): """Repository management commands""" @@ -18,72 +23,130 @@ def repo(): @repo.command() -@click.argument('suffix', required=False) -@click.option('--source', '-s', help='Repository source', default='https://github.com') -@click.option('--branch', '-b', help='Branch or tag to clone') -@click.option('--force', '-f', is_flag=True, help='Replace existing directory') -@click.option('--dest-dir', '-d', help='Destination directory', type=click.Path(path_type=Path), default=LEANUP_CACHE_DIR / "repos") -@click.option('--dest-name', '-n', help='Destination name') -@click.option('--interactive', '-i', is_flag=True, help='Interactive mode') -@click.option('--lake-update', is_flag=True, help='Run lake update after cloning', default=True) -@click.option('--lake-build', is_flag=True, help='Run lake build after cloning', default=True) -@click.option('--build-packages', help='Packages to build after cloning') -def install(suffix: str, source: str, branch: Optional[str], force: bool, - dest_dir: Optional[Path], dest_name: Optional[str], interactive: bool, lake_update: bool, lake_build: bool, build_packages: str): +@click.argument("suffix", required=False) +@click.option("--source", "-s", help="Repository source", default="https://github.com") +@click.option("--branch", "-b", help="Branch or tag to clone") +@click.option("--force", "-f", is_flag=True, help="Replace existing directory") +@click.option( + "--dest-dir", + "-d", + help="Destination directory", + type=click.Path(path_type=Path), + default=LEANUP_CACHE_DIR / "repos", +) +@click.option("--dest-name", "-n", help="Destination name") +@click.option( + "--interactive/--no-interactive", + "-i/-I", + default=None, + help="Auto prompt on missing args, -i forces interactive, -I disables it.", +) +@click.option( + "--lake-update", is_flag=True, help="Run lake update after cloning", default=True +) +@click.option( + "--lake-build", is_flag=True, help="Run lake build after cloning", default=True +) +@click.option("--build-packages", help="Packages to build after cloning") +def install( + suffix: str, + source: str, + branch: Optional[str], + force: bool, + dest_dir: Optional[Path], + dest_name: Optional[str], + interactive: bool, + lake_update: bool, + lake_build: bool, + build_packages: str, +): """Install a repository""" - if interactive: - suffix = click.prompt("Suffix (user/repo) (required)", type=str, default=suffix) - source = click.prompt("Repository source", type=str, default=source) - branch = click.prompt("Branch or tag", type=str, default=branch or "") - config = InstallConfig( - suffix=suffix, - source=source, - branch=branch + usage = "Usage: leanup repo install [SUFFIX] [--source ] [--branch ] [--dest-dir ] [--dest-name ] [--lake-update] [--lake-build] [--build-packages ] [-i|-I]" + missing_required = not suffix + interactive, can_prompt, force_interactive, _, need_prompt = ( + resolve_interactive_mode( + interactive=interactive, + auto_prompt_condition=missing_required, ) - config._dest_dir = click.prompt("Destination directory", type=click.Path(path_type=Path), default=dest_dir) - if dest_name is None: - dest_name = config.suffix - config._dest_name = click.prompt("Destination name", type=str, default=dest_name) - config.lake_update = click.confirm("Run lake update after cloning?", default=lake_update) - config.lake_build = click.confirm("Run lake build after cloning?", default=lake_build) - config._build_packages = click.prompt("Packages to build after cloning(e.g. REPL,REPL.Main)", type=str, default=build_packages or "" ) - if config.dest_path.exists(): - config.override = click.confirm(f"Repository {config.dest_name} already exists in {config.dest_dir}. Override?", default=False) - if not config.override: - click.echo(f"Aborted.", err=True) - sys.exit(1) - else: - config = InstallConfig( + ) + + abort_if_force_without_tty(force_interactive, can_prompt, usage) + abort_if_missing_without_tty( + missing_required=missing_required, + interactive=interactive, + can_prompt=can_prompt, + message="Missing required repository suffix and no TTY is available for interactive prompts.", + usage=usage, + ) + + if missing_required and not need_prompt: + raise click.ClickException("Missing required repository suffix.") + + if need_prompt: + suffix = ask_text("Suffix (user/repo)", default=suffix or "") + source = ask_text("Repository source", default=source) + branch = ask_text("Branch or tag", default=branch or "") or None + dest_dir = Path(ask_text("Destination directory", default=str(dest_dir))) + preview = InstallConfig( suffix=suffix, source=source, branch=branch, dest_dir=dest_dir, dest_name=dest_name, - lake_update=lake_update, - lake_build=lake_build, - build_packages=build_packages, - override=force ) + dest_name = ask_text("Destination name", default=dest_name or preview.dest_name) + lake_update = ask_confirm("Run lake update after cloning?", default=lake_update) + lake_build = ask_confirm("Run lake build after cloning?", default=lake_build) + build_packages = ask_text( + "Packages to build after cloning (e.g. REPL,REPL.Main)", + default=build_packages or "", + ) + + config = InstallConfig( + suffix=suffix, + source=source, + branch=branch, + dest_dir=dest_dir, + dest_name=dest_name, + lake_update=lake_update, + lake_build=lake_build, + build_packages=build_packages, + override=force, + ) + + if need_prompt and config.dest_path.exists() and not config.override: + config.override = ask_confirm( + f"Repository {config.dest_name} already exists in {config.dest_dir}. Override?", + default=False, + ) + if not config.override: + click.echo("Aborted.", err=True) + raise click.Abort() + if not config.is_valid: click.echo("Error: Repository name is required", err=True) - sys.exit(1) + raise click.Abort() config.install() + @repo.command() -@click.option('--name', '-n', help='Filter by repository name') -@click.option('--search-dir', '-s', help='Directory to search for repositories', - type=click.Path(exists=True, file_okay=False, dir_okay=True, path_type=Path), - default=LEANUP_CACHE_DIR / "repos") +@click.option("--name", "-n", help="Filter by repository name") +@click.option( + "--search-dir", + "-s", + help="Directory to search for repositories", + type=click.Path(exists=True, file_okay=False, dir_okay=True, path_type=Path), + default=LEANUP_CACHE_DIR / "repos", +) def list(name: Optional[str], search_dir: Path): """List repositories in the specified directory""" - + if not search_dir.exists(): - click.echo(f"Directory {search_dir} doesn't exist.", err=True) - sys.exit(1) + raise click.ClickException(f"Directory {search_dir} doesn't exist.") names = [dir.name for dir in search_dir.iterdir() if dir.is_dir()] if name: names = [n for n in names if name in n] - + for name in names: click.echo(name) diff --git a/leanup/repo/elan.py b/leanup/repo/elan.py index c9de4c0..cf034b2 100644 --- a/leanup/repo/elan.py +++ b/leanup/repo/elan.py @@ -12,12 +12,13 @@ logger = setup_logger("elan_manager") + class ElanManager: """Elan toolchain manager""" def __init__(self): - self.elan_home = Path(os.environ.get('ELAN_HOME', Path.home() / '.elan')) - self.elan_bin_dir = self.elan_home / 'bin' + self.elan_home = Path(os.environ.get("ELAN_HOME", Path.home() / ".elan")) + self.elan_bin_dir = self.elan_home / "bin" self._elan_exe = None @property @@ -25,73 +26,75 @@ def elan_exe(self): if self._elan_exe is None: self._elan_exe = self.get_elan_executable() return self._elan_exe - + def get_elan_executable(self) -> Optional[Path]: """Get elan executable file path""" - elan_exe = 'elan.exe' if OS_TYPE == 'Windows' else 'elan' + elan_exe = "elan.exe" if OS_TYPE == "Windows" else "elan" elan_path = self.elan_bin_dir / elan_exe - + if elan_path.exists() and elan_path.is_file(): return elan_path - + # Try to find in PATH - elan_in_path = shutil.which('elan') + elan_in_path = shutil.which("elan") if elan_in_path: return Path(elan_in_path) - + return None - + def is_elan_installed(self) -> bool: """Check if elan is installed""" return self.elan_exe is not None - + def get_elan_version(self) -> Optional[str]: """Get installed elan version""" if not self.elan_exe: return None - + try: - output, error, code = execute_command([str(self.elan_exe), '--version']) + output, error, code = execute_command([str(self.elan_exe), "--version"]) if code == 0: # elan 4.0.0 (bb75b50d2 2025-01-30) - elan_regex = re.compile(r'elan\s+(\d+\.\d+\.\d+)') + elan_regex = re.compile(r"elan\s+(\d+\.\d+\.\d+)") match = elan_regex.search(output) if match: return match.group(1) else: - logger.warning(f"Failed to parse elan version from output: {output}") + logger.warning( + f"Failed to parse elan version from output: {output}" + ) return None except Exception as e: logger.error(f"Failed to get elan version: {e}") return None - + def download(self, url: str, target_path: Path) -> bool: """Download elan installer""" try: logger.info(f"Downloading elan installer: {url}") - + response = requests.get(url, stream=True) response.raise_for_status() - + target_path.parent.mkdir(parents=True, exist_ok=True) - - with open(target_path, 'wb') as f: + + with open(target_path, "wb") as f: for chunk in response.iter_content(chunk_size=8192): f.write(chunk) - + logger.info(f"Download completed: {target_path}") return True - + except Exception as e: logger.error(f"Failed to download elan installer: {e}") return False - + def install_elan(self, force: bool = False) -> bool: """Install elan with optional version specification. - + Args: force: Force reinstall even if already installed - + Returns: bool: True if installation successful, False otherwise """ @@ -102,13 +105,9 @@ def install_elan(self, force: bool = False) -> bool: try: # Use working_directory context manager for temporary directory with working_directory() as temp_dir: - if OS_TYPE == 'Windows': + if OS_TYPE == "Windows": # Windows uses PowerShell to run script directly from network (official recommended way) logger.info("Installing elan via PowerShell...") - # Set environment variables for non-interactive installation - env = os.environ.copy() - env['ELAN_HOME'] = str(self.elan_home) - # Use PowerShell to download and execute as recommended by official docs script_content = f""" $env:ELAN_HOME = "{self.elan_home}" @@ -116,46 +115,53 @@ def install_elan(self, force: bool = False) -> bool: & .\\elan-init.ps1 -y Remove-Item "elan-init.ps1" -ErrorAction SilentlyContinue """ - - cmd = ['powershell', '-ExecutionPolicy', 'Bypass', '-Command', script_content] + + cmd = [ + "powershell", + "-ExecutionPolicy", + "Bypass", + "-Command", + script_content, + ] else: download_url = "https://elan.lean-lang.org/elan-init.sh" # Linux/macOS use shell script installation - installer_path = temp_dir / 'elan-init.sh' + installer_path = temp_dir / "elan-init.sh" if not self.download(download_url, installer_path): return False - + logger.info("Running elan installation script...") - # Set environment variables for non-interactive installation - env = os.environ.copy() - env['ELAN_HOME'] = str(self.elan_home) - - cmd = ['sh', str(installer_path), '-y'] + + cmd = ["sh", str(installer_path), "-y"] output, error, code = execute_command(cmd, cwd=str(temp_dir)) if code != 0: logger.error(f"Installation failed: {error}") return False - + # Verify installation if self.is_elan_installed(): installed_version = self.get_elan_version() - logger.info(f"elan installed successfully! Version: {installed_version}") + logger.info( + f"elan installed successfully! Version: {installed_version}" + ) return True else: - logger.error("Installation completed, but elan executable not found") + logger.error( + "Installation completed, but elan executable not found" + ) return False - + except Exception as e: logger.error(f"Error occurred during elan installation: {e}") return False - - def install_lean(self, version:str=None)-> bool: + + def install_lean(self, version: str = None) -> bool: installed = self.get_installed_toolchains() if version in installed: logger.info(f"Lean toolchain {version} is already installed") return True - version = version or 'stable' - cmd = ['toolchain', 'install', version] + version = version or "stable" + cmd = ["toolchain", "install", version] result = self.proxy_elan_command(cmd) return result == 0 @@ -164,10 +170,10 @@ def proxy_elan_command(self, args: List[str]) -> int: if not self.elan_exe: if not self.install_elan(): return 1 - + # Build complete command cmd = [str(self.elan_exe)] + args - + try: # Pass directly to subprocess to maintain interactivity and streaming result = subprocess.run(cmd, check=False) @@ -175,19 +181,21 @@ def proxy_elan_command(self, args: List[str]) -> int: except Exception as e: logger.error(f"Failed to execute elan command: {e}") return 1 - + def get_installed_toolchains(self) -> List[str]: """Get list of installed toolchains""" if not self.elan_exe: return [] - + try: - output, error, code = execute_command([str(self.elan_exe), 'toolchain', 'list']) + output, error, code = execute_command( + [str(self.elan_exe), "toolchain", "list"] + ) if code == 0: toolchains = [] - for line in output.strip().split('\n'): + for line in output.strip().split("\n"): line = line.strip() - if line and not line.startswith('#'): + if line and not line.startswith("#"): # Remove status markers (like (default)) toolchain = line.split()[0] toolchains.append(toolchain) @@ -196,19 +204,19 @@ def get_installed_toolchains(self) -> List[str]: except Exception as e: logger.error(f"Failed to get toolchain list: {e}") return [] - + def get_status_info(self) -> Dict[str, any]: """Get elan status information""" info = { - 'installed': self.is_elan_installed(), - 'version': None, - 'elan_home': str(self.elan_home), - 'executable': None, - 'toolchains': [] + "installed": self.is_elan_installed(), + "version": None, + "elan_home": str(self.elan_home), + "executable": None, + "toolchains": [], } - - if info['installed']: - info['version'] = self.get_elan_version() - info['executable'] = str(self.elan_exe) - info['toolchains'] = self.get_installed_toolchains() + + if info["installed"]: + info["version"] = self.get_elan_version() + info["executable"] = str(self.elan_exe) + info["toolchains"] = self.get_installed_toolchains() return info diff --git a/leanup/repo/manager.py b/leanup/repo/manager.py index cbb9bff..2ef7b4f 100644 --- a/leanup/repo/manager.py +++ b/leanup/repo/manager.py @@ -1,12 +1,10 @@ -from dataclasses import dataclass +from dataclasses import dataclass, field import shutil import re from pathlib import Path -from token import OP from typing import Optional, Union, List, Dict, Any, Tuple import git import os -import toml from leanup.const import OS_TYPE, LEANUP_CACHE_DIR from leanup.utils.basic import execute_command from leanup.utils.custom_logger import setup_logger @@ -14,26 +12,39 @@ logger = setup_logger("repo_manager") -# Installation Config +@dataclass class InstallConfig: - def __init__(self, - suffix: Optional[str]=None, - source: Optional[str]='https://github.com', - url: Optional[str]=None, - branch: Optional[str]=None, - dest_name: Optional[str]=None, - dest_dir: Optional[Path]=None, - build_packages: Optional[List[str]]=None, - lake_update: bool = False, - lake_build:bool = False, - override: bool = False): + _suffix: Optional[str] = None + source: str = "https://github.com" + _url: Optional[str] = None + branch: Optional[str] = None + _dest_name: Optional[str] = None + _dest_dir: Optional[Path] = None + _build_packages: Optional[Union[List[str], str]] = None + lake_update: bool = False + lake_build: bool = False + override: bool = False + + def __init__( + self, + suffix: Optional[str] = None, + source: Optional[str] = "https://github.com", + url: Optional[str] = None, + branch: Optional[str] = None, + dest_name: Optional[str] = None, + dest_dir: Optional[Path] = None, + build_packages: Optional[Union[List[str], str]] = None, + lake_update: bool = False, + lake_build: bool = False, + override: bool = False, + ): self._suffix = suffix + self.source = source or "https://github.com" self._url = url + self.branch = branch self._dest_name = dest_name self._dest_dir = dest_dir self._build_packages = build_packages - self.branch = branch - self.source = source self.lake_update = lake_update self.lake_build = lake_build self.override = override @@ -45,16 +56,16 @@ def url(self): raise ValueError("suffix or url is required") return f"{self.source}/{self._suffix}" return self._url - + @property def suffix(self): if self._suffix is None: - suffix = self._url.strip().split('/')[-1] - if suffix.endswith('.git'): + suffix = self._url.strip().split("/")[-1] + if suffix.endswith(".git"): suffix = suffix[:-4] return suffix return self._suffix - + @property def dest_name(self): if self._dest_name is None: @@ -76,24 +87,24 @@ def build_packages(self): if not value: return [] if isinstance(value, str): - return [pkg.strip() for pkg in value.strip('[]').split(',')] + return [pkg.strip() for pkg in value.strip("[]").split(",")] elif isinstance(value, list): return value else: return [] - + @property def is_valid(self): return self.url is not None @property - def dest_path(self)->Path: + def dest_path(self) -> Path: return self.dest_dir / self.dest_name - + def get(self, key: str, default: Any = None) -> Any: """Get config value""" return getattr(self, key, default) - + def update(self, **kwargs): """Update config""" config = self.copy() @@ -103,8 +114,8 @@ def update(self, **kwargs): k = f"_{k}" setattr(config, k, v) return config - - def copy(self) -> 'InstallConfig': + + def copy(self) -> "InstallConfig": """Copy config""" return InstallConfig( suffix=self._suffix, @@ -121,24 +132,25 @@ def copy(self) -> 'InstallConfig': def install(self): repo = LeanRepo(self.dest_path) - repo.install(self) + return repo.install(self) + class RepoManager: """Class for managing directory operations and git functionality.""" - - def __init__(self, cwd: Union[str, Path]=None): + + def __init__(self, cwd: Union[str, Path] = None): """Initialize with a working directory. - + Args: cwd: Working directory path """ if cwd is None: - cwd = Path.cwd().resolve() + self.cwd = Path.cwd().resolve() else: self.cwd = Path(cwd).resolve() self._git_repo = None self._check_git_repo() - + def _check_git_repo(self) -> None: """Check if the current directory is a git repository and initialize git.Repo if it is.""" try: @@ -149,24 +161,26 @@ def _check_git_repo(self) -> None: logger.debug(f"{self.cwd} is not a git repository") except Exception as e: logger.error(f"Error checking git repository: {e}") - + @property def is_gitrepo(self) -> bool: """Check if the current directory is a git repository. - + Returns: bool: True if the directory is a git repository, False otherwise """ return self._git_repo is not None - - def clone_from(self, url: str, branch: Optional[str] = None, depth: Optional[int] = None) -> bool: + + def clone_from( + self, url: str, branch: Optional[str] = None, depth: Optional[int] = None + ) -> bool: """Clone a git repository to the current directory. - + Args: url: Git repository URL branch: Branch to clone (optional) depth: Depth for shallow clone (optional) - + Returns: bool: True if successful, False otherwise """ @@ -177,11 +191,11 @@ def clone_from(self, url: str, branch: Optional[str] = None, depth: Optional[int cmd.extend(["--branch", branch]) if depth: cmd.extend(["--depth", str(depth)]) - + # Execute clone command self.cwd.mkdir(parents=True, exist_ok=True) stdout, stderr, returncode = execute_command(cmd, cwd=str(self.cwd)) - + if returncode == 0: logger.info(f"Successfully cloned {url} to {self.cwd}") self._check_git_repo() # Refresh git repo status @@ -192,13 +206,13 @@ def clone_from(self, url: str, branch: Optional[str] = None, depth: Optional[int except Exception as e: logger.error(f"Error cloning repository: {e}") return False - + def clone_from_path(self, path: Union[str, Path]) -> bool: """Clone a git repository from a local path. - + Args: path: Local path to the git repository - + Returns: bool: True if successful, False otherwise """ @@ -213,41 +227,43 @@ def clone_from_path(self, path: Union[str, Path]) -> bool: except Exception as e: logger.error(f"Error cloning repository from path: {e}") return False - + def execute_command(self, command: Union[str, List[str]]) -> Tuple[str, str, int]: """Execute a command in the current directory. - + Args: command: Command to execute (string or list of arguments) - + Returns: Tuple containing stdout, stderr, and return code """ return execute_command(command, cwd=str(self.cwd)) - + def read_file(self, file_path: Union[str, Path]) -> str: """Read the contents of a file. - + Args: file_path: Path to the file (relative to cwd) - + Returns: str: File contents - + Raises: FileNotFoundError: If the file doesn't exist """ path = self.cwd / file_path - return path.read_text(encoding='utf-8') - - def write_file(self, file_path: Union[str, Path], content: str, append: bool = False) -> bool: + return path.read_text(encoding="utf-8") + + def write_file( + self, file_path: Union[str, Path], content: str, append: bool = False + ) -> bool: """Write content to a file. - + Args: file_path: Path to the file (relative to cwd) content: Content to write append: Whether to append to the file (default: False) - + Returns: bool: True if successful, False otherwise """ @@ -255,25 +271,29 @@ def write_file(self, file_path: Union[str, Path], content: str, append: bool = F path = self.cwd / file_path # Create parent directories if they don't exist path.parent.mkdir(parents=True, exist_ok=True) - mode = 'a' if append else 'w' - with open(path, mode, encoding='utf-8') as f: + mode = "a" if append else "w" + with open(path, mode, encoding="utf-8") as f: f.write(content) return True except Exception as e: logger.error(f"Error writing to file {file_path}: {e}") return False - - def edit_file(self, file_path: Union[str, Path], - find_text: str, replace_text: str, - use_regex: bool = False) -> bool: + + def edit_file( + self, + file_path: Union[str, Path], + find_text: str, + replace_text: str, + use_regex: bool = False, + ) -> bool: """Edit a file by replacing text. - + Args: file_path: Path to the file (relative to cwd) find_text: Text to find replace_text: Text to replace with use_regex: Whether to use regex for find/replace - + Returns: bool: True if successful, False otherwise """ @@ -282,26 +302,26 @@ def edit_file(self, file_path: Union[str, Path], if not path.exists(): logger.error(f"File {file_path} does not exist") return False - - content = path.read_text(encoding='utf-8') - + + content = path.read_text(encoding="utf-8") + if use_regex: new_content = re.sub(find_text, replace_text, content) else: new_content = content.replace(find_text, replace_text) - - path.write_text(new_content, encoding='utf-8') + + path.write_text(new_content, encoding="utf-8") return True except Exception as e: logger.error(f"Error editing file {file_path}: {e}") return False - + def list_files(self, pattern: Optional[str] = None) -> List[Path]: """List files in the current directory, optionally filtered by pattern. - + Args: pattern: Glob pattern to filter files - + Returns: List of Path objects """ @@ -309,13 +329,13 @@ def list_files(self, pattern: Optional[str] = None) -> List[Path]: return list(self.cwd.glob(pattern)) else: return [p for p in self.cwd.iterdir() if p.is_file()] - + def list_dirs(self, pattern: Optional[str] = None) -> List[Path]: """List subdirectories in the current directory, optionally filtered by pattern. - + Args: pattern: Glob pattern to filter directories - + Returns: List of Path objects """ @@ -323,11 +343,11 @@ def list_dirs(self, pattern: Optional[str] = None) -> List[Path]: return [p for p in self.cwd.glob(pattern) if p.is_dir()] else: return [p for p in self.cwd.iterdir() if p.is_dir()] - + # Git operations def git_status(self) -> Dict[str, Any]: """Get git status information. - + Returns: Dict containing status information or error message """ @@ -338,7 +358,9 @@ def git_status(self) -> Dict[str, Any]: "branch": self._git_repo.active_branch.name, "is_dirty": self._git_repo.is_dirty(), "untracked_files": self._git_repo.untracked_files, - "modified_files": [item.a_path for item in self._git_repo.index.diff(None)] + "modified_files": [ + item.a_path for item in self._git_repo.index.diff(None) + ], } except Exception as e: return {"error": str(e)} @@ -354,10 +376,10 @@ def git_init(self) -> bool: def git_add(self, paths: Union[str, List[str], None] = None) -> bool: """Add files to git staging area. - + Args: paths: File path(s) to add, or None to add all - + Returns: bool: True if successful, False otherwise """ @@ -379,41 +401,41 @@ def git_add(self, paths: Union[str, List[str], None] = None) -> bool: except Exception as e: logger.error(f"Error adding files to git: {e}") return False - + def git_commit(self, message: str) -> bool: """Commit changes to git repository. - + Args: message: Commit message - + Returns: bool: True if successful, False otherwise """ if not self.is_gitrepo: logger.warning("Not a git repository") return False - + try: self._git_repo.git.commit(m=message) return True except Exception as e: logger.error(f"Error committing changes: {e}") return False - + def git_pull(self, remote: str = "origin", branch: Optional[str] = None) -> bool: """Pull changes from remote repository. - + Args: remote: Remote name branch: Branch name (optional) - + Returns: bool: True if successful, False otherwise """ if not self.is_gitrepo: logger.warning("Not a git repository") return False - + try: if branch: self._git_repo.git.pull(remote, branch) @@ -423,21 +445,21 @@ def git_pull(self, remote: str = "origin", branch: Optional[str] = None) -> bool except Exception as e: logger.error(f"Error pulling changes: {e}") return False - + def git_push(self, remote: str = "origin", branch: Optional[str] = None) -> bool: """Push changes to remote repository. - + Args: remote: Remote name branch: Branch name (optional) - + Returns: bool: True if successful, False otherwise """ if not self.is_gitrepo: logger.warning("Not a git repository") return False - + try: if branch: self._git_repo.git.push(remote, branch) @@ -448,52 +470,53 @@ def git_push(self, remote: str = "origin", branch: Optional[str] = None) -> bool logger.error(f"Error pushing changes: {e}") return False + class LeanRepo(RepoManager): """Class for managing Lean repositories with lake support.""" - - def __init__(self, cwd: Union[str, Path]=None): + + def __init__(self, cwd: Union[str, Path] = None): """Initialize LeanRepo with working directory. - + Args: cwd: Working directory path """ super().__init__(cwd) - self.elan_home = Path(os.environ.get('ELAN_HOME', Path.home() / '.elan')) - self.elan_bin_dir = self.elan_home / 'bin' + self.elan_home = Path(os.environ.get("ELAN_HOME", Path.home() / ".elan")) + self.elan_bin_dir = self.elan_home / "bin" self._lake_exe = None self.lean_version = self.get_lean_toolchain() - + @property def lake_exe(self): if self._lake_exe is None: self._lake_exe = self.get_lake_executable() return self._lake_exe - + def get_lake_executable(self) -> Optional[Path]: """Get lake executable file path""" - lake_exe = 'lake.exe' if OS_TYPE == 'Windows' else 'lake' + lake_exe = "lake.exe" if OS_TYPE == "Windows" else "lake" lake_path = self.elan_bin_dir / lake_exe - + if lake_path.exists() and lake_path.is_file(): return lake_path - + # Try to find in PATH - lake_in_path = shutil.which('lake') + lake_in_path = shutil.which("lake") if lake_in_path: return Path(lake_in_path) - + return None def get_lean_toolchain(self) -> Optional[str]: """Read lean-toolchain file to get Lean version. - + Returns: str: Lean version if found, None otherwise """ try: toolchain_file = self.cwd / "lean-toolchain" if toolchain_file.exists(): - content = toolchain_file.read_text(encoding='utf-8').strip() + content = toolchain_file.read_text(encoding="utf-8").strip() logger.debug(f"Found Lean toolchain: {content}") return content else: @@ -502,28 +525,28 @@ def get_lean_toolchain(self) -> Optional[str]: except Exception as e: logger.error(f"Error reading lean-toolchain: {e}") return None - + def lake(self, args: List[str]) -> Tuple[str, str, int]: """Execute lake command with given arguments. - + Args: args: List of lake command arguments - + Returns: Tuple containing stdout, stderr, and return code """ if isinstance(args, str): args = [args] command = [str(self.lake_exe)] + args - logger.debug("Executing lake command: " + ' '.join(command)) + logger.debug("Executing lake command: " + " ".join(command)) return self.execute_command(command) - + def lake_env_which(self, name: str) -> Tuple[str, str, int]: """Check if a lake package is installed. - + Args: name: Package name - + Returns: Tuple containing stdout, stderr, and return code """ @@ -533,13 +556,15 @@ def lake_env_which(self, name: str) -> Tuple[str, str, int]: else: logger.error(f"Error checking package {name}: {err}") return msg, err, code - - def lake_init(self, - name: Optional[str] = None, - template: Optional[str] = None, - language: Optional[str] = None) -> Tuple[str, str, int]: + + def lake_init( + self, + name: Optional[str] = None, + template: Optional[str] = None, + language: Optional[str] = None, + ) -> Tuple[str, str, int]: """Initialize lake repository. - + Args: name: Repository name template: Template name @@ -551,7 +576,7 @@ def lake_init(self, exe executable only lib library only math library only with a mathlib dependency - + Templates can be suffixed with `.lean` or `.toml` to produce a Lean or TOML version of the configuration file, respectively. The default is Lean. @@ -564,23 +589,27 @@ def lake_init(self, if name: cmds.append(name) if template: - assert name is not None, "Repository name is required when template is specified" + assert name is not None, ( + "Repository name is required when template is specified" + ) assert template in ["std", "exe", "lib", "math"], "Invalid template name" cmds.append(template) if language: - assert language in ["lean", "toml", '.lean', '.toml'], "Invalid language name" - if not language.startswith('.'): - language = '.' + language + assert language in ["lean", "toml", ".lean", ".toml"], ( + "Invalid language name" + ) + if not language.startswith("."): + language = "." + language if template is not None: cmds[-1] += f".{language}" return self.lake(cmds) - + def lake_build(self, target: Optional[str] = None) -> Tuple[str, str, int]: """Build the Lean project using lake. - + Args: target: Optional build target - + Returns: Tuple containing stdout, stderr, and return code """ @@ -588,27 +617,28 @@ def lake_build(self, target: Optional[str] = None) -> Tuple[str, str, int]: if target: args.append(target) return self.lake(args) - + def lake_update(self) -> Tuple[str, str, int]: """Update dependencies using lake. - + Returns: Tuple containing stdout, stderr, and return code """ return self.lake(["update"]) - + def lake_env_lean( - self, - filepath: Union[str, Path], - json: bool = True, + self, + filepath: Union[str, Path], + json: bool = True, options: Optional[Dict[str, Any]] = None, - nproc: Optional[int] = None) -> Tuple[str, str, int]: + nproc: Optional[int] = None, + ) -> Tuple[str, str, int]: """Run lean file with lake environment. - + Args: filepath: Path to the Lean file json: Whether to return JSON output, default is True - + Returns: Tuple containing stdout, stderr, and return code """ @@ -616,48 +646,48 @@ def lake_env_lean( if json: args.append("--json") if options is not None: - opts = ["-D {}={}".format(k,v) for k,v in options.items()] + opts = ["-D {}={}".format(k, v) for k, v in options.items()] args += opts if isinstance(nproc, int) and nproc > 0: # nproc += 1 args += ["-j", str(nproc)] args.append(str(filepath)) return self.lake(args) - + def lake_clean(self) -> Tuple[str, str, int]: """Clean build artifacts using lake. - + Returns: Tuple containing stdout, stderr, and return code """ return self.lake(["clean"]) - + def lake_test(self) -> Tuple[str, str, int]: """Run tests using lake. - + Returns: Tuple containing stdout, stderr, and return code """ return self.lake(["test"]) - + def get_project_info(self) -> Dict[str, Any]: """Get comprehensive project information. - + Returns: Dict containing project information """ info = { - 'lean_version': self.get_lean_toolchain(), - 'has_lakefile_toml': (self.cwd / "lakefile.toml").exists(), - 'has_lakefile_lean': (self.cwd / "lakefile.lean").exists(), - 'has_lake_manifest': (self.cwd / "lake-manifest.json").exists(), - 'build_dir_exists': (self.cwd / ".lake").exists(), + "lean_version": self.get_lean_toolchain(), + "has_lakefile_toml": (self.cwd / "lakefile.toml").exists(), + "has_lakefile_lean": (self.cwd / "lakefile.lean").exists(), + "has_lake_manifest": (self.cwd / "lake-manifest.json").exists(), + "build_dir_exists": (self.cwd / ".lake").exists(), } return info - + def install(self, config: InstallConfig, **kwargs): """Install Lean repository. - + Args: config: InstallConfig object kwargs: Additional keyword arguments for lake_init @@ -676,7 +706,7 @@ def install(self, config: InstallConfig, **kwargs): success = repo.clone_from( url=config.url, branch=config.branch, - depth=1 # Shallow clone for faster download + depth=1, # Shallow clone for faster download ) if not success: logger.error(f"Failed to clone repository: {config.url}") diff --git a/leanup/utils/config.py b/leanup/utils/config.py index 4aebd74..158ec4b 100644 --- a/leanup/utils/config.py +++ b/leanup/utils/config.py @@ -2,16 +2,17 @@ from pathlib import Path from typing import Dict, Any, Optional from leanup.utils.custom_logger import setup_logger -from leanup.const import LEANUP_CACHE_DIR, LEANUP_CONFIG_DIR +from leanup.const import LEANUP_CONFIG_DIR logger = setup_logger("config_manager") + class ConfigManager: """Manage leanup configuration""" - + def __init__(self, config_dir: Optional[Path] = None): """Initialize config manager - + Args: config_dir: Custom config directory (default: LEANUP_CONFIG_DIR) """ @@ -19,62 +20,63 @@ def __init__(self, config_dir: Optional[Path] = None): self.config_dir = Path(config_dir) else: self.config_dir = LEANUP_CONFIG_DIR - + # Ensure config directory exists self.config_dir.mkdir(parents=True, exist_ok=True) - + self.config_path = self.config_dir / "config.yaml" self._config = None - + def config_exists(self) -> bool: """Check if config file exists""" return self.config_path.exists() - + def init_config(self) -> bool: """Initialize config file with default settings""" self.config_dir.mkdir(parents=True, exist_ok=True) - # Empty toml file - with open(self.config_path, 'w', encoding='utf-8') as f: - f.write('') - + with open(self.config_path, "w", encoding="utf-8") as f: + f.write("") + self._config = {} + return True + def save_config(self, config: Dict[str, Any]) -> bool: """Save config to file""" try: - with open(self.config_path, 'w', encoding='utf-8') as f: + with open(self.config_path, "w", encoding="utf-8") as f: yaml.dump(config, f, default_flow_style=False) self._config = config return True except Exception as e: logger.error(f"Failed to save config: {e}") return False - + def load_config(self) -> Dict[str, Any]: """Load config from file""" if self._config is not None: return self._config - + if not self.config_exists(): logger.warning("Config file not found, using defaults") return {} - + try: - with open(self.config_path, 'r', encoding='utf-8') as f: + with open(self.config_path, "r", encoding="utf-8") as f: self._config = yaml.safe_load(f) or {} return self._config except Exception as e: logger.error(f"Failed to load config: {e}") return {} - + def get(self, key: str, default: Any = None) -> Any: """Get config value by key (supports dot notation)""" config = self.load_config() - keys = key.split('.') - + keys = key.split(".") + value = config for k in keys: if isinstance(value, dict) and k in value: value = value[k] else: return default - + return value diff --git a/mkdocs.yml b/mkdocs.yml index bc76441..1d05512 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -1,5 +1,5 @@ -site_name: LeanUp Documentation -site_description: Python package for Lean Environment Management +site_name: LeanUp 文档 +site_description: 用于管理 Lean 数学证明语言环境的 Python 工具 site_author: Lean-zh Community site_url: https://www.leanprover.cn/LeanUp/ @@ -36,30 +36,10 @@ theme: - content.code.annotate - content.action.edit - content.action.view - language: en + language: zh plugins: - search - - i18n: - docs_structure: folder - fallback_to_default: true - reconfigure_material: true - reconfigure_search: true - languages: - - locale: en - default: true - name: English - build: true - site_name: "LeanUp Documentation" - - locale: zh - name: 中文 - build: true - site_name: "LeanUp 文档" - nav_translations: - Home: 首页 - Getting Started: 开始使用 - Quick Start: 快速开始 - API Reference: API 文档 markdown_extensions: - pymdownx.highlight: @@ -84,18 +64,11 @@ markdown_extensions: custom_checkbox: true extra: - alternate: - - name: English - link: /LeanUp/ - lang: en - - name: 中文 - link: /LeanUp/zh/ - lang: zh social: - icon: fontawesome/brands/github link: https://github.com/Lean-zh/LeanUp nav: - - Home: index.md - - Getting Started: - - Quick Start: getting-started/quickstart.md - # - API Reference: api-reference.md \ No newline at end of file + - 首页: index.md + - 开始使用: + - 快速开始: getting-started/quickstart.md + # - API Reference: api-reference.md diff --git a/tests/test_cli.py b/tests/test_cli.py index f83d197..25aa50f 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -9,18 +9,18 @@ class TestCLI: """Test CLI commands""" - + def setup_method(self): """Setup test environment""" self.runner = CliRunner() - + def test_cli_help(self): """Test CLI help command""" - result = self.runner.invoke(cli, ['--help']) + result = self.runner.invoke(cli, ["--help"]) assert result.exit_code == 0 - assert 'LeanUp - Lean project management tool' in result.output - - @patch('leanup.cli.ElanManager') + 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 @@ -28,64 +28,64 @@ def test_init_command(self, mock_elan_manager): 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']) - + + result = self.runner.invoke(cli, ["init"]) + if result.exit_code == 0: - '✓ elan installed successfully' in result.output + "✓ elan installed successfully" in result.output # mock_elan.install_elan.assert_called_once() - - @patch('leanup.cli.ElanManager') + + @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']) - + + result = self.runner.invoke(cli, ["init"]) + assert result.exit_code == 0 - assert '✓ elan is already installed' in result.output + assert "✓ elan is already installed" in result.output mock_elan.install_elan.assert_not_called() - - @patch('leanup.cli.ElanManager') + + @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']) - + + result = self.runner.invoke(cli, ["install"]) + assert result.exit_code == 0 - - @patch('leanup.cli.ElanManager') + + @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']) - + + result = self.runner.invoke(cli, ["install", "v4.10.0"]) + assert result.exit_code == 0 - - @patch('leanup.cli.ElanManager') + + @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']) - + + result = self.runner.invoke(cli, ["install", "v4.10.0"]) + assert result.exit_code == 0 - - @patch('leanup.cli.ElanManager') + + @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() @@ -93,64 +93,66 @@ def test_install_command_elan_not_installed(self, mock_elan_manager): 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']) - + + result = self.runner.invoke(cli, ["install"]) + assert result.exit_code == 0 - assert '✓ elan installed successfully' in result.output + 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.ElanManager') + + @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.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']) - + + 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.ElanManager') + 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']) - + + result = self.runner.invoke(cli, ["status"]) + assert result.exit_code == 0 - assert 'elan: ✗ not installed' in result.output - - @patch('leanup.cli.ElanManager') + 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.ElanManager') + + 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']) - + + 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 "elan is not installed. Run 'leanup init' first." in result.output diff --git a/tests/test_repo_cli.py b/tests/test_repo_cli.py new file mode 100644 index 0000000..143159e --- /dev/null +++ b/tests/test_repo_cli.py @@ -0,0 +1,82 @@ +from pathlib import Path +import importlib + +repo_cli_module = importlib.import_module("leanup.cli.repo") + +from click.testing import CliRunner + +from leanup.cli import cli + + +def test_repo_install_no_interactive_missing_suffix_fails(monkeypatch): + runner = CliRunner() + monkeypatch.setattr( + repo_cli_module, + "resolve_interactive_mode", + lambda interactive, auto_prompt_condition: (False, True, False, False, False), + ) + + result = runner.invoke(cli, ["repo", "install", "-I"]) + + assert result.exit_code != 0 + assert "Missing required repository suffix" in result.output + + +def test_repo_install_interactive_prompts_and_installs(monkeypatch, tmp_path): + runner = CliRunner() + values = iter( + [ + "leanprover-community/mathlib4", + "https://github.com", + "v4.14.0", + str(tmp_path), + "mathlib4_v4140", + "REPL,REPL.Main", + ] + ) + confirmations = iter([True, False, False]) + captured = {} + + monkeypatch.setattr( + repo_cli_module, + "resolve_interactive_mode", + lambda interactive, auto_prompt_condition: (None, True, False, True, True), + ) + monkeypatch.setattr( + repo_cli_module, + "ask_text", + lambda message, default="": next(values), + ) + monkeypatch.setattr( + repo_cli_module, + "ask_confirm", + lambda message, default=True: next(confirmations), + ) + + def fake_install(self): + captured.update( + { + "suffix": self.suffix, + "source": self.source, + "branch": self.branch, + "dest_dir": self.dest_dir, + "dest_name": self.dest_name, + "lake_update": self.lake_update, + "lake_build": self.lake_build, + "build_packages": self.build_packages, + } + ) + + monkeypatch.setattr("leanup.repo.manager.InstallConfig.install", fake_install) + + result = runner.invoke(cli, ["repo", "install"]) + + assert result.exit_code == 0 + assert captured["suffix"] == "leanprover-community/mathlib4" + assert captured["source"] == "https://github.com" + assert captured["branch"] == "v4.14.0" + assert captured["dest_dir"] == Path(tmp_path) + assert captured["dest_name"] == "mathlib4_v4140" + assert captured["lake_update"] is True + assert captured["lake_build"] is False + assert captured["build_packages"] == ["REPL", "REPL.Main"] From ed9cec1aa6fea6eb8f2007efee7cb76a30dc8cff Mon Sep 17 00:00:00 2001 From: rexwzh <1073853456@qq.com> Date: Tue, 7 Apr 2026 07:30:25 +0800 Subject: [PATCH 2/8] refactor: polish leanup interaction prompts --- leanup/cli/interaction.py | 52 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 50 insertions(+), 2 deletions(-) diff --git a/leanup/cli/interaction.py b/leanup/cli/interaction.py index 3aca7d4..f9a47a0 100644 --- a/leanup/cli/interaction.py +++ b/leanup/cli/interaction.py @@ -61,9 +61,57 @@ def resolve_value(*candidates: Any) -> Any: return None +def _get_console(): + try: + from rich.console import Console + except ImportError: + return None + return Console(stderr=True) + + +def _render_heading(title: str, subtitle: str | None = None) -> None: + console = _get_console() + if not console: + if subtitle: + click.echo(f"\n{title}\n{subtitle}", err=True) + else: + click.echo(f"\n{title}", err=True) + return + + try: + from rich.panel import Panel + except ImportError: + if subtitle: + click.echo(f"\n{title}\n{subtitle}", err=True) + else: + click.echo(f"\n{title}", err=True) + return + + console.print( + Panel.fit( + subtitle or "", + title=f"[bold cyan]{title}[/bold cyan]", + border_style="cyan", + padding=(0, 1), + ) + ) + + +def _render_note(message: str) -> None: + console = _get_console() + if not console: + click.echo(message, err=True) + return + console.print(f"[dim]{message}[/dim]") + + def ask_text(message: str, default: str = "") -> str: - return click.prompt(message, default=default, show_default=bool(default), err=True) + _render_heading("Input", message) + if default: + _render_note(f"Press Enter to keep default: {default}") + return click.prompt("Value", default=default, show_default=bool(default), err=True) def ask_confirm(message: str, default: bool = True) -> bool: - return click.confirm(message, default=default, err=True) + _render_heading("Confirm", message) + return click.confirm("Continue", default=default, err=True) From be0e0419e8c5f5d0a3829206a443c3e89d8c4d5f Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Tue, 7 Apr 2026 16:03:55 +0800 Subject: [PATCH 3/8] feat: add setup command for cached Lean project bootstrap --- README.md | 69 ++++---- docs/getting-started/quickstart.md | 41 +++-- docs/index.md | 5 +- leanup/__init__.py | 10 +- leanup/cli/__init__.py | 4 + leanup/cli/setup.py | 131 +++++++++++++++ leanup/repo/__init__.py | 10 +- leanup/repo/elan.py | 16 +- leanup/repo/project_setup.py | 207 ++++++++++++++++++++++++ tests/test_elan_manager.py | 23 ++- tests/test_setup.py | 248 +++++++++++++++++++++++++++++ 11 files changed, 696 insertions(+), 68 deletions(-) create mode 100644 leanup/cli/setup.py create mode 100644 leanup/repo/project_setup.py create mode 100644 tests/test_setup.py diff --git a/README.md b/README.md index cc6a3d7..b4107ff 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,7 @@ ## 🎯 功能特性 - **📦 仓库管理**: 安装和管理 Lean 仓库，支持命令优先、交互兜底的配置流程 +- **⚡ 项目初始化**: 快速创建固定 Lean 版本的项目，并复用同版本 mathlib 缓存 - **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows - **📦 简单易用**: 通过 `pip install leanup` 快速安装 - **🔄 命令代理**: 透明代理所有 elan 命令，无缝体验 @@ -45,48 +46,15 @@ pip install -e . # 查看帮助 leanup --help -# 安装 elan 并初始化配置 -leanup init +# 快速初始化一个 Lean + mathlib 项目 +leanup setup ./Demo --lean-version v4.27.0 -# 安装 -leanup install # stable - -# 查看状态 -leanup status - -# 代理执行 elan 命令 -leanup elan --help +# 如需手动透传 elan，也可以继续使用 leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable ``` ## 📖 详细使用指南 -### 管理 Lean 工具链 - -安装 elan 后，您可以使用 `leanup elan` 命令来管理 Lean 工具链： - -```bash -# 列出所有可用的工具链 -leanup elan toolchain list - -# 安装稳定版工具链 -leanup elan toolchain install stable - -# 安装夜间构建版本 -leanup elan toolchain install leanprover/lean4:nightly - -# 设置默认工具链 -leanup elan default stable - -# 更新所有工具链 -leanup elan update - -# 查看当前活动的工具链 -leanup elan show -``` - ### 仓库管理 ```bash @@ -121,6 +89,35 @@ leanup repo list --search-dir /path/to/repos leanup repo list -n mathlib ``` +### 快速初始化项目 + +`leanup setup` 用于快速创建一个固定 Lean 版本的项目，并按需要为 `mathlib` 依赖准备共享缓存。 + +```bash +# 创建一个带 mathlib 的项目，默认有缓存就复用，没有缓存就构建 +leanup setup ./Demo --lean-version v4.27.0 + +# 首次为某个版本准备依赖缓存时，从头构建一次 +leanup setup ./DemoBuild --lean-version v4.27.0 --dependency-mode build + +# 后续同版本项目可直接软链接复用缓存 +leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink + +# 创建不带 mathlib 的纯 Lean 项目 +leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib + +# 指定 Lake 项目名，并覆盖已存在目录 +leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force +``` + +规则说明： + +- `--dependency-mode symlink` 只在启用 `mathlib` 时可用 +- 默认缓存目录为 `LEANUP_CACHE_DIR/setup/mathlib//packages` +- 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 +- 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 +- `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装 + ### 交互式安装 使用 `leanup repo install -i` 时，您可以配置： diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 3aadb80..478af8f 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -14,39 +14,38 @@ pip install -e . ## 基础使用 -### 初始化 elan +### 查看帮助 ```bash -# 查看帮助 leanup --help - -# 安装 elan -leanup init - -# 查看当前状态 -leanup status ``` -### 安装 Lean 工具链 +### 快速创建项目 ```bash -# 安装最新稳定版 Lean 工具链 -leanup install +# 创建一个带 mathlib 的 Lean 项目，默认有缓存就复用，没有缓存就构建 +leanup setup ./Demo --lean-version v4.27.0 -# 安装特定版本的 Lean 工具链 -leanup install v4.14.0 -``` +# 首次为某个版本准备缓存时，从头构建依赖 +leanup setup ./DemoBuild --lean-version v4.27.0 --dependency-mode build -### 管理工具链 +# 后续项目直接复用共享依赖缓存 +leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink -```bash -# 代理执行 elan 命令 -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable +# 创建不依赖 mathlib 的纯 Lean 项目 +leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib ``` +说明： + +- 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` +- Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` +- `symlink` 模式只对 `mathlib` 项目开放 +- 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 +- 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 +- `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装 +- 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...` + ### 仓库管理 ```bash diff --git a/docs/index.md b/docs/index.md index a47c53f..2de3f4f 100644 --- a/docs/index.md +++ b/docs/index.md @@ -4,10 +4,7 @@ ## 功能特性 -- `leanup init`：安装并初始化 elan -- `leanup install [version]`：通过 elan 安装 Lean 工具链 -- `leanup status`：查看当前 elan / toolchain 状态 -- `leanup elan `：透明代理 elan 命令 +- `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 - `leanup repo list`：查看已安装仓库 diff --git a/leanup/__init__.py b/leanup/__init__.py index 2d87293..9f20293 100644 --- a/leanup/__init__.py +++ b/leanup/__init__.py @@ -4,10 +4,18 @@ __email__ = 'leanprover@outlook.com' __version__ = '0.1.9' -from .repo import RepoManager, ElanManager, LeanRepo +from .repo import ( + RepoManager, + ElanManager, + LeanRepo, + LeanProjectSetup, + SetupConfig, + SetupResult, +) from .utils import setup_logger, execute_command, working_directory __all__ = [ 'RepoManager', 'ElanManager', 'LeanRepo', + 'LeanProjectSetup', 'SetupConfig', 'SetupResult', "setup_logger", "execute_command", "working_directory" ] diff --git a/leanup/cli/__init__.py b/leanup/cli/__init__.py index 7e8c12e..76a79f1 100644 --- a/leanup/cli/__init__.py +++ b/leanup/cli/__init__.py @@ -3,6 +3,7 @@ from leanup.utils.custom_logger import setup_logger from leanup.cli.repo import repo +from leanup.cli.setup import setup_project from leanup.cli.elan_ops import ( init_elan, install_lean_toolchain, @@ -40,6 +41,9 @@ def status(): show_status() +cli.add_command(setup_project) + + @cli.command(context_settings=dict(ignore_unknown_options=True)) @click.argument("args", nargs=-1, type=click.UNPROCESSED) def elan(args): diff --git a/leanup/cli/setup.py b/leanup/cli/setup.py new file mode 100644 index 0000000..cf3a616 --- /dev/null +++ b/leanup/cli/setup.py @@ -0,0 +1,131 @@ +from __future__ import annotations + +from pathlib import Path + +import click + +from leanup.cli.interaction import ( + abort_if_force_without_tty, + abort_if_missing_without_tty, + ask_confirm, + ask_text, + resolve_interactive_mode, +) +from leanup.repo.project_setup import LeanProjectSetup, SetupConfig + + +@click.command(name="setup") +@click.argument("path", required=False, type=click.Path(path_type=Path)) +@click.option( + "--lean-version", + "-v", + help="Lean version like v4.27.0 or 4.27.0.", +) +@click.option("--name", help="Lake project name. Defaults to the target directory name.") +@click.option( + "--mathlib/--no-mathlib", + default=True, + help="Enable or disable the mathlib dependency.", +) +@click.option( + "--dependency-mode", + "-m", + type=click.Choice(["symlink", "build"]), + default=None, + help="Use cached mathlib packages via symlink, or build dependencies from scratch.", +) +@click.option("--force", "-f", is_flag=True, help="Replace the target directory if it exists.") +@click.option( + "--interactive/--no-interactive", + "-i/-I", + default=None, + help="Auto prompt on missing args, -i forces interactive, -I disables it.", +) +def setup_project( + path: Path | None, + lean_version: str | None, + name: str | None, + mathlib: bool, + dependency_mode: str | None, + force: bool, + 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]" + missing_required = path is None or not lean_version + interactive, can_prompt, force_interactive, _, need_prompt = ( + resolve_interactive_mode( + interactive=interactive, + auto_prompt_condition=missing_required, + ) + ) + + abort_if_force_without_tty(force_interactive, can_prompt, usage) + abort_if_missing_without_tty( + missing_required=missing_required, + interactive=interactive, + can_prompt=can_prompt, + message="Missing required setup path or Lean version and no TTY is available for interactive prompts.", + usage=usage, + ) + + if missing_required and not need_prompt: + raise click.ClickException("Missing required setup path or Lean version.") + + if need_prompt: + path_input = ask_text("Project directory", default=str(path) if path else "") + path = Path(path_input) + lean_version = ask_text("Lean version", default=lean_version or "") + name = ask_text("Lake project name", default=name or path.name) or None + mathlib = ask_confirm("Enable mathlib dependency?", default=mathlib) + + preview_mode = None + try: + preview_mode = SetupConfig( + target_dir=path, + lean_version=lean_version, + project_name=name, + mathlib=mathlib, + dependency_mode=dependency_mode, + force=force, + ).resolved_dependency_mode + except ValueError: + preview_mode = dependency_mode + + default_mode = preview_mode or dependency_mode or ("build" if not mathlib else "symlink") + + if mathlib: + dependency_mode = ask_text( + "Dependency mode (symlink/build)", + default=default_mode, + ).strip() or default_mode + else: + dependency_mode = "build" + + force = ask_confirm("Replace the target directory if it exists?", default=force) + + config = SetupConfig( + target_dir=path, + lean_version=lean_version, + project_name=name, + mathlib=mathlib, + dependency_mode=dependency_mode, + force=force, + ) + manager = LeanProjectSetup() + + try: + result = manager.setup(config) + except (ValueError, RuntimeError) as exc: + raise click.ClickException(str(exc)) from exc + + click.echo(f"✓ Project ready: {result.target_dir}") + click.echo(f" Lean version: {result.lean_version}") + click.echo(f" Mathlib: {'enabled' if result.mathlib else 'disabled'}") + 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.") diff --git a/leanup/repo/__init__.py b/leanup/repo/__init__.py index 8db6172..5099f6e 100644 --- a/leanup/repo/__init__.py +++ b/leanup/repo/__init__.py @@ -2,5 +2,13 @@ from .manager import RepoManager, LeanRepo from .elan import ElanManager +from .project_setup import LeanProjectSetup, SetupConfig, SetupResult -__all__ = ['RepoManager', 'ElanManager', 'LeanRepo'] +__all__ = [ + 'RepoManager', + 'ElanManager', + 'LeanRepo', + 'LeanProjectSetup', + 'SetupConfig', + 'SetupResult', +] diff --git a/leanup/repo/elan.py b/leanup/repo/elan.py index cf034b2..67c4db1 100644 --- a/leanup/repo/elan.py +++ b/leanup/repo/elan.py @@ -156,15 +156,23 @@ def install_elan(self, force: bool = False) -> bool: return False def install_lean(self, version: str = None) -> bool: + requested = version or "stable" installed = self.get_installed_toolchains() - if version in installed: - logger.info(f"Lean toolchain {version} is already installed") + if self._is_toolchain_installed(requested, installed): + logger.info(f"Lean toolchain {requested} is already installed") return True - version = version or "stable" - cmd = ["toolchain", "install", version] + cmd = ["toolchain", "install", requested] result = self.proxy_elan_command(cmd) return result == 0 + def _is_toolchain_installed(self, requested: str, installed: List[str]) -> bool: + candidates = {requested} + if requested.startswith("v"): + candidates.add(f"leanprover/lean4:{requested}") + elif requested.startswith("leanprover/lean4:"): + candidates.add(requested.split(":", 1)[1]) + return any(toolchain in candidates for toolchain in installed) + def proxy_elan_command(self, args: List[str]) -> int: """Proxy execute elan command with streaming output""" if not self.elan_exe: diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py new file mode 100644 index 0000000..9af1774 --- /dev/null +++ b/leanup/repo/project_setup.py @@ -0,0 +1,207 @@ +from __future__ import annotations + +from dataclasses import dataclass +import os +from pathlib import Path +import re +import shutil + +from leanup.const import LEANUP_CACHE_DIR +from leanup.repo.elan import ElanManager +from leanup.repo.manager import LeanRepo +from leanup.utils.basic import working_directory +from leanup.utils.custom_logger import setup_logger + +logger = setup_logger("project_setup") + +LEAN_VERSION_PATTERN = re.compile(r"^v?4\.\d+\.\d+$") + + +def normalize_lean_version(version: str) -> str: + normalized = version.strip() + if not LEAN_VERSION_PATTERN.match(normalized): + raise ValueError("Lean version must look like v4.x.x or 4.x.x.") + if not normalized.startswith("v"): + normalized = f"v{normalized}" + return normalized + + +def sanitize_project_name(name: str) -> str: + sanitized = re.sub(r"[^A-Za-z0-9_]", "", name.strip()) + if not sanitized: + sanitized = "LeanProject" + if sanitized[0].isdigit(): + sanitized = f"Lean{sanitized}" + return sanitized + + +def remove_path(path: Path) -> None: + if not path.exists() and not path.is_symlink(): + return + if path.is_symlink() or path.is_file(): + path.unlink() + return + shutil.rmtree(path) + + +@dataclass +class SetupConfig: + target_dir: Path + lean_version: str + project_name: str | None = None + mathlib: bool = True + dependency_mode: str | None = None + force: bool = False + + def __post_init__(self) -> None: + self.target_dir = Path(self.target_dir).expanduser().resolve() + self.lean_version = normalize_lean_version(self.lean_version) + default_name = self.project_name or self.target_dir.name + self.project_name = sanitize_project_name(default_name) + + @property + def template(self) -> str: + return "math" if self.mathlib else "std" + + @property + def resolved_dependency_mode(self) -> str: + if self.dependency_mode: + return self.dependency_mode + if not self.mathlib: + return "build" + return "symlink" if self.mathlib_cache_dir.exists() else "build" + + @property + def toolchain(self) -> str: + return f"leanprover/lean4:{self.lean_version}" + + @property + def mathlib_cache_dir(self) -> Path: + return LEANUP_CACHE_DIR / "setup" / "mathlib" / self.lean_version / "packages" + + 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 == "symlink" and not self.mathlib: + raise ValueError("Dependency symlink mode is only available when mathlib is enabled.") + + +@dataclass +class SetupResult: + target_dir: Path + lean_version: str + mathlib: bool + dependency_mode: str + cache_dir: Path | None = None + used_cache: bool = False + + +class LeanProjectSetup: + def __init__(self, elan_manager: ElanManager | None = None): + self.elan_manager = elan_manager or ElanManager() + + def setup(self, config: SetupConfig) -> SetupResult: + config.validate() + self._ensure_target_available(config) + self._ensure_toolchain(config.lean_version) + + with working_directory() as temp_dir: + temp_root = LeanRepo(temp_dir) + stdout, stderr, returncode = temp_root.lake_init( + config.project_name, + config.template, + ) + if returncode != 0: + raise RuntimeError(stderr or stdout or "Failed to initialize Lean project.") + + project_dir = temp_dir / config.project_name + project = LeanRepo(project_dir) + self._write_toolchain(project_dir, config.toolchain) + + used_cache = False + cache_dir = config.mathlib_cache_dir if config.mathlib else None + + if config.mathlib and config.resolved_dependency_mode == "symlink": + self._link_mathlib_cache(config, project_dir) + used_cache = True + + if config.mathlib: + self._run_lake_update(project) + + self._run_lake_build(project) + + if config.mathlib and config.resolved_dependency_mode == "build": + self._refresh_mathlib_cache(config, project_dir) + + shutil.move(str(project_dir), str(config.target_dir)) + + return SetupResult( + target_dir=config.target_dir, + lean_version=config.lean_version, + mathlib=config.mathlib, + dependency_mode=config.resolved_dependency_mode, + cache_dir=cache_dir, + used_cache=used_cache, + ) + + def _ensure_target_available(self, config: SetupConfig) -> None: + target = config.target_dir + if target.exists() or target.is_symlink(): + if not config.force: + raise ValueError(f"Target directory already exists: {target}") + remove_path(target) + + target.parent.mkdir(parents=True, exist_ok=True) + + def _ensure_toolchain(self, version: str) -> None: + if not self.elan_manager.is_elan_installed() and not self.elan_manager.install_elan(): + raise RuntimeError("Failed to install elan.") + if not self.elan_manager.install_lean(version): + raise RuntimeError(f"Failed to install Lean toolchain {version}.") + + def _write_toolchain(self, project_dir: Path, toolchain: str) -> None: + (project_dir / "lean-toolchain").write_text(toolchain + "\n", encoding="utf-8") + + def _run_lake_update(self, repo: LeanRepo) -> None: + stdout, stderr, returncode = repo.lake_update() + if returncode != 0: + raise RuntimeError(stderr or stdout or "lake update failed.") + + def _run_lake_build(self, repo: LeanRepo) -> None: + stdout, stderr, returncode = repo.lake_build() + if returncode != 0: + raise RuntimeError(stderr or stdout or "lake build failed.") + + def _link_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: + cache_dir = config.mathlib_cache_dir + if not cache_dir.exists(): + raise ValueError( + "No cached mathlib packages found for this Lean version. " + "Run setup with --dependency-mode build first." + ) + + packages_dir = project_dir / ".lake" / "packages" + packages_dir.parent.mkdir(parents=True, exist_ok=True) + remove_path(packages_dir) + + try: + packages_dir.symlink_to(cache_dir, target_is_directory=True) + except OSError as exc: + raise RuntimeError(f"Failed to create dependency symlink: {exc}") from exc + + def _refresh_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: + source_dir = project_dir / ".lake" / "packages" + if not source_dir.exists(): + logger.warning("Skipping cache refresh because .lake/packages does not exist.") + return + + cache_dir = config.mathlib_cache_dir + cache_parent = cache_dir.parent + cache_parent.mkdir(parents=True, exist_ok=True) + + temp_cache_dir = cache_parent / f".{cache_dir.name}.tmp" + remove_path(temp_cache_dir) + shutil.copytree(source_dir, temp_cache_dir, symlinks=True) + + remove_path(cache_dir) + os.replace(temp_cache_dir, cache_dir) diff --git a/tests/test_elan_manager.py b/tests/test_elan_manager.py index 1a89bb6..73e5ffa 100644 --- a/tests/test_elan_manager.py +++ b/tests/test_elan_manager.py @@ -103,6 +103,27 @@ def test_download_installer_success(self, mock_get, mock_elan_home, temp_dir): assert result is True assert target_path.exists() + + def test_install_lean_skips_when_version_already_installed(self, mock_elan_home): + with patch.dict(os.environ, {'ELAN_HOME': str(mock_elan_home)}): + manager = ElanManager() + + with patch.object( + manager, + 'get_installed_toolchains', + return_value=['leanprover/lean4:v4.22.0', 'stable'], + ), patch.object(manager, 'proxy_elan_command') as mock_proxy: + assert manager.install_lean('v4.22.0') is True + mock_proxy.assert_not_called() + + def test_install_lean_installs_when_version_missing(self, mock_elan_home): + with patch.dict(os.environ, {'ELAN_HOME': str(mock_elan_home)}): + manager = ElanManager() + + with patch.object(manager, 'get_installed_toolchains', return_value=[]), \ + patch.object(manager, 'proxy_elan_command', return_value=0) as mock_proxy: + assert manager.install_lean('v4.22.0') is True + mock_proxy.assert_called_once_with(['toolchain', 'install', 'v4.22.0']) @patch('subprocess.run') @pytest.mark.skipif(OS_TYPE == 'Windows', reason="Windows path separator issue") @@ -145,4 +166,4 @@ def test_get_status_info_not_installed(self, mock_elan_home): assert info['installed'] is False assert info['version'] is None assert info['executable'] is None - assert info['toolchains'] == [] \ No newline at end of file + assert info['toolchains'] == [] diff --git a/tests/test_setup.py b/tests/test_setup.py new file mode 100644 index 0000000..44f1d9e --- /dev/null +++ b/tests/test_setup.py @@ -0,0 +1,248 @@ +from pathlib import Path + +from click.testing import CliRunner + +from leanup.cli import cli +from leanup.repo.project_setup import LeanProjectSetup, SetupConfig + + +def test_setup_command_rejects_symlink_without_mathlib(): + runner = CliRunner() + + result = runner.invoke( + cli, + [ + "setup", + "Demo", + "--lean-version", + "v4.27.0", + "--no-mathlib", + "--dependency-mode", + "symlink", + ], + ) + + assert result.exit_code != 0 + assert "only available when mathlib is enabled" in result.output + + +def test_setup_command_uses_expected_defaults(monkeypatch, tmp_path): + runner = CliRunner() + captured = {} + + def fake_setup(self, config): + captured["target_dir"] = config.target_dir + captured["lean_version"] = config.lean_version + captured["mathlib"] = config.mathlib + captured["dependency_mode"] = config.resolved_dependency_mode + return type( + "Result", + (), + { + "target_dir": config.target_dir, + "lean_version": config.lean_version, + "mathlib": config.mathlib, + "dependency_mode": config.resolved_dependency_mode, + "cache_dir": config.mathlib_cache_dir, + "used_cache": True, + }, + )() + + monkeypatch.setattr(LeanProjectSetup, "setup", fake_setup) + + target = tmp_path / "Demo" + result = runner.invoke(cli, ["setup", str(target), "--lean-version", "4.27.0"]) + + assert result.exit_code == 0 + assert captured["target_dir"] == target.resolve() + assert captured["lean_version"] == "v4.27.0" + assert captured["mathlib"] is True + assert captured["dependency_mode"] == "build" + + +def test_setup_interactive_uses_previewed_dependency_mode(monkeypatch, tmp_path): + import importlib + + setup_cli_module = importlib.import_module("leanup.cli.setup") + runner = CliRunner() + captured = {} + + def fake_setup(self, config): + captured["dependency_mode"] = config.resolved_dependency_mode + return type( + "Result", + (), + { + "target_dir": config.target_dir, + "lean_version": config.lean_version, + "mathlib": config.mathlib, + "dependency_mode": config.resolved_dependency_mode, + "cache_dir": config.mathlib_cache_dir, + "used_cache": False, + }, + )() + + monkeypatch.setattr( + setup_cli_module, + "resolve_interactive_mode", + lambda interactive, auto_prompt_condition: (None, True, False, True, True), + ) + values = iter([ + str(tmp_path / "Demo"), + "v4.27.0", + "Demo", + "build", + ]) + confirmations = iter([True, False]) + monkeypatch.setattr(setup_cli_module, "ask_text", lambda message, default="": next(values)) + monkeypatch.setattr(setup_cli_module, "ask_confirm", lambda message, default=True: next(confirmations)) + monkeypatch.setattr(LeanProjectSetup, "setup", fake_setup) + + result = runner.invoke(cli, ["setup"]) + + assert result.exit_code == 0 + assert captured["dependency_mode"] == "build" + + +def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): + from leanup.repo import project_setup as project_setup_module + + original_cache_dir = project_setup_module.LEANUP_CACHE_DIR + project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + config = SetupConfig(target_dir=tmp_path / "Demo", lean_version="v4.27.0") + assert config.resolved_dependency_mode == "build" + + config.mathlib_cache_dir.mkdir(parents=True, exist_ok=True) + assert config.resolved_dependency_mode == "symlink" + finally: + project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + + +def test_setup_build_mode_populates_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_update(self): + packages_dir = self.cwd / ".lake" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached mathlib\n", encoding="utf-8") + (self.cwd / "lake-manifest.json").write_text("{}\n", encoding="utf-8") + return "", "", 0 + + def fake_lake_build(self): + build_dir = self.cwd / ".lake" / "build" + build_dir.mkdir(parents=True, exist_ok=True) + return "", "", 0 + + from leanup.repo import project_setup as project_setup_module + + original_cache_dir = project_setup_module.LEANUP_CACHE_DIR + project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + from leanup.repo.manager import LeanRepo + + original_lake_init = LeanRepo.lake_init + original_lake_update = LeanRepo.lake_update + original_lake_build = LeanRepo.lake_build + LeanRepo.lake_init = fake_lake_init + LeanRepo.lake_update = fake_lake_update + LeanRepo.lake_build = fake_lake_build + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + target = tmp_path / "BuildDemo" + config = SetupConfig( + target_dir=target, + lean_version="v4.27.0", + dependency_mode="build", + ) + + result = manager.setup(config) + + assert result.used_cache is False + assert (target / "lean-toolchain").read_text(encoding="utf-8").strip() == "leanprover/lean4:v4.27.0" + assert config.mathlib_cache_dir.exists() + assert (config.mathlib_cache_dir / "mathlib" / "README.md").exists() + finally: + project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + LeanRepo.lake_init = original_lake_init + LeanRepo.lake_update = original_lake_update + LeanRepo.lake_build = original_lake_build + + +def test_setup_symlink_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_update(self): + packages_dir = self.cwd / ".lake" / "packages" + packages_dir.mkdir(parents=True, exist_ok=True) + (self.cwd / "lake-manifest.json").write_text("{}\n", encoding="utf-8") + return "", "", 0 + + def fake_lake_build(self): + return "", "", 0 + + from leanup.repo import project_setup as project_setup_module + + original_cache_dir = project_setup_module.LEANUP_CACHE_DIR + project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + from leanup.repo.manager import LeanRepo + + original_lake_init = LeanRepo.lake_init + original_lake_update = LeanRepo.lake_update + original_lake_build = LeanRepo.lake_build + LeanRepo.lake_init = fake_lake_init + LeanRepo.lake_update = fake_lake_update + LeanRepo.lake_build = fake_lake_build + + cached_packages = project_setup_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.27.0" / "packages" / "mathlib" + cached_packages.mkdir(parents=True, exist_ok=True) + (cached_packages / "README.md").write_text("cached\n", encoding="utf-8") + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + target = tmp_path / "SymlinkDemo" + config = SetupConfig(target_dir=target, lean_version="v4.27.0", dependency_mode="symlink") + + result = manager.setup(config) + + packages_link = target / ".lake" / "packages" + assert result.used_cache is True + assert packages_link.is_symlink() + assert packages_link.resolve() == config.mathlib_cache_dir + assert (packages_link / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cached" + finally: + project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + LeanRepo.lake_init = original_lake_init + LeanRepo.lake_update = original_lake_update + LeanRepo.lake_build = original_lake_build From 6b2d4b428826fe72771b9310c7377f3b2737f76c Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Tue, 7 Apr 2026 16:10:46 +0800 Subject: [PATCH 4/8] feat: add reusable mathlib cache commands --- README.md | 22 +++++ docs/getting-started/quickstart.md | 16 +++ docs/index.md | 1 + leanup/__init__.py | 3 +- leanup/cli/__init__.py | 2 + leanup/cli/mathlib.py | 100 +++++++++++++++++++ leanup/repo/__init__.py | 2 + leanup/repo/mathlib_cache.py | 153 +++++++++++++++++++++++++++++ leanup/repo/project_setup.py | 33 ++----- tests/test_mathlib_cache.py | 145 +++++++++++++++++++++++++++ tests/test_setup.py | 29 +++--- 11 files changed, 465 insertions(+), 41 deletions(-) create mode 100644 leanup/cli/mathlib.py create mode 100644 leanup/repo/mathlib_cache.py create mode 100644 tests/test_mathlib_cache.py diff --git a/README.md b/README.md index b4107ff..4b551cf 100644 --- a/README.md +++ b/README.md @@ -114,10 +114,32 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force - `--dependency-mode symlink` 只在启用 `mathlib` 时可用 - 默认缓存目录为 `LEANUP_CACHE_DIR/setup/mathlib//packages` +- 在当前 workspace 中，默认也会尝试从 `reference/Projects/cache//packages.tar.gz` 自动导入缓存 - 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 - 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 - `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装 +### 管理 mathlib 缓存 + +```bash +# 查看 LeanUp 已有缓存，以及 reference 中可导入的缓存 +leanup mathlib cache list + +# 只看本地已导入缓存 +leanup mathlib cache list --local-only + +# 只看可从 reference 导入的缓存 +leanup mathlib cache list --importable-only + +# 导入某个版本的 reference cache 到 LeanUp 默认缓存目录 +leanup mathlib cache import v4.22.0 + +# 一次性导入全部 reference cache +leanup mathlib cache import --all +``` + +如果需要覆盖 reference cache 来源目录，可以设置环境变量 `LEANUP_MATHLIB_CACHE_SOURCE`，或者在命令里传 `--source-dir`。 + ### 交互式安装 使用 `leanup repo install -i` 时，您可以配置： diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 478af8f..d4b0266 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -40,12 +40,28 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib - 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` - Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` +- 在当前 workspace 中，默认也会尝试从 `reference/Projects/cache//packages.tar.gz` 自动导入缓存 - `symlink` 模式只对 `mathlib` 项目开放 - 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 - 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 - `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装 - 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...` +### 管理 mathlib 缓存 + +```bash +# 查看 LeanUp 已有缓存，以及 reference 中可导入的缓存 +leanup mathlib cache list + +# 导入某个版本的 reference cache +leanup mathlib cache import v4.22.0 + +# 导入全部 reference cache +leanup mathlib cache import --all +``` + +如果需要覆盖 reference cache 来源目录，可以设置 `LEANUP_MATHLIB_CACHE_SOURCE`，或者传 `--source-dir`。 + ### 仓库管理 ```bash diff --git a/docs/index.md b/docs/index.md index 2de3f4f..dc64650 100644 --- a/docs/index.md +++ b/docs/index.md @@ -5,6 +5,7 @@ ## 功能特性 - `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存 +- `leanup mathlib cache ...`：查看和导入 mathlib 共享缓存 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 - `leanup repo list`：查看已安装仓库 diff --git a/leanup/__init__.py b/leanup/__init__.py index 9f20293..c88e01c 100644 --- a/leanup/__init__.py +++ b/leanup/__init__.py @@ -7,6 +7,7 @@ from .repo import ( RepoManager, ElanManager, + MathlibCacheManager, LeanRepo, LeanProjectSetup, SetupConfig, @@ -15,7 +16,7 @@ from .utils import setup_logger, execute_command, working_directory __all__ = [ - 'RepoManager', 'ElanManager', 'LeanRepo', + 'RepoManager', 'ElanManager', 'MathlibCacheManager', 'LeanRepo', 'LeanProjectSetup', 'SetupConfig', 'SetupResult', "setup_logger", "execute_command", "working_directory" ] diff --git a/leanup/cli/__init__.py b/leanup/cli/__init__.py index 76a79f1..568d605 100644 --- a/leanup/cli/__init__.py +++ b/leanup/cli/__init__.py @@ -2,6 +2,7 @@ import sys from leanup.utils.custom_logger import setup_logger +from leanup.cli.mathlib import mathlib from leanup.cli.repo import repo from leanup.cli.setup import setup_project from leanup.cli.elan_ops import ( @@ -42,6 +43,7 @@ def status(): cli.add_command(setup_project) +cli.add_command(mathlib) @cli.command(context_settings=dict(ignore_unknown_options=True)) diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py new file mode 100644 index 0000000..1add611 --- /dev/null +++ b/leanup/cli/mathlib.py @@ -0,0 +1,100 @@ +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") +@click.option( + "--local-only", + is_flag=True, + help="Show only caches already imported into LeanUp's cache directory.", +) +@click.option( + "--importable-only", + is_flag=True, + help="Show only versions that can be imported from the reference cache source.", +) +@click.option( + "--source-dir", + type=click.Path(path_type=Path, file_okay=False, dir_okay=True), + help="Override the reference cache directory to scan for packages.tar.gz archives.", +) +def list_cache(local_only: bool, importable_only: bool, source_dir: Path | None) -> None: + """List available mathlib caches.""" + manager = MathlibCacheManager() + entries = manager.list_entries(source_dir=source_dir) + + filtered = [] + for entry in entries: + if local_only and not entry.local_available: + continue + if importable_only and not entry.importable: + continue + filtered.append(entry) + + if not filtered: + click.echo("No mathlib caches found.") + return + + for entry in filtered: + status = [] + if entry.local_available: + status.append("local") + if entry.importable: + status.append("importable") + click.echo(f"{entry.version}\t{', '.join(status) or 'unavailable'}") + click.echo(f" local: {entry.local_path}") + if entry.archive_path: + click.echo(f" archive: {entry.archive_path}") + + +@cache.command(name="import") +@click.argument("version", required=False) +@click.option("--all", "import_all", is_flag=True, help="Import all importable cache archives.") +@click.option("--force", is_flag=True, help="Replace an existing imported cache.") +@click.option( + "--source-dir", + type=click.Path(path_type=Path, file_okay=False, dir_okay=True), + help="Override the reference cache directory containing versioned packages.tar.gz archives.", +) +def import_cache( + version: str | None, + import_all: bool, + force: bool, + source_dir: Path | None, +) -> None: + """Import mathlib package caches into LeanUp's default cache directory.""" + if import_all and version: + raise click.ClickException("Use either VERSION or --all, not both.") + if not import_all and not version: + raise click.ClickException("Missing VERSION. Use `leanup mathlib cache import ` or --all.") + + manager = MathlibCacheManager() + targets = [] + if import_all: + targets = [entry.version for entry in manager.list_entries(source_dir=source_dir) if entry.importable] + if not targets: + raise click.ClickException("No importable mathlib caches found.") + else: + targets = [normalize_lean_version(version)] + + for target in targets: + try: + packages_dir = manager.import_archive(target, source_dir=source_dir, force=force) + except ValueError as exc: + raise click.ClickException(str(exc)) from exc + click.echo(f"Imported {target} -> {packages_dir}") diff --git a/leanup/repo/__init__.py b/leanup/repo/__init__.py index 5099f6e..4061622 100644 --- a/leanup/repo/__init__.py +++ b/leanup/repo/__init__.py @@ -2,11 +2,13 @@ from .manager import RepoManager, LeanRepo from .elan import ElanManager +from .mathlib_cache import MathlibCacheManager from .project_setup import LeanProjectSetup, SetupConfig, SetupResult __all__ = [ 'RepoManager', 'ElanManager', + 'MathlibCacheManager', 'LeanRepo', 'LeanProjectSetup', 'SetupConfig', diff --git a/leanup/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py new file mode 100644 index 0000000..c37b11c --- /dev/null +++ b/leanup/repo/mathlib_cache.py @@ -0,0 +1,153 @@ +from __future__ import annotations + +from dataclasses import dataclass +from pathlib import Path +import os +import re +import shutil +import tarfile + +from leanup.const import LEANUP_CACHE_DIR +from leanup.utils.custom_logger import setup_logger + +logger = setup_logger("mathlib_cache") + +LEAN_VERSION_PATTERN = re.compile(r"^v?4\.\d+\.\d+$") + + +def normalize_lean_version(version: str) -> str: + normalized = version.strip() + if not LEAN_VERSION_PATTERN.match(normalized): + raise ValueError("Lean version must look like v4.x.x or 4.x.x.") + if not normalized.startswith("v"): + normalized = f"v{normalized}" + return normalized + + +def remove_path(path: Path) -> None: + if not path.exists() and not path.is_symlink(): + return + if path.is_symlink() or path.is_file(): + path.unlink() + return + shutil.rmtree(path) + + +@dataclass +class CacheEntry: + version: str + local_path: Path + archive_path: Path | None + + @property + def local_available(self) -> bool: + return self.local_path.exists() + + @property + def importable(self) -> bool: + return self.archive_path is not None and 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") + + def get_local_packages_dir(self, version: str) -> Path: + return self.cache_root / normalize_lean_version(version) / "packages" + + def discover_reference_cache_dir(self) -> Path | None: + explicit = os.getenv("LEANUP_MATHLIB_CACHE_SOURCE") + candidates = [] + if explicit: + candidates.append(Path(explicit).expanduser()) + + here = Path(__file__).resolve() + for parent in [Path.cwd().resolve(), *Path.cwd().resolve().parents, *here.parents]: + candidates.append(parent / "reference" / "Projects" / "cache") + + seen = set() + for candidate in candidates: + resolved = str(candidate) + if resolved in seen: + continue + seen.add(resolved) + if candidate.exists() and candidate.is_dir(): + return candidate + return None + + def get_reference_archive(self, version: str, source_dir: Path | None = None) -> Path | None: + normalized = normalize_lean_version(version) + source_root = source_dir or self.discover_reference_cache_dir() + if not source_root: + return None + archive = source_root / normalized / "packages.tar.gz" + return archive if archive.exists() else None + + def list_entries(self, source_dir: Path | None = None) -> list[CacheEntry]: + versions = set() + if self.cache_root.exists(): + for child in self.cache_root.iterdir(): + if child.is_dir() and LEAN_VERSION_PATTERN.match(child.name): + versions.add(normalize_lean_version(child.name)) + + reference_root = source_dir or self.discover_reference_cache_dir() + if reference_root and reference_root.exists(): + for child in reference_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), + archive_path=self.get_reference_archive(version, source_dir=source_dir), + ) + for version in sorted(versions) + ] + + def ensure_local_cache(self, version: str, source_dir: Path | None = None) -> Path | None: + local_path = self.get_local_packages_dir(version) + if local_path.exists(): + return local_path + archive = self.get_reference_archive(version, source_dir=source_dir) + if not archive: + return None + self.import_archive(version, archive) + return local_path + + def import_archive( + self, + version: str, + archive_path: Path | None = None, + source_dir: Path | None = None, + force: bool = False, + ) -> Path: + normalized = normalize_lean_version(version) + archive = archive_path or self.get_reference_archive(normalized, source_dir=source_dir) + if not archive: + raise ValueError(f"No reference cache archive found for {normalized}.") + + version_root = self.cache_root / normalized + packages_dir = version_root / "packages" + if packages_dir.exists(): + if not force: + return packages_dir + remove_path(packages_dir) + + version_root.mkdir(parents=True, exist_ok=True) + temp_root = version_root / ".importing" + remove_path(temp_root) + temp_root.mkdir(parents=True, exist_ok=True) + + try: + with tarfile.open(archive, "r:gz") as tar: + tar.extractall(path=temp_root, filter="data") + extracted_packages = temp_root / "packages" + if not extracted_packages.exists(): + raise ValueError(f"Archive {archive} does not contain a packages directory.") + remove_path(packages_dir) + os.replace(extracted_packages, packages_dir) + logger.info(f"Imported mathlib cache {normalized} from {archive}") + return packages_dir + finally: + remove_path(temp_root) diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py index 9af1774..1b89dae 100644 --- a/leanup/repo/project_setup.py +++ b/leanup/repo/project_setup.py @@ -6,25 +6,14 @@ import re import shutil -from leanup.const import LEANUP_CACHE_DIR from leanup.repo.elan import ElanManager +from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version, remove_path from leanup.repo.manager import LeanRepo from leanup.utils.basic import working_directory from leanup.utils.custom_logger import setup_logger logger = setup_logger("project_setup") -LEAN_VERSION_PATTERN = re.compile(r"^v?4\.\d+\.\d+$") - - -def normalize_lean_version(version: str) -> str: - normalized = version.strip() - if not LEAN_VERSION_PATTERN.match(normalized): - raise ValueError("Lean version must look like v4.x.x or 4.x.x.") - if not normalized.startswith("v"): - normalized = f"v{normalized}" - return normalized - def sanitize_project_name(name: str) -> str: sanitized = re.sub(r"[^A-Za-z0-9_]", "", name.strip()) @@ -35,15 +24,6 @@ def sanitize_project_name(name: str) -> str: return sanitized -def remove_path(path: Path) -> None: - if not path.exists() and not path.is_symlink(): - return - if path.is_symlink() or path.is_file(): - path.unlink() - return - shutil.rmtree(path) - - @dataclass class SetupConfig: target_dir: Path @@ -77,7 +57,7 @@ def toolchain(self) -> str: @property def mathlib_cache_dir(self) -> Path: - return LEANUP_CACHE_DIR / "setup" / "mathlib" / self.lean_version / "packages" + return MathlibCacheManager().get_local_packages_dir(self.lean_version) def validate(self) -> None: if self.resolved_dependency_mode not in {"symlink", "build"}: @@ -99,6 +79,7 @@ class SetupResult: class LeanProjectSetup: def __init__(self, elan_manager: ElanManager | None = None): self.elan_manager = elan_manager or ElanManager() + self.cache_manager = MathlibCacheManager() def setup(self, config: SetupConfig) -> SetupResult: config.validate() @@ -173,11 +154,11 @@ def _run_lake_build(self, repo: LeanRepo) -> None: raise RuntimeError(stderr or stdout or "lake build failed.") def _link_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: - cache_dir = config.mathlib_cache_dir - if not cache_dir.exists(): + cache_dir = self.cache_manager.ensure_local_cache(config.lean_version) + if not cache_dir: raise ValueError( "No cached mathlib packages found for this Lean version. " - "Run setup with --dependency-mode build first." + "Import one with `leanup mathlib cache import ` or run setup with --dependency-mode build first." ) packages_dir = project_dir / ".lake" / "packages" @@ -195,7 +176,7 @@ def _refresh_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None logger.warning("Skipping cache refresh because .lake/packages does not exist.") return - cache_dir = config.mathlib_cache_dir + cache_dir = self.cache_manager.get_local_packages_dir(config.lean_version) cache_parent = cache_dir.parent cache_parent.mkdir(parents=True, exist_ok=True) diff --git a/tests/test_mathlib_cache.py b/tests/test_mathlib_cache.py new file mode 100644 index 0000000..2147fc0 --- /dev/null +++ b/tests/test_mathlib_cache.py @@ -0,0 +1,145 @@ +from pathlib import Path +import tarfile + +from click.testing import CliRunner + +from leanup.cli import cli +from leanup.repo.mathlib_cache import MathlibCacheManager + + +def _write_reference_archive(root: Path, version: str) -> Path: + archive_dir = root / version + archive_dir.mkdir(parents=True, exist_ok=True) + staging = root / ".staging" / version / "packages" / "mathlib" + staging.mkdir(parents=True, exist_ok=True) + (staging / "README.md").write_text(f"cache for {version}\n", encoding="utf-8") + archive_path = archive_dir / "packages.tar.gz" + with tarfile.open(archive_path, "w:gz") as tar: + tar.add(staging.parent, arcname="packages") + return archive_path + + +def test_mathlib_cache_import_command(monkeypatch, tmp_path): + import importlib + + mathlib_cli_module = importlib.import_module("leanup.cli.mathlib") + cache_module = importlib.import_module("leanup.repo.mathlib_cache") + + runner = CliRunner() + source_dir = tmp_path / "reference-cache" + _write_reference_archive(source_dir, "v4.22.0") + + original_cache_root = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" + + try: + result = runner.invoke( + cli, + ["mathlib", "cache", "import", "v4.22.0", "--source-dir", str(source_dir)], + ) + + assert result.exit_code == 0 + local_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" + assert local_packages.exists() + assert (local_packages / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cache for v4.22.0" + finally: + cache_module.LEANUP_CACHE_DIR = original_cache_root + + +def test_mathlib_cache_list_command(monkeypatch, tmp_path): + import importlib + + cache_module = importlib.import_module("leanup.repo.mathlib_cache") + runner = CliRunner() + source_dir = tmp_path / "reference-cache" + _write_reference_archive(source_dir, "v4.22.0") + + original_cache_root = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" + + try: + local_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.21.0" / "packages" + (local_packages / "mathlib").mkdir(parents=True, exist_ok=True) + + result = runner.invoke( + cli, + ["mathlib", "cache", "list", "--source-dir", str(source_dir)], + ) + + assert result.exit_code == 0 + assert "v4.21.0" in result.output + assert "v4.22.0" in result.output + assert "local" in result.output + assert "importable" in result.output + finally: + cache_module.LEANUP_CACHE_DIR = original_cache_root + + +def test_setup_symlink_imports_reference_cache_when_available(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_update(self): + packages_dir = self.cwd / ".lake" / "packages" + packages_dir.mkdir(parents=True, exist_ok=True) + (self.cwd / "lake-manifest.json").write_text("{}\n", encoding="utf-8") + return "", "", 0 + + def fake_lake_build(self): + return "", "", 0 + + from leanup.repo import mathlib_cache as cache_module + from leanup.repo.manager import LeanRepo + from leanup.repo.project_setup import LeanProjectSetup, SetupConfig + + source_dir = tmp_path / "reference-cache" + _write_reference_archive(source_dir, "v4.22.0") + + original_cache_root = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" + original_source = cache_module.os.getenv("LEANUP_MATHLIB_CACHE_SOURCE") + original_lake_init = LeanRepo.lake_init + original_lake_update = LeanRepo.lake_update + original_lake_build = LeanRepo.lake_build + + try: + cache_module.os.environ["LEANUP_MATHLIB_CACHE_SOURCE"] = str(source_dir) + LeanRepo.lake_init = fake_lake_init + LeanRepo.lake_update = fake_lake_update + LeanRepo.lake_build = fake_lake_build + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + manager.cache_manager = MathlibCacheManager() + + target = tmp_path / "ImportedDemo" + config = SetupConfig(target_dir=target, lean_version="v4.22.0", dependency_mode="symlink") + + result = manager.setup(config) + + packages_link = target / ".lake" / "packages" + assert result.used_cache is True + assert packages_link.is_symlink() + assert packages_link.resolve() == config.mathlib_cache_dir + assert (packages_link / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cache for v4.22.0" + finally: + if original_source is None: + cache_module.os.environ.pop("LEANUP_MATHLIB_CACHE_SOURCE", None) + else: + cache_module.os.environ["LEANUP_MATHLIB_CACHE_SOURCE"] = original_source + cache_module.LEANUP_CACHE_DIR = original_cache_root + LeanRepo.lake_init = original_lake_init + LeanRepo.lake_update = original_lake_update + LeanRepo.lake_build = original_lake_build diff --git a/tests/test_setup.py b/tests/test_setup.py index 44f1d9e..2c9df46 100644 --- a/tests/test_setup.py +++ b/tests/test_setup.py @@ -105,19 +105,20 @@ def fake_setup(self, config): def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): - from leanup.repo import project_setup as project_setup_module + from leanup.repo.mathlib_cache import MathlibCacheManager + from leanup.repo import mathlib_cache as cache_module - original_cache_dir = project_setup_module.LEANUP_CACHE_DIR - project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" try: config = SetupConfig(target_dir=tmp_path / "Demo", lean_version="v4.27.0") assert config.resolved_dependency_mode == "build" - config.mathlib_cache_dir.mkdir(parents=True, exist_ok=True) + MathlibCacheManager().get_local_packages_dir("v4.27.0").mkdir(parents=True, exist_ok=True) assert config.resolved_dependency_mode == "symlink" finally: - project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + cache_module.LEANUP_CACHE_DIR = original_cache_dir def test_setup_build_mode_populates_shared_cache(tmp_path): @@ -149,10 +150,10 @@ def fake_lake_build(self): build_dir.mkdir(parents=True, exist_ok=True) return "", "", 0 - from leanup.repo import project_setup as project_setup_module + from leanup.repo import mathlib_cache as cache_module - original_cache_dir = project_setup_module.LEANUP_CACHE_DIR - project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" try: from leanup.repo.manager import LeanRepo @@ -179,7 +180,7 @@ def fake_lake_build(self): assert config.mathlib_cache_dir.exists() assert (config.mathlib_cache_dir / "mathlib" / "README.md").exists() finally: - project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + cache_module.LEANUP_CACHE_DIR = original_cache_dir LeanRepo.lake_init = original_lake_init LeanRepo.lake_update = original_lake_update LeanRepo.lake_build = original_lake_build @@ -211,10 +212,10 @@ def fake_lake_update(self): def fake_lake_build(self): return "", "", 0 - from leanup.repo import project_setup as project_setup_module + from leanup.repo import mathlib_cache as cache_module - original_cache_dir = project_setup_module.LEANUP_CACHE_DIR - project_setup_module.LEANUP_CACHE_DIR = tmp_path / "cache" + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" try: from leanup.repo.manager import LeanRepo @@ -226,7 +227,7 @@ def fake_lake_build(self): LeanRepo.lake_update = fake_lake_update LeanRepo.lake_build = fake_lake_build - cached_packages = project_setup_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.27.0" / "packages" / "mathlib" + cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.27.0" / "packages" / "mathlib" cached_packages.mkdir(parents=True, exist_ok=True) (cached_packages / "README.md").write_text("cached\n", encoding="utf-8") @@ -242,7 +243,7 @@ def fake_lake_build(self): assert packages_link.resolve() == config.mathlib_cache_dir assert (packages_link / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cached" finally: - project_setup_module.LEANUP_CACHE_DIR = original_cache_dir + cache_module.LEANUP_CACHE_DIR = original_cache_dir LeanRepo.lake_init = original_lake_init LeanRepo.lake_update = original_lake_update LeanRepo.lake_build = original_lake_build From 64b73ea131043d60d771b62942c39fb5d8480600 Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Tue, 7 Apr 2026 22:22:49 +0800 Subject: [PATCH 5/8] feat: streamline mathlib setup and cache tooling --- README.md | 22 +-- docs/getting-started/quickstart.md | 16 +- docs/index.md | 2 +- leanup/cli/mathlib.py | 98 +++------- leanup/repo/mathlib_cache.py | 107 +++------- leanup/repo/project_setup.py | 127 +++++++++--- .../manifests/v4.14.0/lake-manifest.json | 95 +++++++++ .../manifests/v4.17.0/lake-manifest.json | 95 +++++++++ .../manifests/v4.19.0/lake-manifest.json | 95 +++++++++ .../manifests/v4.21.0/lake-manifest.json | 95 +++++++++ .../manifests/v4.22.0/lake-manifest.json | 95 +++++++++ .../manifests/v4.27.0/lake-manifest.json | 95 +++++++++ .../templates/mathlib/v4.xx.0/Basic.lean.tmpl | 1 + .../templates/mathlib/v4.xx.0/README.md.tmpl | 1 + .../mathlib/v4.xx.0/lakefile.lean.tmpl | 12 ++ .../templates/mathlib/v4.xx.0/root.lean.tmpl | 3 + tests/test_mathlib_cache.py | 145 -------------- tests/test_mathlib_cache_cli.py | 37 ++++ tests/test_setup.py | 185 +++++++++++++++++- 19 files changed, 971 insertions(+), 355 deletions(-) create mode 100644 leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json create mode 100644 leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl create mode 100644 leanup/templates/mathlib/v4.xx.0/README.md.tmpl create mode 100644 leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl create mode 100644 leanup/templates/mathlib/v4.xx.0/root.lean.tmpl delete mode 100644 tests/test_mathlib_cache.py create mode 100644 tests/test_mathlib_cache_cli.py diff --git a/README.md b/README.md index 4b551cf..22b16a6 100644 --- a/README.md +++ b/README.md @@ -114,32 +114,20 @@ leanup setup ./Demo --lean-version v4.27.0 --name MyDemo --force - `--dependency-mode symlink` 只在启用 `mathlib` 时可用 - 默认缓存目录为 `LEANUP_CACHE_DIR/setup/mathlib//packages` -- 在当前 workspace 中，默认也会尝试从 `reference/Projects/cache//packages.tar.gz` 自动导入缓存 -- 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 -- 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 +- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 - `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装 ### 管理 mathlib 缓存 ```bash -# 查看 LeanUp 已有缓存，以及 reference 中可导入的缓存 +# 查看 LeanUp 已有缓存版本 leanup mathlib cache list -# 只看本地已导入缓存 -leanup mathlib cache list --local-only - -# 只看可从 reference 导入的缓存 -leanup mathlib cache list --importable-only - -# 导入某个版本的 reference cache 到 LeanUp 默认缓存目录 -leanup mathlib cache import v4.22.0 - -# 一次性导入全部 reference cache -leanup mathlib cache import --all +# 进入一个 Lean 仓库后，把当前仓库的 .lake/packages 打包到指定目录 +cd /path/to/repo +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache ``` -如果需要覆盖 reference cache 来源目录，可以设置环境变量 `LEANUP_MATHLIB_CACHE_SOURCE`，或者在命令里传 `--source-dir`。 - ### 交互式安装 使用 `leanup repo install -i` 时，您可以配置： diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index d4b0266..72bd6ff 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -40,28 +40,22 @@ leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib - 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` - Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` -- 在当前 workspace 中，默认也会尝试从 `reference/Projects/cache//packages.tar.gz` 自动导入缓存 - `symlink` 模式只对 `mathlib` 项目开放 -- 默认行为是：有缓存就复用，没有缓存就自动构建并刷新缓存 -- 显式指定 `--dependency-mode symlink` 时，如果当前版本还没有缓存，会直接报错 +- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 - `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装 - 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...` ### 管理 mathlib 缓存 ```bash -# 查看 LeanUp 已有缓存，以及 reference 中可导入的缓存 +# 查看 LeanUp 已有缓存版本 leanup mathlib cache list -# 导入某个版本的 reference cache -leanup mathlib cache import v4.22.0 - -# 导入全部 reference cache -leanup mathlib cache import --all +# 进入当前仓库后，打包本仓库的 .lake/packages 到指定目录 +cd /path/to/repo +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache ``` -如果需要覆盖 reference cache 来源目录，可以设置 `LEANUP_MATHLIB_CACHE_SOURCE`，或者传 `--source-dir`。 - ### 仓库管理 ```bash diff --git a/docs/index.md b/docs/index.md index dc64650..5a6d87c 100644 --- a/docs/index.md +++ b/docs/index.md @@ -5,7 +5,7 @@ ## 功能特性 - `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存 -- `leanup mathlib cache ...`：查看和导入 mathlib 共享缓存 +- `leanup mathlib cache list`：查看本地 mathlib 共享缓存版本 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 - `leanup repo list`：查看已安装仓库 diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py index 1add611..121dede 100644 --- a/leanup/cli/mathlib.py +++ b/leanup/cli/mathlib.py @@ -18,83 +18,47 @@ def cache() -> None: @cache.command(name="list") -@click.option( - "--local-only", - is_flag=True, - help="Show only caches already imported into LeanUp's cache directory.", -) -@click.option( - "--importable-only", - is_flag=True, - help="Show only versions that can be imported from the reference cache source.", -) -@click.option( - "--source-dir", - type=click.Path(path_type=Path, file_okay=False, dir_okay=True), - help="Override the reference cache directory to scan for packages.tar.gz archives.", -) -def list_cache(local_only: bool, importable_only: bool, source_dir: Path | None) -> None: +def list_cache() -> None: """List available mathlib caches.""" manager = MathlibCacheManager() - entries = manager.list_entries(source_dir=source_dir) - - filtered = [] - for entry in entries: - if local_only and not entry.local_available: - continue - if importable_only and not entry.importable: - continue - filtered.append(entry) + entries = manager.list_entries() - if not filtered: + if not entries: click.echo("No mathlib caches found.") return - for entry in filtered: - status = [] - if entry.local_available: - status.append("local") - if entry.importable: - status.append("importable") - click.echo(f"{entry.version}\t{', '.join(status) or 'unavailable'}") - click.echo(f" local: {entry.local_path}") - if entry.archive_path: - click.echo(f" archive: {entry.archive_path}") + for entry in entries: + click.echo(entry.version) -@cache.command(name="import") -@click.argument("version", required=False) -@click.option("--all", "import_all", is_flag=True, help="Import all importable cache archives.") -@click.option("--force", is_flag=True, help="Replace an existing imported cache.") +@cache.command(name="pack") @click.option( - "--source-dir", + "--repo-dir", type=click.Path(path_type=Path, file_okay=False, dir_okay=True), - help="Override the reference cache directory containing versioned packages.tar.gz archives.", + default=Path.cwd, + help="Lean repository directory containing .lake/packages.", ) -def import_cache( - version: str | None, - import_all: bool, - force: bool, - source_dir: Path | None, -) -> None: - """Import mathlib package caches into LeanUp's default cache directory.""" - if import_all and version: - raise click.ClickException("Use either VERSION or --all, not both.") - if not import_all and not version: - raise click.ClickException("Missing VERSION. Use `leanup mathlib cache import ` or --all.") - +@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.", +) +def pack_cache(repo_dir: Path, output_dir: Path, lean_version: str) -> None: + """Pack current repository .lake/packages into a versioned cache archive.""" manager = MathlibCacheManager() - targets = [] - if import_all: - targets = [entry.version for entry in manager.list_entries(source_dir=source_dir) if entry.importable] - if not targets: - raise click.ClickException("No importable mathlib caches found.") - else: - targets = [normalize_lean_version(version)] + 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) + except ValueError as exc: + raise click.ClickException(str(exc)) from exc - for target in targets: - try: - packages_dir = manager.import_archive(target, source_dir=source_dir, force=force) - except ValueError as exc: - raise click.ClickException(str(exc)) from exc - click.echo(f"Imported {target} -> {packages_dir}") + click.echo(str(packed)) diff --git a/leanup/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py index c37b11c..390991d 100644 --- a/leanup/repo/mathlib_cache.py +++ b/leanup/repo/mathlib_cache.py @@ -2,7 +2,6 @@ from dataclasses import dataclass from pathlib import Path -import os import re import shutil import tarfile @@ -37,16 +36,11 @@ def remove_path(path: Path) -> None: class CacheEntry: version: str local_path: Path - archive_path: Path | None @property def local_available(self) -> bool: return self.local_path.exists() - @property - def importable(self) -> bool: - return self.archive_path is not None and self.archive_path.exists() - class MathlibCacheManager: def __init__(self, cache_root: Path | None = None): @@ -55,99 +49,54 @@ def __init__(self, cache_root: Path | None = None): def get_local_packages_dir(self, version: str) -> Path: return self.cache_root / normalize_lean_version(version) / "packages" - def discover_reference_cache_dir(self) -> Path | None: - explicit = os.getenv("LEANUP_MATHLIB_CACHE_SOURCE") - candidates = [] - if explicit: - candidates.append(Path(explicit).expanduser()) - - here = Path(__file__).resolve() - for parent in [Path.cwd().resolve(), *Path.cwd().resolve().parents, *here.parents]: - candidates.append(parent / "reference" / "Projects" / "cache") - - seen = set() - for candidate in candidates: - resolved = str(candidate) - if resolved in seen: - continue - seen.add(resolved) - if candidate.exists() and candidate.is_dir(): - return candidate - return None - - def get_reference_archive(self, version: str, source_dir: Path | None = None) -> Path | None: - normalized = normalize_lean_version(version) - source_root = source_dir or self.discover_reference_cache_dir() - if not source_root: - return None - archive = source_root / normalized / "packages.tar.gz" - return archive if archive.exists() else None - - def list_entries(self, source_dir: Path | None = None) -> list[CacheEntry]: + def list_entries(self) -> list[CacheEntry]: versions = set() if self.cache_root.exists(): for child in self.cache_root.iterdir(): if child.is_dir() and LEAN_VERSION_PATTERN.match(child.name): versions.add(normalize_lean_version(child.name)) - reference_root = source_dir or self.discover_reference_cache_dir() - if reference_root and reference_root.exists(): - for child in reference_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), - archive_path=self.get_reference_archive(version, source_dir=source_dir), ) for version in sorted(versions) ] - def ensure_local_cache(self, version: str, source_dir: Path | None = None) -> Path | None: + def ensure_local_cache(self, version: str) -> Path | None: local_path = self.get_local_packages_dir(version) if local_path.exists(): return local_path - archive = self.get_reference_archive(version, source_dir=source_dir) - if not archive: - return None - self.import_archive(version, archive) - return local_path - - def import_archive( - self, - version: str, - archive_path: Path | None = None, - source_dir: Path | None = None, - force: bool = False, - ) -> Path: - normalized = normalize_lean_version(version) - archive = archive_path or self.get_reference_archive(normalized, source_dir=source_dir) - if not archive: - raise ValueError(f"No reference cache archive found for {normalized}.") + return 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 packages_dir = version_root / "packages" - if packages_dir.exists(): - if not force: - return packages_dir - remove_path(packages_dir) + if packages_dir.exists() and not force: + return packages_dir version_root.mkdir(parents=True, exist_ok=True) - temp_root = version_root / ".importing" + temp_root = version_root / ".packages.tmp" remove_path(temp_root) - temp_root.mkdir(parents=True, exist_ok=True) - - try: - with tarfile.open(archive, "r:gz") as tar: - tar.extractall(path=temp_root, filter="data") - extracted_packages = temp_root / "packages" - if not extracted_packages.exists(): - raise ValueError(f"Archive {archive} does not contain a packages directory.") - remove_path(packages_dir) - os.replace(extracted_packages, packages_dir) - logger.info(f"Imported mathlib cache {normalized} from {archive}") - return packages_dir - finally: - remove_path(temp_root) + shutil.copytree(source_dir, temp_root, symlinks=True) + + remove_path(packages_dir) + temp_root.replace(packages_dir) + logger.info(f"Refreshed mathlib cache {normalized} from {source_dir}") + return packages_dir + + def pack_packages_archive(self, packages_dir: Path, output_file: Path) -> Path: + if not packages_dir.exists() or not packages_dir.is_dir(): + raise ValueError(f"Packages directory not found: {packages_dir}") + + output_file.parent.mkdir(parents=True, exist_ok=True) + if output_file.exists(): + output_file.unlink() + + with tarfile.open(output_file, "w:gz", dereference=False) as tar: + tar.add(packages_dir, arcname="packages", recursive=True) + + logger.info(f"Packed {packages_dir} -> {output_file}") + return output_file diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py index 1b89dae..1cd2ba1 100644 --- a/leanup/repo/project_setup.py +++ b/leanup/repo/project_setup.py @@ -1,10 +1,11 @@ from __future__ import annotations from dataclasses import dataclass -import os +import json from pathlib import Path import re import shutil +import tempfile from leanup.repo.elan import ElanManager from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version, remove_path @@ -13,6 +14,8 @@ from leanup.utils.custom_logger import setup_logger logger = setup_logger("project_setup") +TEMPLATE_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" / "v4.xx.0" +BUNDLED_MANIFEST_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" / "manifests" def sanitize_project_name(name: str) -> str: @@ -49,7 +52,7 @@ def resolved_dependency_mode(self) -> str: return self.dependency_mode if not self.mathlib: return "build" - return "symlink" if self.mathlib_cache_dir.exists() else "build" + return "symlink" @property def toolchain(self) -> str: @@ -87,32 +90,28 @@ def setup(self, config: SetupConfig) -> SetupResult: self._ensure_toolchain(config.lean_version) with working_directory() as temp_dir: - temp_root = LeanRepo(temp_dir) - stdout, stderr, returncode = temp_root.lake_init( - config.project_name, - config.template, - ) - if returncode != 0: - raise RuntimeError(stderr or stdout or "Failed to initialize Lean project.") - project_dir = temp_dir / config.project_name + self._create_project_skeleton(config, project_dir) project = LeanRepo(project_dir) self._write_toolchain(project_dir, config.toolchain) + self._copy_reference_manifest(config, project_dir) used_cache = False cache_dir = config.mathlib_cache_dir if config.mathlib else None if config.mathlib and config.resolved_dependency_mode == "symlink": - self._link_mathlib_cache(config, project_dir) - used_cache = True + used_cache = self._prepare_mathlib_cache(config, project_dir) - if config.mathlib: + if config.mathlib and self._should_run_lake_update(config, project_dir): self._run_lake_update(project) + self._run_lake_cache_get(project) + self._refresh_mathlib_cache(config, project_dir) + if config.resolved_dependency_mode == "symlink": + self._link_mathlib_cache(config, project_dir) + used_cache = True self._run_lake_build(project) - - if config.mathlib and config.resolved_dependency_mode == "build": - self._refresh_mathlib_cache(config, project_dir) + self._verify_mathlib_project(project_dir) shutil.move(str(project_dir), str(config.target_dir)) @@ -140,6 +139,60 @@ def _ensure_toolchain(self, version: str) -> None: if not self.elan_manager.install_lean(version): raise RuntimeError(f"Failed to install Lean toolchain {version}.") + def _create_project_skeleton(self, config: SetupConfig, project_dir: Path) -> None: + project_dir.mkdir(parents=True, exist_ok=True) + if config.mathlib: + self._render_mathlib_template(config, project_dir) + return + + repo = LeanRepo(project_dir) + stdout, stderr, returncode = repo.lake_init(config.project_name, config.template) + if returncode != 0: + raise RuntimeError(stderr or stdout or "Failed to initialize Lean project.") + + def _render_mathlib_template(self, config: SetupConfig, project_dir: Path) -> None: + context = { + "project_name": config.project_name, + "lean_version": config.lean_version, + } + templates = { + "README.md.tmpl": project_dir / "README.md", + "lakefile.lean.tmpl": project_dir / "lakefile.lean", + "root.lean.tmpl": project_dir / f"{config.project_name}.lean", + "Basic.lean.tmpl": project_dir / config.project_name / "Basic.lean", + } + for template_name, output_path in templates.items(): + content = (TEMPLATE_ROOT / template_name).read_text(encoding="utf-8") + output_path.parent.mkdir(parents=True, exist_ok=True) + output_path.write_text(content.format(**context), encoding="utf-8") + + def _bundled_manifest_path(self, version: str) -> Path | None: + candidate = BUNDLED_MANIFEST_ROOT / normalize_lean_version(version) / "lake-manifest.json" + if candidate.exists(): + return candidate + return None + + def _copy_reference_manifest(self, config: SetupConfig, project_dir: Path) -> None: + if not config.mathlib: + return + bundled_manifest = self._bundled_manifest_path(config.lean_version) + if bundled_manifest: + manifest_path = project_dir / "lake-manifest.json" + shutil.copy2(bundled_manifest, manifest_path) + self._rewrite_manifest_name(manifest_path, config.project_name) + + def _rewrite_manifest_name(self, manifest_path: Path, project_name: str) -> None: + manifest = json.loads(manifest_path.read_text(encoding="utf-8")) + manifest["name"] = project_name + manifest_path.write_text(json.dumps(manifest, indent=1) + "\n", encoding="utf-8") + + def _should_run_lake_update(self, config: SetupConfig, project_dir: Path) -> bool: + if not config.mathlib: + return False + manifest = project_dir / "lake-manifest.json" + packages = project_dir / ".lake" / "packages" + return not (manifest.exists() and packages.exists()) + def _write_toolchain(self, project_dir: Path, toolchain: str) -> None: (project_dir / "lean-toolchain").write_text(toolchain + "\n", encoding="utf-8") @@ -148,18 +201,39 @@ def _run_lake_update(self, repo: LeanRepo) -> None: if returncode != 0: raise RuntimeError(stderr or stdout or "lake update failed.") + def _run_lake_cache_get(self, repo: LeanRepo) -> None: + stdout, stderr, returncode = repo.lake(["exe", "cache", "get"]) + if returncode != 0: + raise RuntimeError(stderr or stdout or "lake exe cache get failed.") + def _run_lake_build(self, repo: LeanRepo) -> None: stdout, stderr, returncode = repo.lake_build() if returncode != 0: raise RuntimeError(stderr or stdout or "lake build failed.") - def _link_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None: + def _verify_mathlib_project(self, project_dir: Path) -> None: + with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False, encoding="utf-8") as handle: + handle.write("import Mathlib.Init\n#eval Lean.versionString\n") + probe = Path(handle.name) + try: + repo = LeanRepo(project_dir) + stdout, stderr, returncode = repo.lake_env_lean(probe, json=False) + if returncode != 0: + raise RuntimeError(stderr or stdout or "verification failed.") + finally: + if probe.exists(): + probe.unlink() + + def _prepare_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> bool: cache_dir = self.cache_manager.ensure_local_cache(config.lean_version) if not cache_dir: - raise ValueError( - "No cached mathlib packages found for this Lean version. " - "Import one with `leanup mathlib cache import ` or run setup with --dependency-mode build first." - ) + return False + + self._link_mathlib_cache(config, project_dir) + return True + + def _link_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) @@ -176,13 +250,4 @@ def _refresh_mathlib_cache(self, config: SetupConfig, project_dir: Path) -> None logger.warning("Skipping cache refresh because .lake/packages does not exist.") return - cache_dir = self.cache_manager.get_local_packages_dir(config.lean_version) - cache_parent = cache_dir.parent - cache_parent.mkdir(parents=True, exist_ok=True) - - temp_cache_dir = cache_parent / f".{cache_dir.name}.tmp" - remove_path(temp_cache_dir) - shutil.copytree(source_dir, temp_cache_dir, symlinks=True) - - remove_path(cache_dir) - os.replace(temp_cache_dir, cache_dir) + self.cache_manager.refresh_local_cache(config.lean_version, source_dir) diff --git a/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json new file mode 100644 index 0000000..efa9181 --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "68280daef58803f68368eb2e53046dabcd270c9d", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.47", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json new file mode 100644 index 0000000..4c9e941 --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5269898d6a51d047931107c8d72d934d8d5d3753", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.17.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c708be04267e3e995a14ac0d08b1530579c1525a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.52", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json new file mode 100644 index 0000000..231ea65 --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c44e0c8ee63ca166450922a373c7409c5d26b00b", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.19.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "77e08eddc486491d7b9e470926b3dbe50319451a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e6a9f0f5ee3ccf7443a0070f92b62f8db12ae82b", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c4919189477c3221e6a204008998b0d724f49904", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.57", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f5d04a9c4973d401c8c92500711518f7c656f034", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "02dbd02bc00ec4916e99b04b2245b30200e200d0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json new file mode 100644 index 0000000..b1363cf --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "308445d7985027f538e281e18df29ca16ede2ba3", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.21.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c4aa78186d388e50a436e8362b947bae125a2933", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.62", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8ff27701d003456fd59f13a9212431239d902aef", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json new file mode 100644 index 0000000..19c996c --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "eb164a46de87078f27640ee71e6c3841defc2484", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.68", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "240676e9568c254a69be94801889d4b13f3b249f", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.22.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json new file mode 100644 index 0000000..6769981 --- /dev/null +++ b/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c04225ee7c0585effbd933662b3151f01b600e40", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.85", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "lean4web", + "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl b/leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl @@ -0,0 +1 @@ +def hello := "world" diff --git a/leanup/templates/mathlib/v4.xx.0/README.md.tmpl b/leanup/templates/mathlib/v4.xx.0/README.md.tmpl new file mode 100644 index 0000000..1ec9149 --- /dev/null +++ b/leanup/templates/mathlib/v4.xx.0/README.md.tmpl @@ -0,0 +1 @@ +# {project_name} diff --git a/leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl b/leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl new file mode 100644 index 0000000..951a48e --- /dev/null +++ b/leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl @@ -0,0 +1,12 @@ +import Lake +open Lake DSL + +package «{project_name}» where + -- add any additional package configuration options here + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "{lean_version}" + +@[default_target] +lean_lib «{project_name}» where + -- add any library configuration options here diff --git a/leanup/templates/mathlib/v4.xx.0/root.lean.tmpl b/leanup/templates/mathlib/v4.xx.0/root.lean.tmpl new file mode 100644 index 0000000..b081467 --- /dev/null +++ b/leanup/templates/mathlib/v4.xx.0/root.lean.tmpl @@ -0,0 +1,3 @@ +-- This module serves as the root of the `{project_name}` library. +-- Import modules here that should be built as part of the library. +import {project_name}.Basic diff --git a/tests/test_mathlib_cache.py b/tests/test_mathlib_cache.py deleted file mode 100644 index 2147fc0..0000000 --- a/tests/test_mathlib_cache.py +++ /dev/null @@ -1,145 +0,0 @@ -from pathlib import Path -import tarfile - -from click.testing import CliRunner - -from leanup.cli import cli -from leanup.repo.mathlib_cache import MathlibCacheManager - - -def _write_reference_archive(root: Path, version: str) -> Path: - archive_dir = root / version - archive_dir.mkdir(parents=True, exist_ok=True) - staging = root / ".staging" / version / "packages" / "mathlib" - staging.mkdir(parents=True, exist_ok=True) - (staging / "README.md").write_text(f"cache for {version}\n", encoding="utf-8") - archive_path = archive_dir / "packages.tar.gz" - with tarfile.open(archive_path, "w:gz") as tar: - tar.add(staging.parent, arcname="packages") - return archive_path - - -def test_mathlib_cache_import_command(monkeypatch, tmp_path): - import importlib - - mathlib_cli_module = importlib.import_module("leanup.cli.mathlib") - cache_module = importlib.import_module("leanup.repo.mathlib_cache") - - runner = CliRunner() - source_dir = tmp_path / "reference-cache" - _write_reference_archive(source_dir, "v4.22.0") - - original_cache_root = cache_module.LEANUP_CACHE_DIR - cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" - - try: - result = runner.invoke( - cli, - ["mathlib", "cache", "import", "v4.22.0", "--source-dir", str(source_dir)], - ) - - assert result.exit_code == 0 - local_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" - assert local_packages.exists() - assert (local_packages / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cache for v4.22.0" - finally: - cache_module.LEANUP_CACHE_DIR = original_cache_root - - -def test_mathlib_cache_list_command(monkeypatch, tmp_path): - import importlib - - cache_module = importlib.import_module("leanup.repo.mathlib_cache") - runner = CliRunner() - source_dir = tmp_path / "reference-cache" - _write_reference_archive(source_dir, "v4.22.0") - - original_cache_root = cache_module.LEANUP_CACHE_DIR - cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" - - try: - local_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.21.0" / "packages" - (local_packages / "mathlib").mkdir(parents=True, exist_ok=True) - - result = runner.invoke( - cli, - ["mathlib", "cache", "list", "--source-dir", str(source_dir)], - ) - - assert result.exit_code == 0 - assert "v4.21.0" in result.output - assert "v4.22.0" in result.output - assert "local" in result.output - assert "importable" in result.output - finally: - cache_module.LEANUP_CACHE_DIR = original_cache_root - - -def test_setup_symlink_imports_reference_cache_when_available(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_update(self): - packages_dir = self.cwd / ".lake" / "packages" - packages_dir.mkdir(parents=True, exist_ok=True) - (self.cwd / "lake-manifest.json").write_text("{}\n", encoding="utf-8") - return "", "", 0 - - def fake_lake_build(self): - return "", "", 0 - - from leanup.repo import mathlib_cache as cache_module - from leanup.repo.manager import LeanRepo - from leanup.repo.project_setup import LeanProjectSetup, SetupConfig - - source_dir = tmp_path / "reference-cache" - _write_reference_archive(source_dir, "v4.22.0") - - original_cache_root = cache_module.LEANUP_CACHE_DIR - cache_module.LEANUP_CACHE_DIR = tmp_path / "leanup-cache" - original_source = cache_module.os.getenv("LEANUP_MATHLIB_CACHE_SOURCE") - original_lake_init = LeanRepo.lake_init - original_lake_update = LeanRepo.lake_update - original_lake_build = LeanRepo.lake_build - - try: - cache_module.os.environ["LEANUP_MATHLIB_CACHE_SOURCE"] = str(source_dir) - LeanRepo.lake_init = fake_lake_init - LeanRepo.lake_update = fake_lake_update - LeanRepo.lake_build = fake_lake_build - - manager = LeanProjectSetup(elan_manager=FakeElanManager()) - manager.cache_manager = MathlibCacheManager() - - target = tmp_path / "ImportedDemo" - config = SetupConfig(target_dir=target, lean_version="v4.22.0", dependency_mode="symlink") - - result = manager.setup(config) - - packages_link = target / ".lake" / "packages" - assert result.used_cache is True - assert packages_link.is_symlink() - assert packages_link.resolve() == config.mathlib_cache_dir - assert (packages_link / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cache for v4.22.0" - finally: - if original_source is None: - cache_module.os.environ.pop("LEANUP_MATHLIB_CACHE_SOURCE", None) - else: - cache_module.os.environ["LEANUP_MATHLIB_CACHE_SOURCE"] = original_source - cache_module.LEANUP_CACHE_DIR = original_cache_root - LeanRepo.lake_init = original_lake_init - LeanRepo.lake_update = original_lake_update - LeanRepo.lake_build = original_lake_build diff --git a/tests/test_mathlib_cache_cli.py b/tests/test_mathlib_cache_cli.py new file mode 100644 index 0000000..6165dbc --- /dev/null +++ b/tests/test_mathlib_cache_cli.py @@ -0,0 +1,37 @@ +from pathlib import Path +import tarfile + +from click.testing import CliRunner + +from leanup.cli import cli + + +def test_mathlib_cache_pack_archives_current_repo(tmp_path): + runner = CliRunner() + repo_dir = tmp_path / "Demo" + packages_dir = repo_dir / ".lake" / "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", + ], + ) + + archive = output_dir / "v4.22.0" / "packages.tar.gz" + assert result.exit_code == 0 + assert archive.exists() + with tarfile.open(archive, "r:gz") as tar: + names = tar.getnames() + assert "packages/mathlib/README.md" in names diff --git a/tests/test_setup.py b/tests/test_setup.py index 2c9df46..0ad224a 100644 --- a/tests/test_setup.py +++ b/tests/test_setup.py @@ -1,3 +1,4 @@ +import os from pathlib import Path from click.testing import CliRunner @@ -57,7 +58,7 @@ def fake_setup(self, config): assert captured["target_dir"] == target.resolve() assert captured["lean_version"] == "v4.27.0" assert captured["mathlib"] is True - assert captured["dependency_mode"] == "build" + assert captured["dependency_mode"] == "symlink" def test_setup_interactive_uses_previewed_dependency_mode(monkeypatch, tmp_path): @@ -91,7 +92,7 @@ def fake_setup(self, config): str(tmp_path / "Demo"), "v4.27.0", "Demo", - "build", + "symlink", ]) confirmations = iter([True, False]) monkeypatch.setattr(setup_cli_module, "ask_text", lambda message, default="": next(values)) @@ -101,7 +102,7 @@ def fake_setup(self, config): result = runner.invoke(cli, ["setup"]) assert result.exit_code == 0 - assert captured["dependency_mode"] == "build" + assert captured["dependency_mode"] == "symlink" def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): @@ -113,7 +114,7 @@ def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): try: config = SetupConfig(target_dir=tmp_path / "Demo", lean_version="v4.27.0") - assert config.resolved_dependency_mode == "build" + assert config.resolved_dependency_mode == "symlink" MathlibCacheManager().get_local_packages_dir("v4.27.0").mkdir(parents=True, exist_ok=True) assert config.resolved_dependency_mode == "symlink" @@ -150,6 +151,18 @@ def fake_lake_build(self): build_dir.mkdir(parents=True, exist_ok=True) return "", "", 0 + def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): + assert Path(filepath).suffix == ".lean" + return "4.27.0\n", "", 0 + + def fake_lake(self, args): + if args == ["exe", "cache", "get"]: + packages_dir = self.cwd / ".lake" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached from cache get\n", encoding="utf-8") + return "", "", 0 + raise AssertionError(f"unexpected lake args: {args}") + from leanup.repo import mathlib_cache as cache_module original_cache_dir = cache_module.LEANUP_CACHE_DIR @@ -161,9 +174,13 @@ def fake_lake_build(self): original_lake_init = LeanRepo.lake_init original_lake_update = LeanRepo.lake_update original_lake_build = LeanRepo.lake_build + original_lake_env_lean = LeanRepo.lake_env_lean + original_lake = LeanRepo.lake LeanRepo.lake_init = fake_lake_init LeanRepo.lake_update = fake_lake_update LeanRepo.lake_build = fake_lake_build + LeanRepo.lake_env_lean = fake_lake_env_lean + LeanRepo.lake = fake_lake manager = LeanProjectSetup(elan_manager=FakeElanManager()) target = tmp_path / "BuildDemo" @@ -177,6 +194,9 @@ def fake_lake_build(self): assert result.used_cache is False assert (target / "lean-toolchain").read_text(encoding="utf-8").strip() == "leanprover/lean4:v4.27.0" + 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 config.mathlib_cache_dir.exists() assert (config.mathlib_cache_dir / "mathlib" / "README.md").exists() finally: @@ -184,6 +204,8 @@ def fake_lake_build(self): LeanRepo.lake_init = original_lake_init LeanRepo.lake_update = original_lake_update LeanRepo.lake_build = original_lake_build + LeanRepo.lake_env_lean = original_lake_env_lean + LeanRepo.lake = original_lake def test_setup_symlink_mode_reuses_shared_cache(tmp_path): @@ -212,6 +234,13 @@ def fake_lake_update(self): 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.27.0\n", "", 0 + + def fake_lake(self, args): + raise AssertionError(f"unexpected lake args: {args}") + from leanup.repo import mathlib_cache as cache_module original_cache_dir = cache_module.LEANUP_CACHE_DIR @@ -223,9 +252,13 @@ def fake_lake_build(self): original_lake_init = LeanRepo.lake_init original_lake_update = LeanRepo.lake_update original_lake_build = LeanRepo.lake_build + original_lake_env_lean = LeanRepo.lake_env_lean + original_lake = LeanRepo.lake LeanRepo.lake_init = fake_lake_init LeanRepo.lake_update = fake_lake_update LeanRepo.lake_build = fake_lake_build + 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.mkdir(parents=True, exist_ok=True) @@ -247,3 +280,147 @@ def fake_lake_build(self): LeanRepo.lake_init = original_lake_init LeanRepo.lake_update = original_lake_update LeanRepo.lake_build = original_lake_build + LeanRepo.lake_env_lean = original_lake_env_lean + LeanRepo.lake = original_lake + + +def test_setup_symlink_mode_skips_lake_update_when_manifest_exists(tmp_path): + class FakeElanManager: + def is_elan_installed(self): + return True + + def install_elan(self): + return True + + def install_lean(self, version): + return True + + calls = {"lake_update": 0, "lake_build": 0} + + def fake_lake_update(self): + calls["lake_update"] += 1 + return "", "", 0 + + def fake_lake_build(self): + calls["lake_build"] += 1 + 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 + from leanup.repo.manager import LeanRepo + + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" + original_lake_update = LeanRepo.lake_update + original_lake_build = LeanRepo.lake_build + 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.mkdir(parents=True, exist_ok=True) + (cached_packages / "README.md").write_text("cached\n", encoding="utf-8") + + LeanRepo.lake_update = fake_lake_update + LeanRepo.lake_build = fake_lake_build + LeanRepo.lake_env_lean = fake_lake_env_lean + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + target = tmp_path / "FastDemo" + config = SetupConfig(target_dir=target, lean_version="v4.22.0", dependency_mode="symlink") + + manager.setup(config) + + assert calls["lake_update"] == 0 + assert calls["lake_build"] == 1 + assert (target / "lake-manifest.json").exists() + assert '"name": "FastDemo"' in (target / "lake-manifest.json").read_text(encoding="utf-8") + finally: + cache_module.LEANUP_CACHE_DIR = original_cache_dir + LeanRepo.lake_update = original_lake_update + LeanRepo.lake_build = original_lake_build + LeanRepo.lake_env_lean = original_lake_env_lean + + +def test_setup_uses_bundled_manifest_without_external_reference(tmp_path): + class FakeElanManager: + def is_elan_installed(self): + return True + + def install_elan(self): + return True + + def install_lean(self, version): + return True + + calls = {"lake_update": 0, "lake_build": 0} + + def fake_lake_update(self): + calls["lake_update"] += 1 + return "", "", 0 + + def fake_lake_build(self): + calls["lake_build"] += 1 + 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 + + def fake_lake(self, args): + if args == ["exe", "cache", "get"]: + packages_dir = self.cwd / ".lake" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached from cache get\n", encoding="utf-8") + return "", "", 0 + raise AssertionError(f"unexpected lake args: {args}") + + from leanup.repo import mathlib_cache as cache_module + from leanup.repo.manager import LeanRepo + + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" + original_lake_update = LeanRepo.lake_update + original_lake_build = LeanRepo.lake_build + original_lake_env_lean = LeanRepo.lake_env_lean + original_lake = LeanRepo.lake + + try: + LeanRepo.lake_update = fake_lake_update + LeanRepo.lake_build = fake_lake_build + LeanRepo.lake_env_lean = fake_lake_env_lean + LeanRepo.lake = fake_lake + + manager = LeanProjectSetup(elan_manager=FakeElanManager()) + target = tmp_path / "BundledDemo" + config = SetupConfig(target_dir=target, lean_version="v4.22.0", dependency_mode="symlink") + + manager.setup(config) + + assert calls["lake_update"] == 1 + assert calls["lake_build"] == 1 + assert (target / "lake-manifest.json").exists() + assert '"inputRev": "v4.22.0"' in (target / "lake-manifest.json").read_text(encoding="utf-8") + assert '"name": "BundledDemo"' in (target / "lake-manifest.json").read_text(encoding="utf-8") + assert (cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages").exists() + assert ( + cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "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 + LeanRepo.lake_update = original_lake_update + LeanRepo.lake_build = original_lake_build + LeanRepo.lake_env_lean = original_lake_env_lean + LeanRepo.lake = original_lake + + +def test_bundled_manifest_versions_cover_supported_range_subset(): + from pathlib import Path + + manifest_root = Path(__file__).resolve().parents[1] / "leanup" / "templates" / "mathlib" / "manifests" + bundled_versions = sorted(path.name for path in manifest_root.iterdir() if path.is_dir()) + + for version in ["v4.14.0", "v4.17.0", "v4.19.0", "v4.21.0", "v4.22.0"]: + assert version in bundled_versions From de88c05b22a2621c324ea506271d43bb33861f80 Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Wed, 8 Apr 2026 00:32:06 +0800 Subject: [PATCH 6/8] feat: generate manifests from packages and polish cache tools --- README.md | 6 + docs/getting-started/quickstart.md | 6 + docs/index.md | 1 + leanup/__init__.py | 2 +- leanup/cli/mathlib.py | 9 +- leanup/cli/setup.py | 17 ++- leanup/repo/mathlib_cache.py | 28 +++- leanup/repo/project_setup.py | 133 +++++++++++++++--- .../mathlib/{v4.xx.0 => }/Basic.lean.tmpl | 0 .../mathlib/{v4.xx.0 => }/README.md.tmpl | 0 .../mathlib/{v4.xx.0 => }/lakefile.lean.tmpl | 0 .../manifests/v4.14.0/lake-manifest.json | 95 ------------- .../manifests/v4.17.0/lake-manifest.json | 95 ------------- .../manifests/v4.19.0/lake-manifest.json | 95 ------------- .../manifests/v4.21.0/lake-manifest.json | 95 ------------- .../manifests/v4.22.0/lake-manifest.json | 95 ------------- .../manifests/v4.27.0/lake-manifest.json | 95 ------------- .../mathlib/{v4.xx.0 => }/root.lean.tmpl | 0 tests/test_mathlib_cache_cli.py | 77 ++++++++++ tests/test_setup.py | 98 ++++++++++--- 20 files changed, 330 insertions(+), 617 deletions(-) rename leanup/templates/mathlib/{v4.xx.0 => }/Basic.lean.tmpl (100%) rename leanup/templates/mathlib/{v4.xx.0 => }/README.md.tmpl (100%) rename leanup/templates/mathlib/{v4.xx.0 => }/lakefile.lean.tmpl (100%) delete mode 100644 leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json delete mode 100644 leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json delete mode 100644 leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json delete mode 100644 leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json delete mode 100644 leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json delete mode 100644 leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json rename leanup/templates/mathlib/{v4.xx.0 => }/root.lean.tmpl (100%) diff --git a/README.md b/README.md index 22b16a6..9a0383a 100644 --- a/README.md +++ b/README.md @@ -126,8 +126,14 @@ leanup mathlib cache list # 进入一个 Lean 仓库后，把当前仓库的 .lake/packages 打包到指定目录 cd /path/to/repo leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache + +# 如果本机安装了 pigz，也可以显式启用并发压缩 +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --pigz ``` +- `--pigz` 会在本机存在 `pigz` 时启用并发压缩 +- 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 + ### 交互式安装 使用 `leanup repo install -i` 时，您可以配置： diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 72bd6ff..63ac34e 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -54,8 +54,14 @@ leanup mathlib cache list # 进入当前仓库后，打包本仓库的 .lake/packages 到指定目录 cd /path/to/repo leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache + +# 如果本机安装了 pigz，也可以显式启用并发压缩 +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --pigz ``` +- `--pigz` 会在本机存在 `pigz` 时启用并发压缩 +- 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 + ### 仓库管理 ```bash diff --git a/docs/index.md b/docs/index.md index 5a6d87c..bbf4679 100644 --- a/docs/index.md +++ b/docs/index.md @@ -6,6 +6,7 @@ - `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存 - `leanup mathlib cache list`：查看本地 mathlib 共享缓存版本 +- `leanup mathlib cache pack`：将当前仓库的 `.lake/packages` 打包为共享缓存归档 - `leanup repo install`：安装 Lean 仓库，支持命令优先、交互补参 - `leanup repo list`：查看已安装仓库 diff --git a/leanup/__init__.py b/leanup/__init__.py index c88e01c..f75a4bc 100644 --- a/leanup/__init__.py +++ b/leanup/__init__.py @@ -2,7 +2,7 @@ __author__ = """Lean-zh Community""" __email__ = 'leanprover@outlook.com' -__version__ = '0.1.9' +__version__ = '0.2.0' from .repo import ( RepoManager, diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py index 121dede..9c33278 100644 --- a/leanup/cli/mathlib.py +++ b/leanup/cli/mathlib.py @@ -49,7 +49,12 @@ def list_cache() -> None: required=True, help="Lean version like v4.22.0.", ) -def pack_cache(repo_dir: Path, output_dir: Path, lean_version: str) -> None: +@click.option( + "--pigz/--no-pigz", + default=False, + 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) @@ -57,7 +62,7 @@ def pack_cache(repo_dir: Path, output_dir: Path, lean_version: str) -> None: archive = output_dir / version / "packages.tar.gz" try: - packed = manager.pack_packages_archive(packages_dir, archive) + packed = manager.pack_packages_archive(packages_dir, archive, use_pigz=pigz) except ValueError as exc: raise click.ClickException(str(exc)) from exc diff --git a/leanup/cli/setup.py b/leanup/cli/setup.py index cf3a616..fe4ffa7 100644 --- a/leanup/cli/setup.py +++ b/leanup/cli/setup.py @@ -14,6 +14,13 @@ from leanup.repo.project_setup import LeanProjectSetup, SetupConfig +def _require_non_empty(value: str, field_name: str) -> str: + cleaned = value.strip() + if not cleaned: + raise click.ClickException(f"{field_name} is required.") + return cleaned + + @click.command(name="setup") @click.argument("path", required=False, type=click.Path(path_type=Path)) @click.option( @@ -73,9 +80,15 @@ def setup_project( raise click.ClickException("Missing required setup path or Lean version.") if need_prompt: - path_input = ask_text("Project directory", default=str(path) if path else "") + path_input = _require_non_empty( + ask_text("Project directory", default=str(path) if path else ""), + "Project directory", + ) path = Path(path_input) - lean_version = ask_text("Lean version", default=lean_version or "") + lean_version = _require_non_empty( + ask_text("Lean version", default=lean_version or ""), + "Lean version", + ) name = ask_text("Lake project name", default=name or path.name) or None mathlib = ask_confirm("Enable mathlib dependency?", default=mathlib) diff --git a/leanup/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py index 390991d..9723187 100644 --- a/leanup/repo/mathlib_cache.py +++ b/leanup/repo/mathlib_cache.py @@ -4,7 +4,9 @@ from pathlib import Path import re import shutil +import subprocess import tarfile +import tempfile from leanup.const import LEANUP_CACHE_DIR from leanup.utils.custom_logger import setup_logger @@ -87,16 +89,34 @@ def refresh_local_cache(self, version: str, source_dir: Path, force: bool = True logger.info(f"Refreshed mathlib cache {normalized} from {source_dir}") return packages_dir - def pack_packages_archive(self, packages_dir: Path, output_file: Path) -> Path: + def pack_packages_archive(self, packages_dir: Path, output_file: Path, use_pigz: bool = False) -> Path: if not packages_dir.exists() or not packages_dir.is_dir(): raise ValueError(f"Packages directory not found: {packages_dir}") + source_dir = packages_dir.resolve() if packages_dir.is_symlink() else packages_dir + output_file.parent.mkdir(parents=True, exist_ok=True) if output_file.exists(): output_file.unlink() - with tarfile.open(output_file, "w:gz", dereference=False) as tar: - tar.add(packages_dir, arcname="packages", recursive=True) + if use_pigz and shutil.which("pigz"): + self._pack_with_pigz(source_dir, output_file) + else: + with tarfile.open(output_file, "w:gz", dereference=False) as tar: + tar.add(source_dir, arcname="packages", recursive=True) - logger.info(f"Packed {packages_dir} -> {output_file}") + logger.info(f"Packed {source_dir} -> {output_file}") return output_file + + def _pack_with_pigz(self, source_dir: Path, output_file: Path) -> None: + with tempfile.NamedTemporaryFile(suffix=".tar", delete=False) as handle: + temp_tar = Path(handle.name) + + try: + with tarfile.open(temp_tar, "w", dereference=False) as tar: + tar.add(source_dir, arcname="packages", recursive=True) + + with output_file.open("wb") as output_handle: + subprocess.run(["pigz", "-c", str(temp_tar)], check=True, stdout=output_handle) + finally: + temp_tar.unlink(missing_ok=True) diff --git a/leanup/repo/project_setup.py b/leanup/repo/project_setup.py index 1cd2ba1..9d17a17 100644 --- a/leanup/repo/project_setup.py +++ b/leanup/repo/project_setup.py @@ -6,6 +6,7 @@ import re import shutil import tempfile +from urllib.parse import urlparse from leanup.repo.elan import ElanManager from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version, remove_path @@ -14,8 +15,7 @@ from leanup.utils.custom_logger import setup_logger logger = setup_logger("project_setup") -TEMPLATE_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" / "v4.xx.0" -BUNDLED_MANIFEST_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" / "manifests" +TEMPLATE_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" def sanitize_project_name(name: str) -> str: @@ -86,31 +86,43 @@ def __init__(self, elan_manager: ElanManager | None = None): def setup(self, config: SetupConfig) -> SetupResult: config.validate() + logger.info(f"Preparing Lean project at {config.target_dir}") self._ensure_target_available(config) self._ensure_toolchain(config.lean_version) with working_directory() as temp_dir: project_dir = temp_dir / config.project_name + logger.info(f"Generating project skeleton for {config.project_name}") self._create_project_skeleton(config, project_dir) project = LeanRepo(project_dir) self._write_toolchain(project_dir, config.toolchain) - self._copy_reference_manifest(config, project_dir) used_cache = False cache_dir = config.mathlib_cache_dir if config.mathlib else None if config.mathlib and config.resolved_dependency_mode == "symlink": + logger.info("Checking reusable mathlib package cache") used_cache = self._prepare_mathlib_cache(config, project_dir) + if used_cache: + self._write_manifest_from_packages(config, project_dir) if config.mathlib and self._should_run_lake_update(config, project_dir): + logger.info("Running lake update") self._run_lake_update(project) + logger.info("Running lake exe cache get") self._run_lake_cache_get(project) + logger.info("Refreshing shared packages cache") self._refresh_mathlib_cache(config, project_dir) + logger.info("Generating manifest from resolved packages") + self._write_manifest_from_packages(config, project_dir) if config.resolved_dependency_mode == "symlink": + logger.info("Linking shared packages cache into project") self._link_mathlib_cache(config, project_dir) used_cache = True + logger.info("Running lake build") self._run_lake_build(project) + logger.info("Verifying project with Mathlib.Init and Lean.versionString") self._verify_mathlib_project(project_dir) shutil.move(str(project_dir), str(config.target_dir)) @@ -134,6 +146,7 @@ def _ensure_target_available(self, config: SetupConfig) -> None: target.parent.mkdir(parents=True, exist_ok=True) def _ensure_toolchain(self, version: str) -> None: + logger.info(f"Ensuring Lean toolchain {version} is installed") if not self.elan_manager.is_elan_installed() and not self.elan_manager.install_elan(): raise RuntimeError("Failed to install elan.") if not self.elan_manager.install_lean(version): @@ -166,26 +179,106 @@ def _render_mathlib_template(self, config: SetupConfig, project_dir: Path) -> No output_path.parent.mkdir(parents=True, exist_ok=True) output_path.write_text(content.format(**context), encoding="utf-8") - def _bundled_manifest_path(self, version: str) -> Path | None: - candidate = BUNDLED_MANIFEST_ROOT / normalize_lean_version(version) / "lake-manifest.json" - if candidate.exists(): - return candidate - return None - - def _copy_reference_manifest(self, config: SetupConfig, project_dir: Path) -> None: - if not config.mathlib: + def _write_manifest_from_packages(self, config: SetupConfig, project_dir: Path) -> None: + packages_dir = project_dir / ".lake" / "packages" + if not packages_dir.exists(): return - bundled_manifest = self._bundled_manifest_path(config.lean_version) - if bundled_manifest: - manifest_path = project_dir / "lake-manifest.json" - shutil.copy2(bundled_manifest, manifest_path) - self._rewrite_manifest_name(manifest_path, config.project_name) - - def _rewrite_manifest_name(self, manifest_path: Path, project_name: str) -> None: - manifest = json.loads(manifest_path.read_text(encoding="utf-8")) - manifest["name"] = project_name + if not self._can_generate_manifest_from_packages(packages_dir): + logger.info("Skipping manifest generation from packages because git metadata is incomplete") + return + + mathlib_manifest = self._read_mathlib_embedded_manifest(packages_dir) + packages = [] + for package_dir in sorted(path for path in packages_dir.iterdir() if path.is_dir()): + packages.append( + self._build_manifest_entry( + package_dir=package_dir, + lean_version=config.lean_version, + mathlib_manifest=mathlib_manifest, + ) + ) + + manifest = { + "version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": packages, + "name": config.project_name, + "lakeDir": ".lake", + } + manifest_path = project_dir / "lake-manifest.json" manifest_path.write_text(json.dumps(manifest, indent=1) + "\n", encoding="utf-8") + def _can_generate_manifest_from_packages(self, packages_dir: Path) -> bool: + package_dirs = [path for path in packages_dir.iterdir() if path.is_dir()] + if not package_dirs: + return False + for package_dir in package_dirs: + if not (package_dir / ".git").exists(): + return False + return True + + def _read_mathlib_embedded_manifest(self, packages_dir: Path) -> dict[str, dict]: + mathlib_manifest_path = packages_dir / "mathlib" / "lake-manifest.json" + if not mathlib_manifest_path.exists(): + return {} + manifest = json.loads(mathlib_manifest_path.read_text(encoding="utf-8")) + return {entry["name"]: entry for entry in manifest.get("packages", [])} + + def _build_manifest_entry( + self, + package_dir: Path, + lean_version: str, + mathlib_manifest: dict[str, dict], + ) -> dict: + package_name = package_dir.name + url = self._read_git_origin_url(package_dir) + head_rev = self._read_git_head(package_dir) + config_file = self._detect_config_file(package_dir) + inherited = package_name != "mathlib" + input_rev = lean_version if package_name == "mathlib" else mathlib_manifest.get(package_name, {}).get("inputRev", "main") + + return { + "url": url, + "type": "git", + "subDir": None, + "scope": self._infer_scope(url), + "rev": head_rev, + "name": package_name, + "manifestFile": "lake-manifest.json", + "inputRev": input_rev, + "inherited": inherited, + "configFile": config_file, + } + + def _read_git_origin_url(self, package_dir: Path) -> str: + from git import Repo + + repo = Repo(package_dir) + return next(repo.remote("origin").urls) + + def _read_git_head(self, package_dir: Path) -> str: + from git import Repo + + repo = Repo(package_dir) + return repo.head.commit.hexsha + + def _detect_config_file(self, package_dir: Path) -> str: + if (package_dir / "lakefile.lean").exists(): + return "lakefile.lean" + if (package_dir / "lakefile.toml").exists(): + return "lakefile.toml" + raise RuntimeError(f"No Lake config file found in package: {package_dir}") + + def _infer_scope(self, url: str) -> str: + parsed = urlparse(url) + path = parsed.path.rstrip("/") + if path.endswith(".git"): + path = path[:-4] + parts = [part for part in path.split("/") if part] + if len(parts) >= 2: + return parts[-2] + return "" + def _should_run_lake_update(self, config: SetupConfig, project_dir: Path) -> bool: if not config.mathlib: return False diff --git a/leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl b/leanup/templates/mathlib/Basic.lean.tmpl similarity index 100% rename from leanup/templates/mathlib/v4.xx.0/Basic.lean.tmpl rename to leanup/templates/mathlib/Basic.lean.tmpl diff --git a/leanup/templates/mathlib/v4.xx.0/README.md.tmpl b/leanup/templates/mathlib/README.md.tmpl similarity index 100% rename from leanup/templates/mathlib/v4.xx.0/README.md.tmpl rename to leanup/templates/mathlib/README.md.tmpl diff --git a/leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl b/leanup/templates/mathlib/lakefile.lean.tmpl similarity index 100% rename from leanup/templates/mathlib/v4.xx.0/lakefile.lean.tmpl rename to leanup/templates/mathlib/lakefile.lean.tmpl diff --git a/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json deleted file mode 100644 index efa9181..0000000 --- a/leanup/templates/mathlib/manifests/v4.14.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "68280daef58803f68368eb2e53046dabcd270c9d", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.47", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json deleted file mode 100644 index 4c9e941..0000000 --- a/leanup/templates/mathlib/manifests/v4.17.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "5269898d6a51d047931107c8d72d934d8d5d3753", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.17.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c708be04267e3e995a14ac0d08b1530579c1525a", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.52", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json deleted file mode 100644 index 231ea65..0000000 --- a/leanup/templates/mathlib/manifests/v4.19.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c44e0c8ee63ca166450922a373c7409c5d26b00b", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.19.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "77e08eddc486491d7b9e470926b3dbe50319451a", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "e6a9f0f5ee3ccf7443a0070f92b62f8db12ae82b", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c4919189477c3221e6a204008998b0d724f49904", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.57", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "f5d04a9c4973d401c8c92500711518f7c656f034", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "02dbd02bc00ec4916e99b04b2245b30200e200d0", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json deleted file mode 100644 index b1363cf..0000000 --- a/leanup/templates/mathlib/manifests/v4.21.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "308445d7985027f538e281e18df29ca16ede2ba3", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c4aa78186d388e50a436e8362b947bae125a2933", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.62", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8ff27701d003456fd59f13a9212431239d902aef", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json deleted file mode 100644 index 19c996c..0000000 --- a/leanup/templates/mathlib/manifests/v4.22.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "eb164a46de87078f27640ee71e6c3841defc2484", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.68", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "240676e9568c254a69be94801889d4b13f3b249f", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json b/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json deleted file mode 100644 index 6769981..0000000 --- a/leanup/templates/mathlib/manifests/v4.27.0/lake-manifest.json +++ /dev/null @@ -1,95 +0,0 @@ -{"version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c04225ee7c0585effbd933662b3151f01b600e40", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.85", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", - "inherited": true, - "configFile": "lakefile.toml"}], - "name": "lean4web", - "lakeDir": ".lake"} diff --git a/leanup/templates/mathlib/v4.xx.0/root.lean.tmpl b/leanup/templates/mathlib/root.lean.tmpl similarity index 100% rename from leanup/templates/mathlib/v4.xx.0/root.lean.tmpl rename to leanup/templates/mathlib/root.lean.tmpl diff --git a/tests/test_mathlib_cache_cli.py b/tests/test_mathlib_cache_cli.py index 6165dbc..baa0a5e 100644 --- a/tests/test_mathlib_cache_cli.py +++ b/tests/test_mathlib_cache_cli.py @@ -4,6 +4,7 @@ from click.testing import CliRunner from leanup.cli import cli +from leanup.repo.mathlib_cache import MathlibCacheManager def test_mathlib_cache_pack_archives_current_repo(tmp_path): @@ -35,3 +36,79 @@ def test_mathlib_cache_pack_archives_current_repo(tmp_path): with tarfile.open(archive, "r:gz") as tar: names = tar.getnames() assert "packages/mathlib/README.md" in names + + +def test_mathlib_cache_pack_follows_root_packages_symlink(tmp_path): + runner = CliRunner() + source_dir = tmp_path / "shared-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), + "--output-dir", + str(output_dir), + "--lean-version", + "v4.29.0", + ], + ) + + archive = output_dir / "v4.29.0" / "packages.tar.gz" + assert result.exit_code == 0 + with tarfile.open(archive, "r:gz") as tar: + names = tar.getnames() + assert "packages/mathlib/README.md" in names + + +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" + 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 = {} + + def fake_pack(self, packages_dir, output_file, use_pigz=False): + captured["packages_dir"] = packages_dir + captured["output_file"] = output_file + captured["use_pigz"] = use_pigz + output_file.parent.mkdir(parents=True, exist_ok=True) + output_file.write_bytes(b"ok") + return output_file + + monkeypatch.setattr(MathlibCacheManager, "pack_packages_archive", fake_pack) + + result = runner.invoke( + cli, + [ + "mathlib", + "cache", + "pack", + "--repo-dir", + str(repo_dir), + "--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["use_pigz"] is True diff --git a/tests/test_setup.py b/tests/test_setup.py index 0ad224a..b8aa82e 100644 --- a/tests/test_setup.py +++ b/tests/test_setup.py @@ -2,11 +2,26 @@ from pathlib import Path from click.testing import CliRunner +from git import Repo from leanup.cli import cli from leanup.repo.project_setup import LeanProjectSetup, SetupConfig +def _init_fake_package_repo(package_dir: Path, package_name: str = "mathlib") -> None: + package_dir.mkdir(parents=True, exist_ok=True) + (package_dir / "README.md").write_text("cached\n", encoding="utf-8") + (package_dir / "lakefile.lean").write_text(f"package {package_name} where\n", encoding="utf-8") + repo = Repo.init(package_dir) + with repo.config_writer() as config: + config.set_value("user", "name", "LeanUp Test") + config.set_value("user", "email", "leanup@example.com") + if "origin" not in [remote.name for remote in repo.remotes]: + repo.create_remote("origin", f"https://github.com/leanprover-community/{package_name}.git") + repo.index.add(["README.md", "lakefile.lean"]) + repo.index.commit("init") + + def test_setup_command_rejects_symlink_without_mathlib(): runner = CliRunner() @@ -105,6 +120,45 @@ def fake_setup(self, config): assert captured["dependency_mode"] == "symlink" +def test_setup_interactive_rejects_blank_project_directory(monkeypatch): + import importlib + + setup_cli_module = importlib.import_module("leanup.cli.setup") + runner = CliRunner() + + monkeypatch.setattr( + setup_cli_module, + "resolve_interactive_mode", + lambda interactive, auto_prompt_condition: (None, True, False, True, True), + ) + monkeypatch.setattr(setup_cli_module, "ask_text", lambda message, default="": " ") + + result = runner.invoke(cli, ["setup"]) + + assert result.exit_code != 0 + assert "Project directory is required." in result.output + + +def test_setup_interactive_rejects_blank_lean_version(monkeypatch, tmp_path): + import importlib + + setup_cli_module = importlib.import_module("leanup.cli.setup") + runner = CliRunner() + values = iter([str(tmp_path / "Demo"), " "]) + + monkeypatch.setattr( + setup_cli_module, + "resolve_interactive_mode", + lambda interactive, auto_prompt_condition: (None, True, False, True, True), + ) + monkeypatch.setattr(setup_cli_module, "ask_text", lambda message, default="": next(values)) + + result = runner.invoke(cli, ["setup"]) + + assert result.exit_code != 0 + assert "Lean version is required." in result.output + + def test_setup_config_prefers_symlink_when_cache_exists(tmp_path): from leanup.repo.mathlib_cache import MathlibCacheManager from leanup.repo import mathlib_cache as cache_module @@ -158,8 +212,11 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): def fake_lake(self, args): if args == ["exe", "cache", "get"]: packages_dir = self.cwd / ".lake" / "packages" / "mathlib" - packages_dir.mkdir(parents=True, exist_ok=True) + _init_fake_package_repo(packages_dir) (packages_dir / "README.md").write_text("cached from cache get\n", encoding="utf-8") + repo = Repo(packages_dir) + repo.index.add(["README.md", "lakefile.lean"]) + repo.index.commit("update readme") return "", "", 0 raise AssertionError(f"unexpected lake args: {args}") @@ -225,7 +282,10 @@ def fake_lake_init(self, name, template=None): (project_dir / "lakefile.lean").write_text(f"template={template}\n", encoding="utf-8") return "", "", 0 + calls = {"lake_update": 0, "cache_get": 0} + def fake_lake_update(self): + calls["lake_update"] += 1 packages_dir = self.cwd / ".lake" / "packages" packages_dir.mkdir(parents=True, exist_ok=True) (self.cwd / "lake-manifest.json").write_text("{}\n", encoding="utf-8") @@ -239,6 +299,12 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): return "4.27.0\n", "", 0 def fake_lake(self, args): + if args == ["exe", "cache", "get"]: + calls["cache_get"] += 1 + packages_dir = self.cwd / ".lake" / "packages" / "mathlib" + packages_dir.mkdir(parents=True, exist_ok=True) + (packages_dir / "README.md").write_text("cached\n", encoding="utf-8") + return "", "", 0 raise AssertionError(f"unexpected lake args: {args}") from leanup.repo import mathlib_cache as cache_module @@ -261,8 +327,7 @@ def fake_lake(self, args): LeanRepo.lake = fake_lake cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.27.0" / "packages" / "mathlib" - cached_packages.mkdir(parents=True, exist_ok=True) - (cached_packages / "README.md").write_text("cached\n", encoding="utf-8") + _init_fake_package_repo(cached_packages) manager = LeanProjectSetup(elan_manager=FakeElanManager()) target = tmp_path / "SymlinkDemo" @@ -275,6 +340,9 @@ def fake_lake(self, args): assert packages_link.is_symlink() assert packages_link.resolve() == config.mathlib_cache_dir assert (packages_link / "mathlib" / "README.md").read_text(encoding="utf-8").strip() == "cached" + assert (target / "lake-manifest.json").exists() + assert calls["lake_update"] == 0 + assert calls["cache_get"] == 0 finally: cache_module.LEANUP_CACHE_DIR = original_cache_dir LeanRepo.lake_init = original_lake_init @@ -320,8 +388,7 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): try: cached_packages = cache_module.LEANUP_CACHE_DIR / "setup" / "mathlib" / "v4.22.0" / "packages" / "mathlib" - cached_packages.mkdir(parents=True, exist_ok=True) - (cached_packages / "README.md").write_text("cached\n", encoding="utf-8") + _init_fake_package_repo(cached_packages) LeanRepo.lake_update = fake_lake_update LeanRepo.lake_build = fake_lake_build @@ -372,8 +439,11 @@ def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): def fake_lake(self, args): if args == ["exe", "cache", "get"]: packages_dir = self.cwd / ".lake" / "packages" / "mathlib" - packages_dir.mkdir(parents=True, exist_ok=True) + _init_fake_package_repo(packages_dir) (packages_dir / "README.md").write_text("cached from cache get\n", encoding="utf-8") + repo = Repo(packages_dir) + repo.index.add(["README.md", "lakefile.lean"]) + repo.index.commit("update readme") return "", "", 0 raise AssertionError(f"unexpected lake args: {args}") @@ -402,8 +472,10 @@ def fake_lake(self, args): assert calls["lake_update"] == 1 assert calls["lake_build"] == 1 assert (target / "lake-manifest.json").exists() - assert '"inputRev": "v4.22.0"' in (target / "lake-manifest.json").read_text(encoding="utf-8") - assert '"name": "BundledDemo"' in (target / "lake-manifest.json").read_text(encoding="utf-8") + manifest_text = (target / "lake-manifest.json").read_text(encoding="utf-8") + 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 / "setup" / "mathlib" / "v4.22.0" / "packages" / "mathlib" / "README.md" @@ -414,13 +486,3 @@ def fake_lake(self, args): LeanRepo.lake_build = original_lake_build LeanRepo.lake_env_lean = original_lake_env_lean LeanRepo.lake = original_lake - - -def test_bundled_manifest_versions_cover_supported_range_subset(): - from pathlib import Path - - manifest_root = Path(__file__).resolve().parents[1] / "leanup" / "templates" / "mathlib" / "manifests" - bundled_versions = sorted(path.name for path in manifest_root.iterdir() if path.is_dir()) - - for version in ["v4.14.0", "v4.17.0", "v4.19.0", "v4.21.0", "v4.22.0"]: - assert version in bundled_versions From c5bfdaaae1c313b2238e4e0ef37b6b9092468568 Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Wed, 8 Apr 2026 00:46:16 +0800 Subject: [PATCH 7/8] feat: improve cache packing defaults and progress logs --- README.md | 7 ++-- docs/getting-started/quickstart.md | 7 ++-- leanup/cli/mathlib.py | 2 +- leanup/repo/mathlib_cache.py | 55 ++++++++++++++++++++++-------- tests/test_mathlib_cache_cli.py | 37 ++++++++++++++++++++ 5 files changed, 86 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 9a0383a..51eb441 100644 --- a/README.md +++ b/README.md @@ -127,12 +127,13 @@ leanup mathlib cache list cd /path/to/repo leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache -# 如果本机安装了 pigz，也可以显式启用并发压缩 -leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --pigz +# 如需关闭并发压缩，可以显式禁用 pigz +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --no-pigz ``` -- `--pigz` 会在本机存在 `pigz` 时启用并发压缩 +- 默认会在本机存在 `pigz` 时启用并发压缩 - 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 +- `--no-pigz` 可显式关闭并发压缩 ### 交互式安装 diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 63ac34e..a51dfe6 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -55,12 +55,13 @@ leanup mathlib cache list cd /path/to/repo leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache -# 如果本机安装了 pigz，也可以显式启用并发压缩 -leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --pigz +# 如需关闭并发压缩，可以显式禁用 pigz +leanup mathlib cache pack --lean-version v4.22.0 --output-dir /path/to/cache --no-pigz ``` -- `--pigz` 会在本机存在 `pigz` 时启用并发压缩 +- 默认会在本机存在 `pigz` 时启用并发压缩 - 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 +- `--no-pigz` 可显式关闭并发压缩 ### 仓库管理 diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py index 9c33278..75b0352 100644 --- a/leanup/cli/mathlib.py +++ b/leanup/cli/mathlib.py @@ -51,7 +51,7 @@ def list_cache() -> None: ) @click.option( "--pigz/--no-pigz", - default=False, + 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: diff --git a/leanup/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py index 9723187..2983092 100644 --- a/leanup/repo/mathlib_cache.py +++ b/leanup/repo/mathlib_cache.py @@ -94,29 +94,54 @@ def pack_packages_archive(self, packages_dir: Path, output_file: Path, use_pigz: raise ValueError(f"Packages directory not found: {packages_dir}") source_dir = packages_dir.resolve() if packages_dir.is_symlink() else packages_dir + logger.info(f"Preparing packages archive from {packages_dir}") + if packages_dir.is_symlink(): + logger.info(f"Resolved root packages symlink to {source_dir}") output_file.parent.mkdir(parents=True, exist_ok=True) - if output_file.exists(): - output_file.unlink() + temp_output = output_file.parent / f".{output_file.name}.tmp" + remove_path(temp_output) if use_pigz and shutil.which("pigz"): - self._pack_with_pigz(source_dir, output_file) + logger.info("Using pigz for parallel compression") + self._pack_with_pigz(source_dir, temp_output) else: - with tarfile.open(output_file, "w:gz", dereference=False) as tar: + if use_pigz: + logger.info("pigz requested but not found; falling back to standard gzip") + else: + logger.info("Using standard gzip compression") + logger.info(f"Writing tar.gz archive to temporary file {temp_output}") + with tarfile.open(temp_output, "w:gz", dereference=False) as tar: tar.add(source_dir, arcname="packages", recursive=True) + remove_path(output_file) + temp_output.replace(output_file) + logger.info(f"Packed {source_dir} -> {output_file}") return output_file def _pack_with_pigz(self, source_dir: Path, output_file: Path) -> None: - with tempfile.NamedTemporaryFile(suffix=".tar", delete=False) as handle: - temp_tar = Path(handle.name) - - try: - with tarfile.open(temp_tar, "w", dereference=False) as tar: - tar.add(source_dir, arcname="packages", recursive=True) - - with output_file.open("wb") as output_handle: - subprocess.run(["pigz", "-c", str(temp_tar)], check=True, stdout=output_handle) - finally: - temp_tar.unlink(missing_ok=True) + logger.info(f"Streaming tar archive from {source_dir.parent} into pigz") + transform = f"s,^{re.escape(source_dir.name)},packages," + with output_file.open("wb") as output_handle: + tar_proc = subprocess.Popen( + [ + "tar", + "-C", + str(source_dir.parent), + "--transform", + transform, + "-cf", + "-", + source_dir.name, + ], + stdout=subprocess.PIPE, + ) + try: + subprocess.run(["pigz", "-c"], check=True, stdin=tar_proc.stdout, stdout=output_handle) + finally: + if tar_proc.stdout is not None: + tar_proc.stdout.close() + tar_returncode = tar_proc.wait() + if tar_returncode != 0: + raise subprocess.CalledProcessError(tar_returncode, tar_proc.args) diff --git a/tests/test_mathlib_cache_cli.py b/tests/test_mathlib_cache_cli.py index baa0a5e..a855393 100644 --- a/tests/test_mathlib_cache_cli.py +++ b/tests/test_mathlib_cache_cli.py @@ -112,3 +112,40 @@ def fake_pack(self, packages_dir, output_file, use_pigz=False): assert captured["packages_dir"] == repo_dir / ".lake" / "packages" assert captured["output_file"] == output_dir / "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" + 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 = {} + + def fake_pack(self, packages_dir, output_file, use_pigz=False): + captured["use_pigz"] = use_pigz + output_file.parent.mkdir(parents=True, exist_ok=True) + output_file.write_bytes(b"ok") + return output_file + + monkeypatch.setattr(MathlibCacheManager, "pack_packages_archive", fake_pack) + + result = runner.invoke( + cli, + [ + "mathlib", + "cache", + "pack", + "--repo-dir", + str(repo_dir), + "--output-dir", + str(output_dir), + "--lean-version", + "v4.22.0", + ], + ) + + assert result.exit_code == 0 + assert captured["use_pigz"] is True From 87ea772860912ccc2c83333aee114dd8b5d98dc5 Mon Sep 17 00:00:00 2001 From: rex <1073853456@qq.com> Date: Wed, 8 Apr 2026 01:12:06 +0800 Subject: [PATCH 8/8] ci: drop windows test job --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index ad35aad..48759ae 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -16,7 +16,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-latest, macos-latest, windows-latest] + os: [ubuntu-latest, macos-latest] python-version: ["3.9"] steps: