lean4-setup

Lean 4 Repository Setup

The first time you build in a lean4 repository clone, you need to run

cmake --preset release
make -j -C build/release

The cmake command is not needed on subsequent builds.

Tests

Running a Single Test

cd tests/lean/run
./test_single.sh example_test.lean

Running the Full Test Suite

make -j -C build/release test ARGS="-j$(nproc)"

Writing Tests

• All new tests should go in tests/lean/run/
• These tests don't have expected output files — they run on a success/failure basis
• Use #guard_msgs to check for specific messages

Lean 4 repositories for interactive use

If you are cloning or repairing the leanprover/lean4 repository for a user to work in, you need to do further set up. First, do an initial build according to the instructions above. Then you'll need to pick a toolchain name. If this is the only clone of lean4 on the machine, just use lean4. Otherwise you might use something like lean4-XYZ.

Then run the following commands:

elan toolchain link lean4-XYZ build/release/stage1
elan toolchain link lean4-XYZ-stage0 build/release/stage0
echo lean4-XYZ > lean-toolchain
echo lean4-XYZ > script/lean-toolchain
echo lean4-XYZ > tests/lean-toolchain
echo lean4-XYZ-stage0 > src/lean-toolchain

After setting up the toolchains, verify it worked:

cd tests/lean/run
lean --version  # Should show the commit hash from your clone, not a release version

When done with the clone, remove the toolchains:

elan toolchain uninstall lean4-XYZ
elan toolchain uninstall lean4-XYZ-stage0

• The tests/ directory needs stage1 because tests run against the full Lean system
• The src/ directory needs stage0 because it's rebuilding the stdlib itself