安装与排障

环境要求

macOS arm64，或采用 glibc、支持 AVX2 的 Linux x86_64。Linux 发行包基于 Ubuntu 22.04 构建。
curl，以及 shasum 或 sha256sum。
默认后端需要 codex CLI；也可以配置其他后端。
Lean/Mathlib 需要额外约 10 GiB 磁盘空间。Linux 的 Lean 支持还需要 bwrap（bubblewrap 包）与 socat。
仅使用内置 Python 分析工具时才需要 Python 3.12+。

选择安装方式

在发行版 checkout 或解压后的安装目录执行：

bash setup.sh               # 默认仅安装 CLI 与 WebUI
bash setup.sh --with-lean     # CLI、WebUI、Lean 和 Mathlib
bash setup.sh --without-lean  # 仅 CLI 与 WebUI
bash setup.sh --install-lean  # 之后补装或修复 Lean

bash setup.sh 默认只安装 CLI 和 WebUI，不显示安装方式选择提示；交互终端与脚本调用行为一致。安装 Lean/Mathlib 需要显式传入 --with-lean 或 --install-lean，已有 Lean 安装会保留。

轻量安装后，第一次获准执行本地 Lean goal、check、verify 或库操作时，可以自动补装工具链，并显示安装进度和失败原因。自动补装只作用于发行包自带的 lean-workspace；远程 LeanSearch 和用户自己的 Lean 项目不会触发安装。

Setup 按需创建 .env，并在 ~/.local/bin/ 安装受管理的 mathcode 启动脚本。已有配置会保留。安装包自带 CLI、WebUI 与 ripgrep，不需要源码 checkout 或 node_modules。

升级与修复

git pull --ff-only           # 适用于 clone 的发行仓库
bash setup.sh --without-lean # 也可按需选择 --with-lean
bash setup.sh --status

Setup 检查运行时版本和哈希，从对应 GitHub Release 修复缺失、过旧或无效的文件，并在替换已有安装前验证下载内容的校验和。--status 显示 CLI、WebUI、ripgrep 和 Lean 的状态。升级后请重启正在运行的 WebUI daemon。

bash setup.sh --clean 清理已安装的运行时和工具链，保留 LeanFormalizations/ 中的证明、vault 数据和锁定的 Lake manifest；之后重新执行 setup。全部选项见 bash setup.sh --help。

直接下载 archive

从 Releases 下载对应平台的 .tar.gz 和 SHA256SUMS.txt。用匹配条目验证 archive 后解压，在该目录运行 setup。Archive 是自包含的，只有需要修复时 setup 才会下载运行时文件。手动更新时也要选择正确平台。

Lean 工具链选择

选择安装 Lean 时，默认使用 .local/elan 中的本地工具链，版本由 lean-workspace/lean-toolchain 锁定。Setup 保留随包提供的 lake-manifest.json，并要求 MathCodeLean readiness 构建成功；Mathlib cache 下载失败时可以回退到本地构建。

若要复用系统安装：

MATHCODE_SETUP_USE_SYSTEM_LEAN=1 bash setup.sh --with-lean

Lean 和 Lake 都必须符合锁定版本。Setup 将 Elan proxy 解析为具体可执行文件，校验后把路径保存到 .env；不符合要求时回退到包内工具链。选择锁定工具链时会忽略外部 ELAN_TOOLCHAIN 覆盖。用户自己的项目仍使用自己的工具链配置。

常见问题

现象	处理方法
Setup 后找不到 `mathcode`	打开新 shell，或直接使用 `./run`。
`exec format error` 或 `Bad CPU type in executable`	重新执行 setup，或下载匹配系统和 CPU 的 archive。
缺少 Codex 认证	执行 `codex auth login`。
Lean 状态为 deferred	需要本地 Lean 时执行 `bash setup.sh --install-lean`。
升级后 WebUI 仍使用旧默认值	重启 daemon，并检查设置页的 Follow application defaults。

Setup 只替换自己创建的启动脚本。可用 MATHCODE_INSTALL_BIN_DIR 指定其他目录，相对路径以安装包根目录为基准。写入启动脚本失败时仍可通过 ./run 使用安装包。