tutorial.md

# Kimina Lean Server 离线镜像构建与部署指南

本文档说明如何将 `kimina-lean-server` 打包为完全离线的 Docker 镜像，部署到无公网访问的内部服务器上。

---

## 一、构建思路

### 1.1 为什么要做离线镜像

kimina-lean-server 运行时依赖以下组件，它们在首次启动或运行过程中会尝试联网：

| 组件 | 联网行为 | 离线处理方式 |
|---|---|---|
| **elan** | 安装时下载 Lean 工具链；运行时会检查更新 | 构建时预装工具链；运行时禁用更新检查 |
| **lake** | `lake build` 时从 git 拉取依赖；`lake exe cache get` 下载编译缓存 | 构建时完成所有编译；修改 manifest 为本地 path 类型 |
| **mathlib4** | 依赖众多 Lean 包，需从 GitHub 下载 | 构建时完整克隆并编译，预装入镜像 |
| **Python 依赖** | `pip install` 从 PyPI 下载 | 构建时全部安装到镜像中 |

### 1.2 核心策略：构建时联网，运行时零依赖

整个方案遵循"有网构建、无网运行"的原则：

1. **构建阶段**（在有网络的机器上）：安装 elan、下载 Lean 工具链、克隆 repl 和 mathlib4、编译所有依赖、安装 Python 包
2. **镜像封装**：将编译产物、缓存、依赖全部打入 Docker 镜像
3. **离线阶段**（内部服务器）：仅通过 `docker load` 加载镜像，无需任何外部网络

### 1.3 关键处理点

- **lake-manifest.json 改写**：构建完成后，将 mathlib4 的 `lake-manifest.json` 中所有包的 `type` 从 `"git"` 改为 `"path"`，并删除 `url` 字段。这样 lake 在运行时不会再尝试从 git 拉取依赖
- **elan 自更新禁用**：通过 `ELAN_NO_UPDATE_CHECK=1` 和 `elan config --disable-self-update` 双重保证
- **工具链预装**：构建时通过 `elan-init.sh --default-toolchain v4.26.0` 将工具链固定安装到镜像中

---

## 二、文件说明

### 2.1 `Dockerfile`（仓库根目录）

定义镜像的构建流程，关键步骤：

```dockerfile
# 基础镜像：Python 3.13 slim
FROM python:3.13-slim

# 构建参数：Lean 版本、REPL 源、mathlib 源等
ARG LEAN_SERVER_LEAN_VERSION=v4.26.0
ARG REPL_REPO_URL=https://github.com/leanprover-community/repl.git
ARG REPL_BRANCH=${LEAN_SERVER_LEAN_VERSION}
ARG MATHLIB_REPO_URL=https://github.com/leanprover-community/mathlib4.git
ARG MATHLIB_BRANCH=${LEAN_SERVER_LEAN_VERSION}

# 运行时环境变量
ENV LEAN_SERVER_LEAN_VERSION=${LEAN_SERVER_LEAN_VERSION} \
    LEAN_SERVER_REPL_PATH=/repl/.lake/build/bin/repl \
    LEAN_SERVER_PROJECT_DIR=/mathlib4 \
    LEAN_SERVER_MAX_REPL_MEM=12G \          # 关键：内存限制（见下文注意事项）
    LEAN_SERVER_INIT_REPLS='{"import Mathlib": 1}' \
    ELAN_NO_UPDATE_CHECK=1                   # 禁用 elan 更新检查

# 1. 安装系统依赖（curl, git, jq, build-essential 等）
RUN apt-get update && apt-get install -y ...

# 2. 复制并执行 setup.sh（安装 elan、lean、repl、mathlib4）
COPY setup.sh /usr/local/bin/
RUN sed -i 's/\r$//' /usr/local/bin/setup.sh \   # 修复 Windows CRLF
 && chmod +x /usr/local/bin/setup.sh \
 && /usr/local/bin/setup.sh

# 3. 安装 Python 依赖
RUN pip install ... && prisma generate

# 4. 启动服务
CMD ["python", "-m", "server"]
```

### 2.2 `setup.sh`（仓库根目录）

在容器构建阶段执行，完成 Lean 生态的预装：

```bash
#!/usr/bin/env bash
set -euxo pipefail

# 安装 elan（Lean 工具链管理器）
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
  | sh -s -- --default-toolchain "${LEAN_SERVER_LEAN_VERSION}" -y

# 禁用 elan 自动更新（离线环境必须）
elan config --disable-self-update

# 克隆并编译 REPL
install_repo repl "$REPL_REPO_URL" "$REPL_BRANCH" false

# 克隆并编译 mathlib4
install_repo mathlib4 "$MATHLIB_REPO_URL" "$MATHLIB_BRANCH" true
```

`install_repo` 函数的核心逻辑：

1. `git clone --single-branch --depth 1` 浅克隆仓库
2. `lake exe cache get` 下载 mathlib4 的预编译缓存（加速构建，失败则回退到源码编译）
3. `lake build` 编译项目
4. 对 mathlib4 执行 **manifest 改写**：
   ```bash
   jq '.packages |= map(.type="path"|del(.url)|.dir=".lake/packages/"+.name)' \
      lake-manifest.json
   ```
5. 构建完成后删除 `.git` 目录减小镜像体积

### 2.3 `deploy/offline/build-and-save.sh`

一键构建脚本，执行以下流程：

```
构建镜像
    |
    v
启动容器（--network=none）进行离线冒烟测试
    |
    v
等待 "Initialized REPLs" 日志（最多 10 分钟）
    |
    v
测试通过 → docker save | gzip 导出 tar.gz
```

可覆盖的环境变量：

| 变量 | 默认值 | 说明 |
|---|---|---|
| `LEAN_VERSION` | `v4.26.0` | Lean 版本 |
| `IMAGE` | `kimina-lean-server:${LEAN_VERSION}-offline` | 输出镜像名 |
| `PLATFORM` | `linux/amd64` | 目标平台架构 |
| `APT_MIRROR` | "" | APT 源镜像（国内网络可设阿里云） |
| `PIP_INDEX_URL` | "" | pip 源镜像 |
| `SKIP_UV` | "" | 非空则跳过 uv 安装 |

### 2.4 `deploy/offline/compose.offline.yaml`

离线服务器上的 Docker Compose 配置：

```yaml
services:
  server:
    image: kimina-lean-server:v4.26.0-offline
    ports:
      - "80:8000"
    environment:
      LEAN_SERVER_ENVIRONMENT: prod
      LEAN_SERVER_LEAN_VERSION: v4.26.0
      LEAN_SERVER_MAX_REPL_MEM: 12G       # 与 Dockerfile 保持一致
      LEAN_SERVER_INIT_REPLS: '{"import Mathlib": 1}'
    restart: unless-stopped
```

---

## 三、构建步骤

### 3.1 前置要求

- 一台**有公网访问**的 Linux 机器（架构需与目标服务器一致，通常为 `linux/amd64`）
- Docker 已安装并运行
- Bash、Git 可用

### 3.2 执行构建

```bash
cd deploy/offline
bash build-and-save.sh
```

构建耗时约 10-30 分钟，取决于网络速度。成功后会输出：

```
==> Offline smoke test PASSED
...
==> Done.
  image:        kimina-lean-server:v4.26.0-offline
  image digest: sha256:...
  tar:          .../deploy/offline/out/kimina-lean-server-v4.26.0.tar.gz
  tar sha256:   8e5d3edcc18ace92aa7252329e0a06a24d1b1506b3263042b0138e56de74761f
```

### 3.3 使用国内镜像加速（可选）

如果构建机器在国内，可设置镜像源：

```bash
export APT_MIRROR=https://mirrors.aliyun.com
export PIP_INDEX_URL=https://mirrors.aliyun.com/pypi/simple/
export SKIP_UV=1
bash build-and-save.sh
```

---

## 四、部署步骤

### 4.1 传输文件到内部服务器

将以下两个文件复制到离线服务器：

```
deploy/offline/out/kimina-lean-server-v4.26.0.tar.gz
deploy/offline/compose.offline.yaml
```

### 4.2 加载镜像

在内部服务器上执行：

```bash
# 加载镜像（约 1-3 分钟，取决于磁盘速度）
gunzip -c kimina-lean-server-v4.26.0.tar.gz | docker load

# 验证镜像已加载
docker images | grep kimina-lean-server
```

### 4.3 启动服务

```bash
docker compose -f compose.offline.yaml up -d
```

服务将在后台运行，监听容器的 8000 端口，映射到宿主机的 80 端口。

### 4.4 查看日志

```bash
docker compose -f compose.offline.yaml logs -f
```

预期输出：

```
INFO  Running Kimina Lean Server 'v2.0.0' in prod mode with Lean version: 'v4.26.0'
INFO  REPL manager initialized with: MAX_REPLS=20, MAX_REPL_USES=-1, MAX_REPL_MEM=12288 MB
INFO  Initialized REPLs with: {"import Mathlib": 1}
INFO  Application startup complete.
INFO  Uvicorn running on http://0.0.0.0:8000
```

---

## 五、测试方法

### 5.1 快速功能测试

服务启动后，在离线服务器上执行：

```bash
curl --request POST \
  --url http://localhost:8000/api/check \
  --header 'Content-Type: application/json' \
  --data '{
    "snippets": [
      {"id": "check-nat-test", "code": "#check Nat"}
    ]
  }'
```

预期返回（类似）：

```json
{
  "snippets": [
    {
      "id": "check-nat-test",
      "response": {
        "messages": [
          {
            "severity": "info",
            "pos": {"line": 1, "column": 0},
            "endPos": {"line": 1, "column": 6},
            "data": "Nat : Type"
          }
        ],
        "env": 0
      }
    }
  ]
}
```

### 5.2 离线环境验证

确认容器确实在断网环境下运行：

```bash
# 查看容器网络模式（应为默认 bridge，但无外网访问）
docker inspect <容器名> | grep -i network

# 进入容器内部测试网络连通性
docker exec -it <容器名> bash -c "curl -I https://github.com 2>&1"
# 预期：连接超时或无法解析（证明确实离线）
```

### 5.3 健康检查端点

```bash
curl http://localhost:8000/health
```

预期返回：

```json
{"status": "ok"}
```

---

## 六、注意事项

### 6.1 内存限制（重要）

Lean 4.26.0 + Mathlib 在 REPL 启动时需要大量虚拟内存。测试发现：

| 内存限制 | 结果 |
|---|---|
| 8G | REPL 启动失败（进程被内存限制阻塞） |
| 9G+ | 正常工作 |
| **12G**（推荐） | 稳定运行，留有余量 |

因此 Dockerfile 和 compose 文件中将默认值设为 `12G`。如果你的服务器内存紧张，可尝试降低到 9-10G，但不建议低于 9G。

### 6.2 架构一致性

构建机器的 CPU 架构必须与目标服务器一致。如果不一致，需使用 Docker 的交叉编译：

```bash
# 例如：在 Apple Silicon Mac 上构建 amd64 镜像
export PLATFORM=linux/amd64
bash build-and-save.sh
```

### 6.3 镜像体积

离线镜像体积较大（约 2-3GB），主要来源于：
- mathlib4 预编译产物和依赖包
- Lean 工具链
- REPL 二进制（约 200MB）

### 6.4 版本升级

如需升级 Lean 版本，修改以下位置后重新构建：

1. `Dockerfile` 中的 `LEAN_SERVER_LEAN_VERSION`
2. `compose.offline.yaml` 中的 `LEAN_SERVER_LEAN_VERSION`
3. 重新运行 `build-and-save.sh`

---

## 七、故障排查

| 现象 | 可能原因 | 解决方法 |
|---|---|---|
| 构建时 `env: 'bash\r': No such file or directory` | setup.sh 有 Windows CRLF 换行符 | Dockerfile 中已添加 `sed -i 's/\r$//'` 自动修复 |
| 离线启动时 REPL 返回空响应 | 内存限制过低 | 提高 `LEAN_SERVER_MAX_REPL_MEM` 到 12G |
| `lake exe cache get` 失败 | 网络问题或 lake 版本不兼容 | setup.sh 中已添加 `|| true` 容错，会回退到源码编译 |
| 容器启动后立刻退出 | REPL 初始化失败 | 查看 `docker logs` 中的错误信息 |
| elan 尝试联网更新 | 环境变量未生效 | 检查 `ELAN_NO_UPDATE_CHECK=1` 是否设置 |