Controlled installation of Lean 4 on MacOS #
This document explains a more controlled installation procedure for Lean on MacOS. There is a quicker way described in the main install page but it requires more trust.
If you get stuck, please come to the chat room to ask for assistance.
We'll need to set up Lean, an editor that knows about Lean, and mathlib
(the math library).
Rather than installing Lean directly, we'll install a small program called elan
which
automatically provides the correct version of Lean on a per-project basis. This is recommended for
all users.
Installing elan
and mathlib supporting tools #
-
Install Homebrew if you do not already have it installed.
-
Run
brew install elan-init
in a terminal window to installelan
.Note that Homebrew also contains a formula named simply
lean
, but that it installs a fixed version of Lean, rather than one provisioned withelan
as per the above. Using this formula is as mentioned not recommended. -
Use
elan
to install the latest stable version oflean
by runningelan toolchain install stable
. You can also set the newly-installed version to be the default version oflean
you get when running outside of a project (discussed below) by runningelan default stable
.
Installing and configuring an editor #
There are three editors you can use with Lean, VS Code emacs and neovim. This document describes using VS Code which currently has the best support for Lean. For emacs, look at https://github.com/leanprover/lean4-mode. For neovim, look at https://github.com/Julian/lean.nvim)
- Install VS Code.
- Launch VS Code.
- Click on the extension icon
(or
in older versions) in the side bar on the left edge of the screen (or press ⇧ Shift⌘ CommandX) and search for
leanprover
. - Select the
lean4
extension (unique nameleanprover.lean4
). - Click "install" (In old versions of VS Code, you might need to click "reload" afterwards)
- Verify Lean is working, for example by saving a file
test.lean
and entering#eval 1+1
. A green line should appear underneath#eval 1+1
, and hovering the mouse over it you should see2
displayed.
Lean Projects #
You can now read instructions about creating and working on Lean projects