Lean REPL Setup

Setup and verification guide for the Lean environment used by wonton-soup.

Toolchain Contract

• Lean version pinned in lean_project/lean-toolchain (currently 4.25.0)
• Local leantree checkout at libs/leantree
• LEAN_PROJECT_PATH must point to this dossier’s lean_project/

Requirements

• Python 3.12+
• uv
• elan

Step 1: Install Pinned Lean

Install elan if needed:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Install + select pinned toolchain:

elan install leanprover/lean4:v4.25.0
elan default leanprover/lean4:v4.25.0
lean --version

Expected: Lean (version 4.25.x, ...).

Step 2: Ensure LeanTree Checkout

From repo root:

git submodule update --init --recursive dossiers/wonton-soup/libs/leantree

Step 3: Create Lean Project

From dossiers/wonton-soup/:

uv run python setup_lean.py

This initializes lean_project/ and fetches Lean dependencies.

Step 4: Export LEAN_PROJECT_PATH

export LEAN_PROJECT_PATH=/path/to/specter-labs/dossiers/wonton-soup/lean_project

Step 5: Smoke Test

From dossiers/wonton-soup/:

uv run python wonton.py lean run -m dev --sample 3 --seed 123 --plain

Expected signals:

• a new logs/corpus-YYYY-MM-DD-HHMMSS/ directory
• run_status.json with status: completed
• summary.json.gz present

Platform Notes

• macOS uses gzcat; most Linux distributions use zcat.
• if elan binaries are not discovered, prepend $HOME/.elan/bin to PATH.

Troubleshooting

lake not found

export PATH="$HOME/.elan/bin:$PATH"

Then verify:

lake --version

Lean version mismatch

elan override set leanprover/lean4:v4.25.0
lean --version

REPL build failures in lean_project/

cd lean_project
lake build

If dependency fetch/build still fails, remove transient build outputs and rebuild with the pinned version active.

LEAN_PROJECT_PATH not respected

Verify current shell value:

echo "$LEAN_PROJECT_PATH"

It must resolve to this dossier’s lean_project path, not another repository.