Menu
Le prompt qui vérifie d'abord la source est sélectionné par défaut. Vous pouvez passer à une commande directe ou télécharger une copie locale.
Lisez SKILL.md et les fichiers associés affichés par SkillsMP avant de décider de l'installer.
Installer avec Codex ou Claude Copiez ce prompt, collez-le dans Codex, Claude ou un autre assistant, puis laissez-le vérifier la page du skill et l'installer pour vous.
Une commande directe contourne le prompt de vérification. Examinez la source avant de l'exécuter.
npx skills add https://github.com/leanprover/skills --skill lean4-setupLa commande reste sur une seule ligne. Faites défiler horizontalement pour la vérifier avant de la copier.
Vous préférez une copie locale ? Téléchargez les fichiers actuellement disponibles dans SkillsMP.
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
Basé sur la classification professionnelle SOC
Affichage de SKILL.md
| name | lean4-setup |
| description | Set up a lean4 repository clone with proper elan toolchains. |
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