Controlled installation of Lean 4 on Debian/Ubuntu #
This document explains a more controlled installation procedure for Lean 4 and mathlib on Linux distributions derived from Debian (Debian itself, Ubuntu, LMDE,...). There is a quicker way described in the main install page but it requires more trust. Of course you can get even more details about what is going on by reading the bash script that will be downloaded below: elan_init.
Lean itself doesn't depend on much infrastructure, but supporting tools needed by most users require
curl. So the first step is:
sudo apt install git curl
The next step installs a small tool called
elanwhich will handle updating Lean according to the needs of your current project (hit Enter when a question is asked). It will live in
$HOME/.elanand adds a line to
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
There are three editors you can use with Lean, VS Code, emacs and neovim. The recommended choice is Visual Studio Code which has the most complete and well-tested support for Lean.
wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868 sudo apt install ./code.deb rm code.deb code --install-extension leanprover.lean4
Now open VS Code, and verify Lean is working, for example by saving a file
#eval 1+1. A green line should appear underneath
#eval 1+1, and hovering the mouse over it you should see
Lean Projects #
You can now read instructions about creating and working on Lean projects