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: 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..51eb441 100644 --- a/README.md +++ b/README.md @@ -16,13 +16,12 @@ **一个用于管理 Lean 数学证明语言环境的 Python 工具** -[English](README-en.md) | [简体中文](README.md) - ## 🎯 功能特性 -- **📦 仓库管理**: 安装和管理 Lean 仓库，支持交互式配置 +- **📦 仓库管理**: 安装和管理 Lean 仓库，支持命令优先、交互兜底的配置流程 +- **⚡ 项目初始化**: 快速创建固定 Lean 版本的项目，并复用同版本 mathlib 缓存 - **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows - **📦 简单易用**: 通过 `pip install leanup` 快速安装 - **🔄 命令代理**: 透明代理所有 elan 命令，无缝体验 @@ -47,48 +46,15 @@ pip install -e . # 查看帮助 leanup --help -# 安装 elan 并初始化配置 -leanup init - -# 安装 -leanup install # stable - -# 查看状态 -leanup status +# 快速初始化一个 Lean + mathlib 项目 +leanup setup ./Demo --lean-version v4.27.0 -# 代理执行 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 @@ -104,9 +70,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" @@ -120,9 +89,55 @@ 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` +- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 +- `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装 + +### 管理 mathlib 缓存 + +```bash +# 查看 LeanUp 已有缓存版本 +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 --no-pigz +``` + +- 默认会在本机存在 `pigz` 时启用并发压缩 +- 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 +- `--no-pigz` 可显式关闭并发压缩 + ### 交互式安装 -使用 `leanup repo install` 的 `--interactive` 标志时，您可以配置： +使用 `leanup repo install -i` 时，您可以配置： - 仓库名称（必需） - 仓库源的基础 URL @@ -134,6 +149,13 @@ leanup repo list -n mathlib - 要编译的特定构建包 - 是否覆盖现有目录 +默认规则： + +- 命令优先，交互兜底 +- 缺必要参数时自动进入交互 +- `-i` 强制交互 +- `-I` 禁止交互，参数不足时直接报错 + ### 编程接口 #### 使用 InstallConfig @@ -201,6 +223,11 @@ stdout, stderr, returncode = lean_repo.lake_env_lean("Main.lean") ## 🛠️ 开发 +仓库级开发规范见： + +- `AGENTS.md` +- `DEVELOP.md` + ### 环境设置 ```bash @@ -228,7 +255,7 @@ coverage report -m ## ⚙️ 配置 -LeanUp 使用位于 `~/.leanup/config.toml` 的配置文件。您可以自定义： +LeanUp 使用位于 `~/.leanup/config.yaml` 的配置文件。您可以自定义： - 默认仓库源 - 仓库缓存目录 @@ -267,4 +294,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..a51dfe6 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -1,92 +1,108 @@ -# 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 +### 查看帮助 ```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 +# 创建一个带 mathlib 的 Lean 项目，默认有缓存就复用，没有缓存就构建 +leanup setup ./Demo --lean-version v4.27.0 + +# 首次为某个版本准备缓存时，从头构建依赖 +leanup setup ./DemoBuild --lean-version v4.27.0 --dependency-mode build -# Install specific Lean toolchain version -leanup install v4.14.0 +# 后续项目直接复用共享依赖缓存 +leanup setup ./DemoFast --lean-version v4.27.0 --dependency-mode symlink + +# 创建不依赖 mathlib 的纯 Lean 项目 +leanup setup ./PlainDemo --lean-version v4.27.0 --no-mathlib ``` -### Manage Toolchains +说明： + +- 共享缓存默认放在 `LEANUP_CACHE_DIR/setup/mathlib//packages` +- Linux 默认通常对应 `~/.cache/leanup/setup/mathlib//packages` +- `symlink` 模式只对 `mathlib` 项目开放 +- 默认行为偏向缓存复用：如果已有 `packages` 缓存就直接链接，否则执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存 +- `setup` 会自动确保 `elan` 和目标 Lean toolchain 已安装 +- 如果你需要直接透传给 `elan`，仍然可以使用 `leanup elan ...` + +### 管理 mathlib 缓存 ```bash -# Proxy execute elan commands -leanup elan --help -leanup elan toolchain list -leanup elan toolchain install stable -leanup elan default stable +# 查看 LeanUp 已有缓存版本 +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 --no-pigz ``` -### Repository Management +- 默认会在本机存在 `pigz` 时启用并发压缩 +- 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包 +- `--no-pigz` 可显式关闭并发压缩 + +### 仓库管理 ```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 +115,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 +187,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..bbf4679 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,21 @@ +# LeanUp + +一个用于管理 Lean 数学证明语言环境的 Python 工具。 + +## 功能特性 + +- `leanup setup`：快速创建固定 Lean 版本项目，支持 mathlib 共享缓存 +- `leanup mathlib cache list`：查看本地 mathlib 共享缓存版本 +- `leanup mathlib cache pack`：将当前仓库的 `.lake/packages` 打包为共享缓存归档 +- `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/__init__.py b/leanup/__init__.py index 2d87293..f75a4bc 100644 --- a/leanup/__init__.py +++ b/leanup/__init__.py @@ -2,12 +2,21 @@ __author__ = """Lean-zh Community""" __email__ = 'leanprover@outlook.com' -__version__ = '0.1.9' +__version__ = '0.2.0' -from .repo import RepoManager, ElanManager, LeanRepo +from .repo import ( + RepoManager, + ElanManager, + MathlibCacheManager, + LeanRepo, + LeanProjectSetup, + SetupConfig, + SetupResult, +) 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 177effa..568d605 100644 --- a/leanup/cli/__init__.py +++ b/leanup/cli/__init__.py @@ -1,11 +1,16 @@ 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.mathlib import mathlib from leanup.cli.repo import repo +from leanup.cli.setup import setup_project +from leanup.cli.elan_ops import ( + init_elan, + install_lean_toolchain, + proxy_elan, + show_status, +) logger = setup_logger("leanup_cli") @@ -21,77 +26,36 @@ 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.add_command(setup_project) +cli.add_command(mathlib) @cli.command(context_settings=dict(ignore_unknown_options=True)) -@click.argument('args', nargs=-1, type=click.UNPROCESSED) +@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..f9a47a0 --- /dev/null +++ b/leanup/cli/interaction.py @@ -0,0 +1,117 @@ +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 _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: + _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: + _render_heading("Confirm", message) + return click.confirm("Continue", default=default, err=True) diff --git a/leanup/cli/mathlib.py b/leanup/cli/mathlib.py new file mode 100644 index 0000000..75b0352 --- /dev/null +++ b/leanup/cli/mathlib.py @@ -0,0 +1,69 @@ +from __future__ import annotations + +from pathlib import Path + +import click + +from leanup.repo.mathlib_cache import MathlibCacheManager, normalize_lean_version + + +@click.group() +def mathlib() -> None: + """Manage mathlib-specific helpers and caches.""" + + +@mathlib.group() +def cache() -> None: + """Manage reusable mathlib package caches.""" + + +@cache.command(name="list") +def list_cache() -> None: + """List available mathlib caches.""" + manager = MathlibCacheManager() + entries = manager.list_entries() + + if not entries: + click.echo("No mathlib caches found.") + return + + for entry in entries: + click.echo(entry.version) + + +@cache.command(name="pack") +@click.option( + "--repo-dir", + type=click.Path(path_type=Path, file_okay=False, dir_okay=True), + default=Path.cwd, + help="Lean repository directory containing .lake/packages.", +) +@click.option( + "--output-dir", + type=click.Path(path_type=Path, file_okay=False, dir_okay=True), + required=True, + help="Directory where /packages.tar.gz will be written.", +) +@click.option( + "--lean-version", + required=True, + help="Lean version like v4.22.0.", +) +@click.option( + "--pigz/--no-pigz", + default=True, + help="Use pigz for parallel compression when it is available.", +) +def pack_cache(repo_dir: Path, output_dir: Path, lean_version: str, pigz: bool) -> None: + """Pack current repository .lake/packages into a versioned cache archive.""" + manager = MathlibCacheManager() + version = normalize_lean_version(lean_version) + packages_dir = repo_dir / ".lake" / "packages" + archive = output_dir / version / "packages.tar.gz" + + try: + packed = manager.pack_packages_archive(packages_dir, archive, use_pigz=pigz) + except ValueError as exc: + raise click.ClickException(str(exc)) from exc + + click.echo(str(packed)) diff --git a/leanup/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/cli/setup.py b/leanup/cli/setup.py new file mode 100644 index 0000000..fe4ffa7 --- /dev/null +++ b/leanup/cli/setup.py @@ -0,0 +1,144 @@ +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 + + +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( + "--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 = _require_non_empty( + ask_text("Project directory", default=str(path) if path else ""), + "Project directory", + ) + path = Path(path_input) + 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) + + 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..4061622 100644 --- a/leanup/repo/__init__.py +++ b/leanup/repo/__init__.py @@ -2,5 +2,15 @@ from .manager import RepoManager, LeanRepo from .elan import ElanManager +from .mathlib_cache import MathlibCacheManager +from .project_setup import LeanProjectSetup, SetupConfig, SetupResult -__all__ = ['RepoManager', 'ElanManager', 'LeanRepo'] +__all__ = [ + 'RepoManager', + 'ElanManager', + 'MathlibCacheManager', + 'LeanRepo', + 'LeanProjectSetup', + 'SetupConfig', + 'SetupResult', +] diff --git a/leanup/repo/elan.py b/leanup/repo/elan.py index c9de4c0..67c4db1 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,58 +115,73 @@ 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: + 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: 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 +189,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 +212,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/repo/mathlib_cache.py b/leanup/repo/mathlib_cache.py new file mode 100644 index 0000000..2983092 --- /dev/null +++ b/leanup/repo/mathlib_cache.py @@ -0,0 +1,147 @@ +from __future__ import annotations + +from dataclasses import dataclass +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 + +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 + + @property + def local_available(self) -> bool: + return self.local_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 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)) + + return [ + CacheEntry( + version=version, + local_path=self.get_local_packages_dir(version), + ) + for version in sorted(versions) + ] + + def ensure_local_cache(self, version: str) -> Path | None: + local_path = self.get_local_packages_dir(version) + if local_path.exists(): + return local_path + 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() and not force: + return packages_dir + + version_root.mkdir(parents=True, exist_ok=True) + temp_root = version_root / ".packages.tmp" + 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, 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 + 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) + temp_output = output_file.parent / f".{output_file.name}.tmp" + remove_path(temp_output) + + if use_pigz and shutil.which("pigz"): + logger.info("Using pigz for parallel compression") + self._pack_with_pigz(source_dir, temp_output) + else: + 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: + 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/leanup/repo/project_setup.py b/leanup/repo/project_setup.py new file mode 100644 index 0000000..9d17a17 --- /dev/null +++ b/leanup/repo/project_setup.py @@ -0,0 +1,346 @@ +from __future__ import annotations + +from dataclasses import dataclass +import json +from pathlib import Path +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 +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") +TEMPLATE_ROOT = Path(__file__).resolve().parent.parent / "templates" / "mathlib" + + +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 + + +@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" + + @property + def toolchain(self) -> str: + return f"leanprover/lean4:{self.lean_version}" + + @property + def mathlib_cache_dir(self) -> Path: + return MathlibCacheManager().get_local_packages_dir(self.lean_version) + + def validate(self) -> None: + if self.resolved_dependency_mode not in {"symlink", "build"}: + raise ValueError("Dependency mode must be either 'symlink' or 'build'.") + if self.resolved_dependency_mode == "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() + self.cache_manager = MathlibCacheManager() + + 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) + + 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)) + + 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: + 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): + 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 _write_manifest_from_packages(self, config: SetupConfig, project_dir: Path) -> None: + packages_dir = project_dir / ".lake" / "packages" + if not packages_dir.exists(): + return + 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 + 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") + + 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_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 _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: + 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) + 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 + + self.cache_manager.refresh_local_cache(config.lean_version, source_dir) diff --git a/leanup/templates/mathlib/Basic.lean.tmpl b/leanup/templates/mathlib/Basic.lean.tmpl new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/leanup/templates/mathlib/Basic.lean.tmpl @@ -0,0 +1 @@ +def hello := "world" diff --git a/leanup/templates/mathlib/README.md.tmpl b/leanup/templates/mathlib/README.md.tmpl new file mode 100644 index 0000000..1ec9149 --- /dev/null +++ b/leanup/templates/mathlib/README.md.tmpl @@ -0,0 +1 @@ +# {project_name} diff --git a/leanup/templates/mathlib/lakefile.lean.tmpl b/leanup/templates/mathlib/lakefile.lean.tmpl new file mode 100644 index 0000000..951a48e --- /dev/null +++ b/leanup/templates/mathlib/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/root.lean.tmpl b/leanup/templates/mathlib/root.lean.tmpl new file mode 100644 index 0000000..b081467 --- /dev/null +++ b/leanup/templates/mathlib/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/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_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_mathlib_cache_cli.py b/tests/test_mathlib_cache_cli.py new file mode 100644 index 0000000..a855393 --- /dev/null +++ b/tests/test_mathlib_cache_cli.py @@ -0,0 +1,151 @@ +from pathlib import Path +import tarfile + +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): + 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 + + +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 + + +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 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"] diff --git a/tests/test_setup.py b/tests/test_setup.py new file mode 100644 index 0000000..b8aa82e --- /dev/null +++ b/tests/test_setup.py @@ -0,0 +1,488 @@ +import os +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() + + 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"] == "symlink" + + +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", + "symlink", + ]) + 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"] == "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 + + 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 == "symlink" + + MathlibCacheManager().get_local_packages_dir("v4.27.0").mkdir(parents=True, exist_ok=True) + assert config.resolved_dependency_mode == "symlink" + finally: + cache_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 + + 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" + _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}") + + from leanup.repo import mathlib_cache as cache_module + + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + from leanup.repo.manager import LeanRepo + + original_lake_init = LeanRepo.lake_init + original_lake_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" + 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 (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: + 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 + LeanRepo.lake_env_lean = original_lake_env_lean + LeanRepo.lake = original_lake + + +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 + + 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") + return "", "", 0 + + def fake_lake_build(self): + return "", "", 0 + + def fake_lake_env_lean(self, filepath, json=True, options=None, nproc=None): + assert Path(filepath).suffix == ".lean" + return "4.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 + + original_cache_dir = cache_module.LEANUP_CACHE_DIR + cache_module.LEANUP_CACHE_DIR = tmp_path / "cache" + + try: + from leanup.repo.manager import LeanRepo + + original_lake_init = LeanRepo.lake_init + original_lake_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" + _init_fake_package_repo(cached_packages) + + 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" + 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 + 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" + _init_fake_package_repo(cached_packages) + + 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" + _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}") + + 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() + 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" + ).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