From 6c4c43472fb7e898b3a8e79f6e21c1ddf651665b Mon Sep 17 00:00:00 2001
From: rex <1073853456@qq.com>
Date: Tue, 7 Jul 2026 14:18:39 +0800
Subject: [PATCH 1/2] docs: add intranet environment restore skill

---
 .../SKILL.md                                  | 172 ++++++++++++++++++
 .../scripts/consumer-restore-version.sh       |  60 ++++++
 .../scripts/consumer-verify-version.sh        |  28 +++
 .../scripts/provider-pack-version.sh          |  71 ++++++++
 .../scripts/provider-serve-assets.sh          |  44 +++++
 .../scripts/provider-verify-assets.sh         |  24 +++
 mkdocs.yml                                    |   2 +
 7 files changed, 401 insertions(+)
 create mode 100644 docs/skills/leanup-environment-pack-serve-restore/SKILL.md
 create mode 100755 docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
 create mode 100755 docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
 create mode 100755 docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
 create mode 100755 docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
 create mode 100755 docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh

diff --git a/docs/skills/leanup-environment-pack-serve-restore/SKILL.md b/docs/skills/leanup-environment-pack-serve-restore/SKILL.md
new file mode 100644
index 0000000..04f5e54
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/SKILL.md
@@ -0,0 +1,172 @@
+---
+name: leanup-environment-pack-serve-restore
+description: Pack a Lean/Mathlib environment on one machine, serve the Lean assets from cache/serve, and restore them on another machine without public-network access for Lean-related actions.
+version: 0.1.0
+updated: 2026-07-07
+---
+
+# LeanUp 环境打包、Serve 与恢复
+
+用于一台 provider 机器已经有可用 Lean/Mathlib 环境，需要把同一版本提供给另一台 consumer 机器恢复的场景。
+
+这个 skill 的边界是 Lean 环境资产，不是 Python 工具安装：
+
+- LeanUp 自身是普通 Python CLI，作为前置条件安装或升级，可以使用常规 Python/package 网络环境。
+- 从 `leanup init --server ...` 之后的 Lean 相关动作应能只依赖 provider 的 `cache/serve`，不访问 GitHub、Elan 官方源、Mathlib 远端仓库或其它公网 Lean 资源。
+
+## 默认目录契约
+
+默认不要另起奇怪的 serve 目录。LeanUp 的默认路径必须和 `init`、`get`、`unpack`、`install`、`setup` 的客户端行为保持一致：
+
+```text
+$HOME/.leanup/cache/serve/      # leanup serve 的默认源目录
+$HOME/.leanup/cache/local/      # consumer 本地可复用 cache
+$HOME/.leanup/cache/downloads/  # 下载/校验 staging
+```
+
+`cache/serve` 的 HTTP 布局固定为：
+
+```text
+/elan/base/elan-base.tar.gz
+/lean/<version>/toolchain.tar.gz
+/mathlib/<version>/mathlib-lake.tar.gz
+```
+
+不要把这些内容放进 `cache/serve`：
+
+```text
+scripts/
+project-files/
+Python wheel/package artifacts
+*-pack-source/
+```
+
+如果确实需要非默认发布目录，只能通过显式参数或环境变量覆盖；调试和标准流程应优先使用默认 `~/.leanup/cache/serve`。
+
+## 随附脚本
+
+脚本位于本目录的 `scripts/` 下：
+
+```text
+provider-pack-version.sh     # provider: 打包 Elan、Lean toolchain、Mathlib .lake
+provider-serve-assets.sh     # provider: 从 ~/.leanup/cache/serve 启动静态文件服务
+provider-verify-assets.sh    # provider: 校验本地文件和 HTTP 可访问性
+consumer-restore-version.sh  # consumer: 使用已安装 LeanUp 从 provider 恢复 Lean 环境
+consumer-verify-version.sh   # consumer: 校验恢复结果
+```
+
+## Provider: 打包资产
+
+前置条件：
+
+- provider 已安装 LeanUp。
+- provider 的 `ELAN_HOME` 中已有目标 Lean 版本。
+- provider 能准备一个可用的 Mathlib workspace。
+- 大归档建议安装 `pigz`。
+
+示例：
+
+```bash
+export VERSION=v4.30.0
+export LEANUP=leanup
+export ELAN_HOME=$HOME/.elan
+export PROJECT_ROOT=$HOME/leanup-provider-projects
+
+./scripts/provider-pack-version.sh "$VERSION"
+```
+
+脚本会在默认位置生成：
+
+```text
+~/.leanup/cache/serve/elan/base/elan-base.tar.gz
+~/.leanup/cache/serve/lean/v4.30.0/toolchain.tar.gz
+~/.leanup/cache/serve/mathlib/v4.30.0/mathlib-lake.tar.gz
+```
+
+Mathlib portable archive 必须来自 copy-mode 的 `.lake` source。不要把绝对 symlink workspace 直接打包，也不要把 `*-pack-source` 常驻留在项目目录里。脚本会使用临时 copy-mode workspace，完成后自动清理。
+
+## Provider: 启动 serve
+
+默认 serve root 是 `~/.leanup/cache/serve`：
+
+```bash
+export HOST=0.0.0.0
+export PORT=8765
+./scripts/provider-serve-assets.sh
+```
+
+如果机器 IP 是 `PROVIDER_HOST`，consumer 使用：
+
+```text
+http://PROVIDER_HOST:8765
+```
+
+校验 provider：
+
+```bash
+export SERVER=http://127.0.0.1:8765
+./scripts/provider-verify-assets.sh v4.30.0
+```
+
+## Consumer: 恢复 Lean 环境
+
+前置条件：consumer 已安装 LeanUp。
+
+```bash
+export VERSION=v4.30.0
+export SERVER=http://PROVIDER_HOST:8765
+export LEANUP=leanup
+export ELAN_HOME=$HOME/.elan
+
+./scripts/consumer-restore-version.sh "$VERSION"
+```
+
+脚本会：
+
+1. 检查 LeanUp 已存在。
+2. 设置 provider host 到 `no_proxy`。
+3. 把公共代理指向不可用地址，证明 Lean 相关动作不需要公网。
+4. 从 provider 获取 Elan base 和 Lean toolchain。
+5. 从 provider 获取 Mathlib `.lake` archive。
+6. 执行 `mathlib unpack/setup/check`。
+
+期望输出包含：
+
+```text
+elan <version>
+Lean (version v4.30.0, ...)
+import Mathlib ok
+lean-related offline restore ok
+```
+
+## 校验边界
+
+为了确认没有使用公网 Lean 资源，consumer 恢复时可设置：
+
+```bash
+export no_proxy="PROVIDER_HOST,127.0.0.1,localhost,${no_proxy:-}"
+export NO_PROXY="$no_proxy"
+export http_proxy=http://127.0.0.1:9
+export https_proxy=http://127.0.0.1:9
+export all_proxy=http://127.0.0.1:9
+```
+
+这样 provider 的 `cache/serve` 仍可访问，而任何意外公网访问都会失败。
+
+## 安全规则
+
+- 不要在 skill、脚本或日志里写入 token、password、proxy auth、API key。
+- 不要把带认证的 proxy 环境输出打印进日志。
+- 不要把机器私有路径作为默认值写死；使用 `$HOME`、`ELAN_HOME`、`SERVER`、`PROJECT_ROOT` 等变量。
+- 不要把 LeanUp wheel 放进 `cache/serve` 作为标准资产；LeanUp 自身是普通 Python 前置条件。
+- 不要依赖持久 `~/.leanup/tmp`；临时工作区应由命令或脚本自己清理。
+- 目录级原子替换的 staging 应和目标目录在同一 filesystem。
+
+## 已验证边界
+
+这套流程已用一个 provider 和一个 consumer 验证过：
+
+- provider 从默认 `~/.leanup/cache/serve` 提供三类 Lean 资产。
+- consumer 使用预装 LeanUp。
+- consumer 从 `leanup init --server ...` 开始设置死代理，仅 provider host 走 `no_proxy`。
+- Elan、Lean toolchain、Mathlib `.lake` 恢复和 `import Mathlib` 校验通过。
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh b/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
new file mode 100755
index 0000000..7325f43
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+VERSION="${1:-${VERSION:-v4.30.0}}"
+SERVER="${SERVER:?Set SERVER to the provider URL, for example http://PROVIDER_HOST:8765}"
+LEANUP="${LEANUP:-leanup}"
+ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
+CHECK_ROOT="${CHECK_ROOT:-$HOME/leanup-check-$VERSION}"
+TMPDIR="${TMPDIR:-$HOME/.cache/leanup-runtime-tmp}"
+
+export PATH="$ELAN_HOME/bin:$PATH"
+export TMPDIR
+mkdir -p "$TMPDIR"
+
+provider_host=$(printf '%s\n' "$SERVER" | sed -E 's#^[a-zA-Z]+://([^/:]+).*#\1#')
+export no_proxy="$provider_host,127.0.0.1,localhost,${no_proxy:-}"
+export NO_PROXY="$no_proxy"
+
+# LeanUp is a normal Python tool prerequisite. The no-public-network boundary
+# starts at Lean-related environment restore actions below.
+test -x "$(command -v "$LEANUP")"
+"$LEANUP" --version
+
+# The provider server is reachable through no_proxy; accidental public-network
+# access fails fast.
+export http_proxy=http://127.0.0.1:9
+export https_proxy=http://127.0.0.1:9
+export all_proxy=http://127.0.0.1:9
+
+"$LEANUP" init --server "$SERVER"
+"$LEANUP" elan get --server "$SERVER"
+"$LEANUP" elan unpack --elan-home "$ELAN_HOME"
+"$LEANUP" lean get "$VERSION" --server "$SERVER"
+"$LEANUP" lean unpack "$VERSION" --elan-home "$ELAN_HOME"
+"$LEANUP" elan check --elan-home "$ELAN_HOME"
+"$LEANUP" lean check "$VERSION" --elan-home "$ELAN_HOME"
+
+archive="$HOME/.leanup/cache/serve/mathlib/$VERSION/mathlib-lake.tar.gz"
+mkdir -p "$(dirname "$archive")"
+curl --noproxy "$provider_host,127.0.0.1,localhost" --fail --location \
+  --output "$archive.tmp" "$SERVER/mathlib/$VERSION/mathlib-lake.tar.gz"
+mv "$archive.tmp" "$archive"
+
+"$LEANUP" mathlib unpack "$VERSION"
+rm -rf "$CHECK_ROOT"
+"$LEANUP" mathlib setup "$CHECK_ROOT" \
+  --lean-version "$VERSION" \
+  --name MathlibCheck \
+  --dependency-mode symlink \
+  --force \
+  -I
+"$LEANUP" mathlib check "$VERSION" --source "$CHECK_ROOT"
+
+if find "$TMPDIR" -maxdepth 1 -mindepth 1 | grep -q .; then
+  echo "unexpected temporary residue in $TMPDIR" >&2
+  find "$TMPDIR" -maxdepth 2 -mindepth 1 >&2
+  exit 1
+fi
+
+echo "lean-related offline restore ok for $VERSION via $SERVER"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh b/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
new file mode 100755
index 0000000..7676a95
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+VERSION="${1:-${VERSION:-v4.30.0}}"
+LEANUP="${LEANUP:-leanup}"
+ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
+CHECK_ROOT="${CHECK_ROOT:-$HOME/leanup-check-$VERSION}"
+TMPDIR="${TMPDIR:-$HOME/.cache/leanup-runtime-tmp}"
+
+export PATH="$ELAN_HOME/bin:$PATH"
+export http_proxy=http://127.0.0.1:9
+export https_proxy=http://127.0.0.1:9
+export all_proxy=http://127.0.0.1:9
+
+"$LEANUP" --version
+"$LEANUP" elan check --elan-home "$ELAN_HOME"
+"$LEANUP" lean check "$VERSION" --elan-home "$ELAN_HOME"
+"$ELAN_HOME/toolchains/leanprover--lean4---$VERSION/bin/lake" --version
+"$LEANUP" mathlib check "$VERSION" --source "$CHECK_ROOT"
+
+test -L "$CHECK_ROOT/.lake" || test -d "$CHECK_ROOT/.lake"
+if [ -d "$TMPDIR" ] && find "$TMPDIR" -maxdepth 1 -mindepth 1 | grep -q .; then
+  echo "unexpected temporary residue in $TMPDIR" >&2
+  find "$TMPDIR" -maxdepth 2 -mindepth 1 >&2
+  exit 1
+fi
+
+echo "consumer verification ok for $VERSION"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
new file mode 100755
index 0000000..5351eb3
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+VERSION="${1:-${VERSION:-v4.30.0}}"
+LEANUP="${LEANUP:-leanup}"
+ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
+PROJECT_ROOT="${PROJECT_ROOT:-$HOME/leanup-provider-projects}"
+SERVE_ROOT="${SERVE_ROOT:-$HOME/.leanup/cache/serve}"
+LOG="${LOG:-$HOME/.leanup/logs/provider-pack-${VERSION}.log}"
+PACK_WORK_ROOT="${PACK_WORK_ROOT:-${TMPDIR:-/tmp}}"
+PACK_WORK_DIR=""
+
+cleanup_pack_work() {
+  if [ -n "$PACK_WORK_DIR" ] && [ -d "$PACK_WORK_DIR" ]; then
+    rm -rf "$PACK_WORK_DIR"
+  fi
+}
+trap cleanup_pack_work EXIT
+
+export PATH="$ELAN_HOME/bin:$PATH"
+export TMPDIR="${TMPDIR:-/tmp}"
+export TMP_DIR="${TMP_DIR:-$TMPDIR}"
+
+mkdir -p "$PROJECT_ROOT" "$SERVE_ROOT" "$(dirname "$LOG")"
+{
+  echo "[$(date -Is)] provider pack start version=$VERSION host=$(hostname)"
+  echo "leanup=$LEANUP"
+  echo "elan_home=$ELAN_HOME"
+  echo "project_root=$PROJECT_ROOT"
+  echo "serve_root=$SERVE_ROOT"
+  echo "tmpdir=$TMPDIR tmp_dir=$TMP_DIR"
+  command -v pigz || true
+  nproc || true
+} | tee -a "$LOG"
+
+"$LEANUP" lean check "$VERSION" --elan-home "$ELAN_HOME" | tee -a "$LOG"
+"$LEANUP" elan pack --elan-home "$ELAN_HOME" | tee -a "$LOG"
+"$LEANUP" lean pack "$VERSION" --elan-home "$ELAN_HOME" | tee -a "$LOG"
+
+# Optional provider workspace for local use. It is not the portable pack source.
+SOURCE_DIR="$PROJECT_ROOT/$VERSION"
+"$LEANUP" mathlib setup "$SOURCE_DIR" \
+  --lean-version "$VERSION" \
+  --name MathlibProvider \
+  --dependency-mode symlink \
+  --force \
+  -I 2>&1 | tee -a "$LOG"
+
+# Portable .lake archives must come from a copy-mode source. Keep it temporary.
+mkdir -p "$PACK_WORK_ROOT"
+PACK_WORK_DIR=$(mktemp -d "$PACK_WORK_ROOT/leanup-pack-${VERSION}.XXXXXX")
+PACK_SOURCE_DIR="$PACK_WORK_DIR/MathlibPack"
+"$LEANUP" mathlib setup "$PACK_SOURCE_DIR" \
+  --lean-version "$VERSION" \
+  --name MathlibPack \
+  --dependency-mode copy \
+  --force \
+  -I 2>&1 | tee -a "$LOG"
+
+"$LEANUP" mathlib check "$VERSION" --source "$PACK_SOURCE_DIR" | tee -a "$LOG"
+"$LEANUP" mathlib pack "$VERSION" --source "$PACK_SOURCE_DIR" | tee -a "$LOG"
+
+for required in \
+  "$SERVE_ROOT/elan/base/elan-base.tar.gz" \
+  "$SERVE_ROOT/lean/$VERSION/toolchain.tar.gz" \
+  "$SERVE_ROOT/mathlib/$VERSION/mathlib-lake.tar.gz"; do
+  test -s "$required"
+done
+
+find "$SERVE_ROOT" -maxdepth 5 -type f -printf '%p %s bytes\n' | sort | tee -a "$LOG"
+echo "[$(date -Is)] provider pack done version=$VERSION" | tee -a "$LOG"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
new file mode 100755
index 0000000..d1b773b
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
@@ -0,0 +1,44 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+HOST="${HOST:-0.0.0.0}"
+PORT="${PORT:-8765}"
+ROOT="${ROOT:-$HOME/.leanup/cache/serve}"
+LOG="${LOG:-$HOME/.leanup/logs/provider-serve.log}"
+PIDFILE="${PIDFILE:-$HOME/.leanup/state/locks/leanup-asset-server.pid}"
+PYTHON="${PYTHON:-python3}"
+
+mkdir -p "$ROOT" "$(dirname "$LOG")" "$(dirname "$PIDFILE")"
+
+running_pid=""
+if [ -f "$PIDFILE" ]; then
+  candidate=$(cat "$PIDFILE" 2>/dev/null || true)
+  if [ -n "$candidate" ] && kill -0 "$candidate" 2>/dev/null; then
+    running_pid="$candidate"
+  fi
+fi
+
+start_server() {
+  cd "$ROOT"
+  nohup "$PYTHON" -m http.server "$PORT" --bind "$HOST" >"$LOG" 2>&1 &
+  echo $! > "$PIDFILE"
+  echo "started pid=$(cat "$PIDFILE") root=$ROOT port=$PORT"
+}
+
+if [ -n "$running_pid" ]; then
+  running_root=$(readlink "/proc/$running_pid/cwd" 2>/dev/null || true)
+  if [ "$running_root" = "$ROOT" ]; then
+    echo "already running: pid=$running_pid root=$ROOT port=$PORT"
+  else
+    echo "restarting: pid=$running_pid old_root=$running_root new_root=$ROOT port=$PORT"
+    kill "$running_pid"
+    sleep 1
+    start_server
+  fi
+else
+  start_server
+fi
+
+sleep 1
+curl --noproxy '*' -sS "http://127.0.0.1:$PORT/" >/dev/null
+echo "local check ok: http://127.0.0.1:$PORT/ root=$ROOT"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
new file mode 100755
index 0000000..38006bf
--- /dev/null
+++ b/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+VERSION="${1:-${VERSION:-v4.30.0}}"
+SERVER="${SERVER:-http://127.0.0.1:8765}"
+ROOT="${ROOT:-$HOME/.leanup/cache/serve}"
+
+paths=(
+  "elan/base/elan-base.tar.gz"
+  "lean/$VERSION/toolchain.tar.gz"
+  "mathlib/$VERSION/mathlib-lake.tar.gz"
+)
+
+for path in "${paths[@]}"; do
+  file="$ROOT/$path"
+  test -s "$file"
+  printf 'local %s %s bytes\n' "$path" "$(stat -c '%s' "$file")"
+  curl --noproxy '*' --fail -sSI "$SERVER/$path" \
+    | awk -v p="$path" 'NR==1 {printf "http %s %s ", p, $0} tolower($1)=="content-length:" {print $0}'
+done
+
+tar -tzf "$ROOT/lean/$VERSION/toolchain.tar.gz" | sed -n '1,3p' >/dev/null
+tar -tzf "$ROOT/mathlib/$VERSION/mathlib-lake.tar.gz" | sed -n '1,3p' >/dev/null
+echo "provider asset verification ok for $VERSION via $SERVER"
diff --git a/mkdocs.yml b/mkdocs.yml
index 1d05512..aba601d 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -71,4 +71,6 @@ nav:
   - 首页: index.md
   - 开始使用:
     - 快速开始: getting-started/quickstart.md
+  - Skills:
+    - 环境打包与内网恢复: skills/leanup-environment-pack-serve-restore/SKILL.md
   # - API Reference: api-reference.md

From 0787aca251060eb8e4ae5303d67960381d75e400 Mon Sep 17 00:00:00 2001
From: Rex <85153659+LooKeng@users.noreply.github.com>
Date: Tue, 7 Jul 2026 16:09:37 +0800
Subject: [PATCH 2/2] docs: move environment restore skill to root skills

---
 mkdocs.yml                                           |  2 --
 skills/README.md                                     |  9 +++++++++
 .../leanup-environment-pack-serve-restore/SKILL.md   | 12 +++++++++---
 .../scripts/consumer-restore-version.sh              |  5 ++++-
 .../scripts/consumer-verify-version.sh               |  3 +++
 .../scripts/provider-pack-version.sh                 |  5 ++++-
 .../scripts/provider-serve-assets.sh                 |  4 +++-
 .../scripts/provider-verify-assets.sh                |  4 +++-
 8 files changed, 35 insertions(+), 9 deletions(-)
 create mode 100644 skills/README.md
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/SKILL.md (89%)
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh (90%)
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh (87%)
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh (92%)
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh (89%)
 rename {docs/skills => skills}/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh (83%)

diff --git a/mkdocs.yml b/mkdocs.yml
index aba601d..1d05512 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -71,6 +71,4 @@ nav:
   - 首页: index.md
   - 开始使用:
     - 快速开始: getting-started/quickstart.md
-  - Skills:
-    - 环境打包与内网恢复: skills/leanup-environment-pack-serve-restore/SKILL.md
   # - API Reference: api-reference.md
diff --git a/skills/README.md b/skills/README.md
new file mode 100644
index 0000000..782c695
--- /dev/null
+++ b/skills/README.md
@@ -0,0 +1,9 @@
+# LeanUp Skills
+
+This directory contains reusable operational skills for LeanUp maintainers and operators.
+
+Available skills:
+
+- `leanup-environment-pack-serve-restore/` — pack Lean environment assets on a provider machine, serve them from LeanUp's default `~/.leanup/cache/serve`, and restore them on a consumer machine without public-network access for Lean-related actions.
+
+These skills are documentation and operational scripts. They are not imported by the LeanUp Python package at runtime.
diff --git a/docs/skills/leanup-environment-pack-serve-restore/SKILL.md b/skills/leanup-environment-pack-serve-restore/SKILL.md
similarity index 89%
rename from docs/skills/leanup-environment-pack-serve-restore/SKILL.md
rename to skills/leanup-environment-pack-serve-restore/SKILL.md
index 04f5e54..1cfb28e 100644
--- a/docs/skills/leanup-environment-pack-serve-restore/SKILL.md
+++ b/skills/leanup-environment-pack-serve-restore/SKILL.md
@@ -41,7 +41,7 @@ Python wheel/package artifacts
 *-pack-source/
 ```
 
-如果确实需要非默认发布目录，只能通过显式参数或环境变量覆盖；调试和标准流程应优先使用默认 `~/.leanup/cache/serve`。
+如果确实需要非默认目录，优先显式设置 `LEANUP_HOME` 或 `LEANUP_CACHE_DIR`，让 provider 和 consumer 都从同一套 LeanUp cache 规则推导路径；调试和标准流程应优先使用默认 `~/.leanup/cache/serve`。
 
 ## 随附脚本
 
@@ -71,6 +71,9 @@ export VERSION=v4.30.0
 export LEANUP=leanup
 export ELAN_HOME=$HOME/.elan
 export PROJECT_ROOT=$HOME/leanup-provider-projects
+# Optional when using a non-default LeanUp home/cache:
+# export LEANUP_HOME=$HOME/.leanup
+# export LEANUP_CACHE_DIR=$LEANUP_HOME/cache
 
 ./scripts/provider-pack-version.sh "$VERSION"
 ```
@@ -117,6 +120,9 @@ export VERSION=v4.30.0
 export SERVER=http://PROVIDER_HOST:8765
 export LEANUP=leanup
 export ELAN_HOME=$HOME/.elan
+# Optional when using a non-default LeanUp home/cache:
+# export LEANUP_HOME=$HOME/.leanup
+# export LEANUP_CACHE_DIR=$LEANUP_HOME/cache
 
 ./scripts/consumer-restore-version.sh "$VERSION"
 ```
@@ -134,9 +140,9 @@ export ELAN_HOME=$HOME/.elan
 
 ```text
 elan <version>
-Lean (version v4.30.0, ...)
+Lean (version 4.30.0, ...)
 import Mathlib ok
-lean-related offline restore ok
+lean-related offline restore ok for <version> via <server>
 ```
 
 ## 校验边界
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh b/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
similarity index 90%
rename from docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
rename to skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
index 7325f43..0eb8a2f 100755
--- a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
+++ b/skills/leanup-environment-pack-serve-restore/scripts/consumer-restore-version.sh
@@ -5,9 +5,12 @@ VERSION="${1:-${VERSION:-v4.30.0}}"
 SERVER="${SERVER:?Set SERVER to the provider URL, for example http://PROVIDER_HOST:8765}"
 LEANUP="${LEANUP:-leanup}"
 ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
+LEANUP_HOME="${LEANUP_HOME:-$HOME/.leanup}"
+LEANUP_CACHE_DIR="${LEANUP_CACHE_DIR:-$LEANUP_HOME/cache}"
 CHECK_ROOT="${CHECK_ROOT:-$HOME/leanup-check-$VERSION}"
 TMPDIR="${TMPDIR:-$HOME/.cache/leanup-runtime-tmp}"
 
+export LEANUP_HOME LEANUP_CACHE_DIR
 export PATH="$ELAN_HOME/bin:$PATH"
 export TMPDIR
 mkdir -p "$TMPDIR"
@@ -35,7 +38,7 @@ export all_proxy=http://127.0.0.1:9
 "$LEANUP" elan check --elan-home "$ELAN_HOME"
 "$LEANUP" lean check "$VERSION" --elan-home "$ELAN_HOME"
 
-archive="$HOME/.leanup/cache/serve/mathlib/$VERSION/mathlib-lake.tar.gz"
+archive="$LEANUP_CACHE_DIR/serve/mathlib/$VERSION/mathlib-lake.tar.gz"
 mkdir -p "$(dirname "$archive")"
 curl --noproxy "$provider_host,127.0.0.1,localhost" --fail --location \
   --output "$archive.tmp" "$SERVER/mathlib/$VERSION/mathlib-lake.tar.gz"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh b/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
similarity index 87%
rename from docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
rename to skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
index 7676a95..965b60f 100755
--- a/docs/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
+++ b/skills/leanup-environment-pack-serve-restore/scripts/consumer-verify-version.sh
@@ -4,9 +4,12 @@ set -euo pipefail
 VERSION="${1:-${VERSION:-v4.30.0}}"
 LEANUP="${LEANUP:-leanup}"
 ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
+LEANUP_HOME="${LEANUP_HOME:-$HOME/.leanup}"
+LEANUP_CACHE_DIR="${LEANUP_CACHE_DIR:-$LEANUP_HOME/cache}"
 CHECK_ROOT="${CHECK_ROOT:-$HOME/leanup-check-$VERSION}"
 TMPDIR="${TMPDIR:-$HOME/.cache/leanup-runtime-tmp}"
 
+export LEANUP_HOME LEANUP_CACHE_DIR
 export PATH="$ELAN_HOME/bin:$PATH"
 export http_proxy=http://127.0.0.1:9
 export https_proxy=http://127.0.0.1:9
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh b/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
similarity index 92%
rename from docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
rename to skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
index 5351eb3..ed2c597 100755
--- a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
+++ b/skills/leanup-environment-pack-serve-restore/scripts/provider-pack-version.sh
@@ -5,7 +5,9 @@ VERSION="${1:-${VERSION:-v4.30.0}}"
 LEANUP="${LEANUP:-leanup}"
 ELAN_HOME="${ELAN_HOME:-$HOME/.elan}"
 PROJECT_ROOT="${PROJECT_ROOT:-$HOME/leanup-provider-projects}"
-SERVE_ROOT="${SERVE_ROOT:-$HOME/.leanup/cache/serve}"
+LEANUP_HOME="${LEANUP_HOME:-$HOME/.leanup}"
+LEANUP_CACHE_DIR="${LEANUP_CACHE_DIR:-$LEANUP_HOME/cache}"
+SERVE_ROOT="${SERVE_ROOT:-$LEANUP_CACHE_DIR/serve}"
 LOG="${LOG:-$HOME/.leanup/logs/provider-pack-${VERSION}.log}"
 PACK_WORK_ROOT="${PACK_WORK_ROOT:-${TMPDIR:-/tmp}}"
 PACK_WORK_DIR=""
@@ -17,6 +19,7 @@ cleanup_pack_work() {
 }
 trap cleanup_pack_work EXIT
 
+export LEANUP_HOME LEANUP_CACHE_DIR
 export PATH="$ELAN_HOME/bin:$PATH"
 export TMPDIR="${TMPDIR:-/tmp}"
 export TMP_DIR="${TMP_DIR:-$TMPDIR}"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh b/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
similarity index 89%
rename from docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
rename to skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
index d1b773b..68e59c6 100755
--- a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
+++ b/skills/leanup-environment-pack-serve-restore/scripts/provider-serve-assets.sh
@@ -3,7 +3,9 @@ set -euo pipefail
 
 HOST="${HOST:-0.0.0.0}"
 PORT="${PORT:-8765}"
-ROOT="${ROOT:-$HOME/.leanup/cache/serve}"
+LEANUP_HOME="${LEANUP_HOME:-$HOME/.leanup}"
+LEANUP_CACHE_DIR="${LEANUP_CACHE_DIR:-$LEANUP_HOME/cache}"
+ROOT="${ROOT:-$LEANUP_CACHE_DIR/serve}"
 LOG="${LOG:-$HOME/.leanup/logs/provider-serve.log}"
 PIDFILE="${PIDFILE:-$HOME/.leanup/state/locks/leanup-asset-server.pid}"
 PYTHON="${PYTHON:-python3}"
diff --git a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh b/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
similarity index 83%
rename from docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
rename to skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
index 38006bf..548cf49 100755
--- a/docs/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
+++ b/skills/leanup-environment-pack-serve-restore/scripts/provider-verify-assets.sh
@@ -3,7 +3,9 @@ set -euo pipefail
 
 VERSION="${1:-${VERSION:-v4.30.0}}"
 SERVER="${SERVER:-http://127.0.0.1:8765}"
-ROOT="${ROOT:-$HOME/.leanup/cache/serve}"
+LEANUP_HOME="${LEANUP_HOME:-$HOME/.leanup}"
+LEANUP_CACHE_DIR="${LEANUP_CACHE_DIR:-$LEANUP_HOME/cache}"
+ROOT="${ROOT:-$LEANUP_CACHE_DIR/serve}"
 
 paths=(
   "elan/base/elan-base.tar.gz"