How to install Lean and mathlib on MacOS #

This document explains how to get started with Lean and mathlib if you are using MacOS.

If you get stuck, please come to the chat room to ask for assistance.

There is a video walkthrough of these instructions on YouTube.

Installing Lean and mathlib #

Intel Macs #

Here we will discuss the fast way, assuming a lot of trust from you. It will install Lean, with supporting tools elan and leanpkg, the supporting tool leanproject for Lean's mathematical library, as well as the code editor VS Code and its Lean plugin. If you don't like this method, there is a detailed webpage which will decompose the process into described stages, and won't ask for a blind sudo.

The fast way is: open a terminal and type:

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

M1 Macs / Apple Silicon #

Given that GitHub Actions does not yet support builds on Apple ARM, installation of Lean is for the moment a bit more complex.

Specifically, elan – which is installed as part of the above instructions – will not be able to fetch Lean binaries on these devices if installed the normal way.

The following instructions are adapted from Fedor Pavutnitskiy, and allow you to install elan through Rosetta.

1. Open a new terminal window and install XCode Command Line Tools and Rosetta 2 using xcode-select --install and softwareupdate --install-rosetta.

2. We will install a second, separate x86 installation of Homebrew, which is easiest done by running a shell entirely using Rosetta 2. Do so by running arch -x86_64 zsh. The remainder of the commands below should be run from within this x86-running window, though once the steps have been completed, the installed tools will work in any future shell.

3. Install a second installation of Homebrew for x86 with /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)". It will automatically install itself into a second location (/usr/local, rather than /opt/).

4. Follow the same steps described in Controlled Installation for macOS using the brew you just installed:

/usr/local/bin/brew install elan-init mathlibtools
elan toolchain install stable 
elan default stable  

5. Install Visual Studio Code and the Lean extension via brew install --cask visual-studio-code && code --install-extension jroesch.lean (both the x86 and ARM versions of brew should work).

There is a Zulip thread with some interim further details and advice. If you have trouble, feel free to ask for help.

Lean Projects #

You can now read instructions about creating and working on Lean projects

If you encounter any command not found errors when opening a new terminal, logging out from MacOS and logging in again should fix it.