Lean setup

Skill leanprover/skills/skills/lean-setup

Set up a lean4 repository clone with proper elan toolchains.From its SKILL.md

Install

npx -y skills add leanprover/skills --skill lean-setup

Assembled from the repository path, not quoted from the project. Check it against their README if it does not work.

SKILL.md

1.8 KB, as published. Nobody here has run it

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