diff --git a/docs/en/getting-started/quickstart.md b/docs/en/getting-started/quickstart.md new file mode 100644 index 0000000..2eec021 --- /dev/null +++ b/docs/en/getting-started/quickstart.md @@ -0,0 +1,181 @@ +# 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/index.md b/docs/en/index.md similarity index 100% rename from docs/index.md rename to docs/en/index.md diff --git a/docs/zh/getting-started/quickstart.md b/docs/zh/getting-started/quickstart.md new file mode 100644 index 0000000..c21de39 --- /dev/null +++ b/docs/zh/getting-started/quickstart.md @@ -0,0 +1,181 @@ +# 快速开始 + +## 安装 + +```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.zh.md b/docs/zh/index.md similarity index 96% rename from docs/index.zh.md rename to docs/zh/index.md index 8194c60..83a40c7 100644 --- a/docs/index.zh.md +++ b/docs/zh/index.md @@ -11,7 +11,7 @@ ## 快速开始 -查看[快速开始](getting-started/quickstart.zh.md)指南,开始使用 LeanUp。 +查看[快速开始](getting-started/quickstart.md)指南,开始使用 LeanUp。 ## 命令行界面 diff --git a/mkdocs.yml b/mkdocs.yml index 0e56f57..bc76441 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -41,7 +41,7 @@ theme: plugins: - search - i18n: - docs_structure: suffix + docs_structure: folder fallback_to_default: true reconfigure_material: true reconfigure_search: true