<commit_before># How to install Lean using elan

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

If you get stuck, please come to [the chat room](https://leanprover.zulipchat.com/) to ask for
assistance.

## Preliminaries

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.
  * Ubuntu: `sudo apt install git curl` if you don't already have these.
  * macOS: Install [homebrew](https://brew.sh/), then run `brew install libgmp coreutils` in a terminal
    (`libgmp` is required by `lean`, `coreutils` by `leanpkg`).
  * Windows 10: 
    * Either (recommended): install [Git for Windows](https://gitforwindows.org/), after which you
      can open a terminal by typing "git bash" in the Windows search bar.
    * Or: install [Msys2](https://www.msys2.org/), after which you can open a terminal by
      typing "msys2" in the Windows search bar. You'll also need to run `pacman -S unzip git` in 
      an msys2 terminal.

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.

   On Linux and on macOS, this automatically appends a line to your `$HOME/.profile`
   which prepends `$HOME/.elan/bin` to your `$PATH`.

   On Windows, this doesn't happen automatically, so you'll need to run
   `echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile` in the terminal.

   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.)<commit_msg>fix(docs/elan): fix homebrew instructions for macOS (#395)<commit_after># How to install Lean using elan

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

If you get stuck, please come to [the chat room](https://leanprover.zulipchat.com/) to ask for
assistance.

## Preliminaries

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.
  * Ubuntu: `sudo apt install git curl` if you don't already have these.
  * macOS: Install [homebrew](https://brew.sh/), then run `brew install gmp coreutils` in a terminal
    (`gmp` is required by `lean`, `coreutils` by `leanpkg`).
  * Windows 10: 
    * Either (recommended): install [Git for Windows](https://gitforwindows.org/), after which you
      can open a terminal by typing "git bash" in the Windows search bar.
    * Or: install [Msys2](https://www.msys2.org/), after which you can open a terminal by
      typing "msys2" in the Windows search bar. You'll also need to run `pacman -S unzip git` in 
      an msys2 terminal.

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.

   On Linux and on macOS, this automatically appends a line to your `$HOME/.profile`
   which prepends `$HOME/.elan/bin` to your `$PATH`.

   On Windows, this doesn't happen automatically, so you'll need to run
   `echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile` in the terminal.

   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.)
{'fraction_non_alphanumeric': 0.09606873210101537, 'fraction_numerical': 0.004946628482166103, 'mean_word_length': 3.640096618357488, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, 'https://': 10, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2426471', 'n_tokens_mistral': 1198, 'n_tokens_neox': 1131, 'n_words': 517}