Stats
Actions
Tags
Help us improve
Share bugs, ideas, or general feedback.
From lean
Sets up Lean 4 repository clones with elan toolchains, including cmake/make builds, test execution, and linking for interactive use.
npx claudepluginhub leanprover/skills --plugin leanHow this skill is triggered — by the user, by Claude, or both
Slash command
/lean:lean-setupThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
The first time you build in a lean4 repository clone, you need to run
Bisects Lean 4 toolchain commits to identify regressions or behavior changes using self-contained test file signatures. Useful for Lean 4 debugging.
Assists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Interactive wizard configures repositories for Claude Code best practices by creating CLAUDE.md, slash commands, agents, hooks, and permissions. Activates on 'setup claude', 'init claude', or repo setup requests.
Share bugs, ideas, or general feedback.
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.
cd tests/lean/run
./test_single.sh example_test.lean
make -j -C build/release test ARGS="-j$(nproc)"
tests/lean/run/#guard_msgs to check for specific messagesIf 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
tests/ directory needs stage1 because tests run against the full Lean systemsrc/ directory needs stage0 because it's rebuilding the stdlib itself