Skip to content

Latest commit

 

History

History
59 lines (41 loc) · 2.32 KB

macos.md

File metadata and controls

59 lines (41 loc) · 2.32 KB

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

curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

(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) in the side bar on the left edge of the screen (or press ⇧ Shift⌘ CommandX) and search for leanprover.
  4. Click "install", and then "reload" to restart VS Code.
  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.

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