Metadata-Version: 2.4
Name: leanup
Version: 0.2.2
Summary: Python package for Lean Environment Management
Author: Lean-zh Community
Author-email: leanprover@outlook.com
Maintainer: Lean-zh Community
Maintainer-email: leanprover@outlook.com
License: MIT license
Requires-Python: >=3.6
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: gitpython
Requires-Dist: psutil
Requires-Dist: toml
Requires-Dist: click
Requires-Dist: platformdirs
Requires-Dist: loguru
Requires-Dist: requests
Requires-Dist: colorama
Requires-Dist: fastapi
Requires-Dist: uvicorn
Provides-Extra: dev
Requires-Dist: coverage; extra == "dev"
Requires-Dist: mypy; extra == "dev"
Requires-Dist: pytest; extra == "dev"
Requires-Dist: ruff; extra == "dev"
Requires-Dist: mkdocs>=1.4.0; extra == "dev"
Requires-Dist: mkdocs-material>=9.0.0; extra == "dev"
Requires-Dist: mkdocs-static-i18n>=0.5.0; extra == "dev"
Requires-Dist: pytest>=7.0.0; extra == "dev"
Requires-Dist: pytest-cov>=4.0.0; extra == "dev"
Dynamic: license-file

# LeanUp

<div align="center">
    <a href="https://pypi.python.org/pypi/leanup">
        <img src="https://img.shields.io/pypi/v/leanup.svg" alt="PyPI version" />
    </a>
    <a href="https://github.com/Lean-zh/LeanUp/actions/workflows/ci.yaml">
        <img src="https://github.com/Lean-zh/LeanUp/actions/workflows/ci.yaml/badge.svg" alt="Tests" />
    </a>
    <a href="https://codecov.io/gh/Lean-zh/LeanUp">
        <img src="https://codecov.io/gh/Lean-zh/LeanUp/branch/main/graph/badge.svg" alt="Coverage" />
    </a>
</div>

<div align="center">

**一个用于管理 Lean 数学证明语言环境的 Python 工具**

</div>

## 🎯 功能特性

- **📦 仓库管理**: 安装和管理 Lean 仓库，支持命令优先、交互兜底的配置流程
- **⚡ 项目初始化**: 快速创建固定 Lean 版本的项目，并复用同版本 mathlib 缓存
- **🌍 跨平台支持**: 支持 Linux、macOS 和 Windows
- **📦 简单易用**: 通过 `pip install leanup` 快速安装

## 🚀 快速开始

### 安装

```bash
# 从 PyPI 安装
pip install leanup 

# 或者克隆仓库后安装
git clone https://github.com/Lean-zh/LeanUp.git
cd LeanUp
pip install -e .
```

### 基础使用

```bash
# 查看帮助
leanup --help

# 快速初始化一个 Lean + mathlib 项目
leanup setup ./Demo --lean-version v4.27.0

```

## 📖 详细使用指南

### 仓库管理

```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 -I leanprover-community/mathlib4

# 指定要构建的包
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
```

### 快速初始化项目

`leanup setup` 用于快速创建一个固定 Lean 版本的项目，并按需要为 `mathlib` 依赖准备共享缓存。

```bash
# 创建一个带 mathlib 的项目，默认有缓存就复用，没有缓存就自动准备缓存
leanup setup ./Demo --lean-version v4.27.0

# 使用 copy 模式，把共享缓存复制到项目里
leanup setup ./DemoCopy --lean-version v4.27.0 --dependency-mode copy

# 后续同版本项目可直接软链接复用缓存
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` 和 `copy`
- 默认缓存目录为 `LEANUP_CACHE_DIR/mathlib/packages/<version>/packages`
- 如果已有 `packages` 缓存，则按 `symlink` 或 `copy` 的方式放进项目
- 如果缓存不存在，则会自动执行 `lake update`、`lake exe cache get`，再把 `.lake/packages` 写回缓存
- `setup` 会确保对应 Lean toolchain 已通过 `elan` 安装

### 管理 mathlib 缓存

```bash
# 查看 LeanUp 已有缓存版本
leanup cache list

# 查看远端服务已有缓存版本和下载 URL
leanup cache list --base-url http://127.0.0.1:8000

# 在临时目录创建某个 Lean 版本对应的共享 mathlib packages 缓存
leanup cache create v4.22.0

# 将本地缓存里的 packages/<version>/packages 打包成 archives/<version>/packages.tar.gz
leanup cache pack v4.22.0

# 或者使用指定缓存根
leanup cache pack v4.22.0 --output-dir /path/to/cache

# 从 LeanUp cache 服务下载 packages.tar.gz，并解压到本地缓存根
leanup cache get v4.22.0 --base-url http://127.0.0.1:8000

# 启动本地缓存服务：
# - /f/... 路由给 lake exe cache get 使用
# - /packages/... 路由给 leanup cache get 使用
leanup cache serve

# 让 mathlib 官方 cache client 改走 LeanUp 服务
export MATHLIB_CACHE_GET_URL=http://127.0.0.1:8000
lake exe cache get

# 如需关闭并发压缩，可以显式禁用 pigz
leanup cache pack v4.22.0 --output-dir /path/to/cache --no-pigz
```

- 默认会在本机存在 `pigz` 时启用并发压缩
- 如果系统里没有 `pigz`，命令会自动回退到普通 gzip 打包
- `--no-pigz` 可显式关闭并发压缩
- `leanup cache create` 会在 `tempfile` 临时工作目录中执行 `lake update` 和 `lake exe cache get`，然后把 `.lake/packages` 回填到 `mathlib/packages/<version>/packages`，再生成 `mathlib/archives/<version>/packages.tar.gz`
- `leanup cache pack` 会从 `mathlib/packages/<version>/packages` 生成 `mathlib/archives/<version>/packages.tar.gz`
- `leanup cache get` 会下载远端 `packages.tar.gz` 到 `mathlib/archives/<version>/packages.tar.gz`，并解压到 `mathlib/packages/<version>/packages`
- `leanup cache get` 和 `leanup cache pack` 都通过临时文件 / 临时目录完成后再原子替换，避免中途中断破坏缓存
- `leanup cache serve` 使用 FastAPI/uvicorn 提供服务，并暴露 `/packages/mathlib/index.json` 让其他机器列出远端可用版本

### 交互式安装

使用 `leanup repo install -i` 时，您可以配置：

- 仓库名称（必需）
- 仓库源的基础 URL
- 分支或标签
- 存储仓库的目标目录
- 自定义目标名称
- 是否在克隆后运行 `lake update`
- 是否在克隆后运行 `lake build`
- 要编译的特定构建包
- 是否覆盖现有目录

默认规则：

- 命令优先，交互兜底
- 缺必要参数时自动进入交互
- `-i` 强制交互
- `-I` 禁止交互，参数不足时直接报错

### 编程接口

#### 使用 InstallConfig

```python
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
)

# 执行安装
config.install()
```

#### 使用 RepoManager

```python
from leanup.repo.manager import RepoManager

# 创建仓库管理器
repo = RepoManager("/path/to/directory")

# 克隆仓库
repo.clone_from("https://github.com/owner/repo.git", branch="main")

# 文件操作
repo.write_file("test.txt", "Hello world")
content = repo.read_file("test.txt")
repo.edit_file("test.txt", "world", "universe")

# 列出文件和目录
files = repo.list_files("*.lean")
dirs = repo.list_dirs()
```

#### 使用 LeanRepo

```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: {info['has_lakefile_toml']}")

# Lake 操作
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")
```

## 🛠️ 开发

仓库级开发规范见：

- `AGENTS.md`
- `DEVELOP.md`

### 环境设置

```bash
# 克隆仓库
git clone https://github.com/Lean-zh/LeanUp.git
cd LeanUp

# 安装开发依赖
pip install -e ".[dev]"

# 安装项目（可编辑模式）
pip install -e .
```

### 运行测试

```bash
# 运行所有测试
pytest tests/ -v

# 运行测试并生成覆盖率报告
coverage run -m pytest tests/
coverage report -m
```

## ⚙️ 配置

LeanUp 使用位于 `~/.leanup/config.yaml` 的配置文件。您可以自定义：

- 默认仓库源
- 仓库缓存目录
- elan 自动安装设置
- 仓库前缀和基础 URL

## 🌍 跨平台支持

LeanUp 在以下平台上经过测试：

- **Linux**: Ubuntu 20.04+, CentOS 7+, Debian 10+
- **macOS**: macOS 10.15+（Intel 和 Apple Silicon）
- **Windows**: Windows 10+

## 📊 项目状态

| 功能 | 状态 | 说明 |
|------|------|------|
| elan 安装 | ✅ | 支持自动检测平台和版本 |
| 命令代理 | ✅ | 透明传递所有 elan 命令 |
| 仓库管理 | ✅ | 安装和管理 Lean 仓库 |
| 交互式配置 | ✅ | 用户友好的设置过程 |
| 跨平台支持 | ✅ | Linux/macOS/Windows |
| 单元测试 | ✅ | 覆盖率 > 85% |
| CI/CD | ✅ | GitHub Actions 多平台测试 |

## 🤝 贡献

欢迎贡献代码！请查看 [贡献指南](CONTRIBUTING.md) 了解详细信息。

## 📝 许可证

本项目采用 MIT 许可证。详细信息请查看 [LICENSE](LICENSE) 文件。

## 🔗 相关链接

- [Lean 官方网站](https://leanprover.github.io/)
- [Lean 社区文档](https://leanprover-community.github.io/)
- [elan 工具链管理器](https://github.com/leanprover/elan)
