Installation de Lean

Sous Windows

  1. Installer Git for Windows L'installateur pose beaucoup de questions mais les réponses par défaut conviennent.

  2. Lancer Git bash
    1. taper la ligne curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
    2. sélectionner (1) « proceed with installation »
    3. lorsque l'écran montre « Elan is installed now. Great! » appuyer sur la touche entrée
    4. Redémarrez la session.
  3. Installer Visual Studio Code. Les réponses par défaut conviennent pour toutes les questions posées par l'installateur.

  4. Lancer VScode, cliquer sur l'icône « extensions » dans la barre d'icônes à gauche, chercher leanprover. Cliquer sur Install puis sur Reload quand l'installation est terminée.

  5. Télécharger m114.zip et le décompresser

  6. Dans VScode, menu fichier, cliquer sur « Open folder » (ou « Ouvrir dossier » s'il est en français) et sélectionner le répertoire créé par la décompression de m114.zip (c'est le répertoire qui contient leanpkg.toml pas un répertoire qui contient directement des fichiers .lean). Ensuite ouvrir un fichier Lean comme d'habitude

Sous Linux

  1. Dans un terminal :
    1. Installer git et curl. Par exemple, avec une distribution Debian ou dérivée (Ubuntu...) taper dans un terminal sudo apt install git curl.
    2. taper la ligne curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
    3. sélectionner (1) « proceed with installation »
    4. lorsque l'écran montre « Elan is installed now. Great! » appuyer sur la touche entrée
    5. Taper source ~/.elan/env
  2. Installer Visual Studio Code. Les réponses par défaut conviennent pour toutes les questions posées par l'installateur.

  3. Lancer VScode, cliquer sur l'icône « extensions » dans la barre d'icônes à gauche, chercher leanprover. Cliquer sur Install puis sur Reload quand l'installation est terminée.

  4. Télécharger m114.zip et le décompresser

  5. Dans VScode, menu fichier, cliquer sur « Open folder » (ou « Ouvrir dossier » s'il est en français) et sélectionner le répertoire créé par la décompression de m114.zip (c'est le répertoire qui contient leanpkg.toml pas un répertoire qui contient directement des fichiers .lean). Ensuite ouvrir un fichier Lean comme d'habitude

mis à jour le 29 avril 2020.