Installation and troubleshooting

Requirements

macOS arm64, or glibc-based Linux x86_64 with AVX2. Linux releases are built on Ubuntu 22.04.
curl and either shasum or sha256sum.
The codex CLI for the default backend; see other providers.
About 10 GiB of additional disk space for Lean/Mathlib. Linux Lean support also requires bwrap (the bubblewrap package) and socat.
Python 3.12+ only if you use the bundled Python analysis tools.

Choose an install mode

From the release checkout or an extracted release bundle:

bash setup.sh               # CLI and WebUI only (default)
bash setup.sh --with-lean     # CLI, WebUI, Lean and Mathlib
bash setup.sh --without-lean  # CLI and WebUI only
bash setup.sh --install-lean  # add or repair Lean support later

bash setup.sh defaults to CLI and WebUI only, without a selection prompt, in both interactive terminals and scripts. Lean/Mathlib installation requires --with-lean or --install-lean. Existing Lean installations are kept.

After a core-only install, the first approved local Lean goal, check, verify, or library operation can install the deferred toolchain. Progress and failures are shown during installation. This applies only to the bundled lean-workspace; remote LeanSearch and caller-owned Lean projects do not trigger installation.

Setup creates .env if needed and installs a managed mathcode launcher in ~/.local/bin/. Existing configuration is preserved. The bundle includes CLI, WebUI, and ripgrep; a source checkout or node_modules is not required.

Upgrade and repair

git pull --ff-only           # for a cloned release checkout
bash setup.sh --without-lean # or --with-lean, according to your needs
bash setup.sh --status

Setup checks runtime versions and hashes, repairing missing, stale or invalid files from the matching GitHub Release. It verifies the downloaded checksum before replacing an existing installation. --status reports CLI, WebUI, ripgrep and Lean readiness. Restart a running WebUI daemon after upgrading.

bash setup.sh --clean removes installed runtime/toolchain artifacts while preserving proofs in LeanFormalizations/, vault data, and the locked Lake manifest. Rerun setup afterwards. See bash setup.sh --help for all flags.

Use a downloaded archive

Download your platform's .tar.gz and SHA256SUMS.txt from Releases. Check the archive against its matching checksum entry, extract it, then run setup from that folder. The archive is self-contained; setup downloads runtime files only when repair is needed. Keep using the matching platform when updating manually.

Lean toolchain selection

When Lean installation is requested, the default is a bundle-local toolchain in .local/elan, pinned by lean-workspace/lean-toolchain. Setup retains the bundled lake-manifest.json and requires a successful MathCodeLean readiness build; failed Mathlib cache fetches can fall back to building locally.

To reuse a system installation, run:

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

Both Lean and Lake must match the pinned version. Setup resolves Elan proxies to concrete binaries and saves validated paths in .env; an invalid pair falls back to bundle-local Lean. Ambient ELAN_TOOLCHAIN overrides are ignored when selecting the pinned toolchain. Custom projects retain their own toolchain setup.

Troubleshooting

Symptom	Action
`mathcode` is not found after setup	Open a new shell, or use `./run` immediately.
`exec format error` or `Bad CPU type in executable`	Rerun setup or download the archive for your OS and CPU.
Codex authentication is missing	Run `codex auth login`.
Lean is reported as deferred	Run `bash setup.sh --install-lean` when you need local Lean support.
An upgrade still uses old WebUI defaults	Restart the daemon and check Follow application defaults in Settings.

Setup replaces only launchers it previously created. Use MATHCODE_INSTALL_BIN_DIR to select another launcher directory; relative paths are resolved from the bundle root. If setup cannot write the launcher, the bundle remains usable through ./run.