Skip to content

macos.md

Latest commit

 

History

History
66 lines (45 loc) · 2.51 KB

macos.md

File metadata and controls

66 lines (45 loc) · 2.51 KB
Raw

How to install Lean and mathlib on MacOS

This document explains how to get started with Lean and mathlib.

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

If you prefer, you can watch a short video tutorial

We'll need to set up Lean, an editor that knows about Lean, and mathlib (the standard 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

  1. We'll need a terminal, along with some basic prerequisites. Install homebrew, then run brew install gmp coreutils in a terminal (gmp is required by lean, coreutils by leanpkg).

  2. At a terminal, run the command

    curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

    and hit enter when a question is asked.

    It is recommended that you re-login, so that your environment knows about elan. (Alternatively, type source $HOME/.elan/env to update the current terminal.)

Installing mathlib supporting tools

At a terminal, run the command

brew install python3
sudo pip3 install mathlibtools

This will install tools that, amongst other things, let you download compiled binaries for mathlib.

Installing and configuring an editor

There are two editors you can use with Lean, VS Code and emacs. This document describes using VS Code (for emacs, look at https://github.com/leanprover/lean-mode).

  1. Install VS Code.
  2. Launch VS Code.
  3. Click on the extension icon (image of icon) (or (image of icon) in older versions) in the side bar on the left edge of the screen (or press ⇧ Shift⌘ CommandX) and search for leanprover.
  4. Click "install" (In old versions of VSCode, you might need to click "reload" afterwards)
  5. 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 see 2 displayed.

Note however that you cannot use mathlib, and in particular any imports, in the file test.lean created above.

You're not done yet!

👉 If you want to use mathlib, you should now read the instructions about creating and working on Lean projects.