What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

Question

I want to install Lean from scratch to see if I can fix a previous issue related to the location where I can create lean projects (and a related issue).

The official instructions don't seem to make it super clear how to re-install lean (or uninstall it). Given there are several (mysterious to me) tools for lean like elan, lake, lake-toolchains and perhaps others I am not aware -- I was hoping for an approved way to uninstall lean as if I were trying to install it from scratch.

I see I can run:

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

which requests my trust, which I'm fine to give but worried I might create a worse mess impossible to fix.

alternatively I can re-run the install commands blindly and hope it works:

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 install elan.

Note that Homebrew also contains a formula named simply lean, but that it installs a fixed version of Lean, rather than one provisioned with elan as per the above. Using this formula is as mentioned not recommended.

Use elan to install the latest stable version of lean by running elan toolchain install stable. You can also set the newly-installed version to be the default version of lean you get when running outside of a project (discussed below) by running elan default stable.

however all seem hacky with potential issues. Any better recommendations? The ideal algorithm I think would be:

1. uninstall all of lean properly (including all tools e.g. lake, elan, lake-toolchains etc) -- without uninstalling my vscode
2. then re-run the lean install code from scratch, e.g., /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile

suggestions on how to do this?

---

What does the official install script install_mac.sh do?

here is a detailed commented version of it, it actually seems quite safe/sensible to execute:

#!/usr/bin/env bash
# Shebang line to specify the script should be run with bash

set -exo pipefail
# Set bash options:
# -e: Exit immediately if a command exits with a non-zero status.
# -x: Print commands and their arguments as they are executed.
# -o pipefail: Causes a pipeline to return the exit status of the last command in the pipe that failed.

# Install Homebrew
if ! which brew > /dev/null; then
    # Checks if Homebrew is not installed by attempting to locate the `brew` command and redirects output to /dev/null
    # Install Homebrew
    /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install.sh)"
    # If Homebrew is not installed, it executes the Homebrew installation script downloaded from GitHub
else
    # Update it, in case it has been ages since it's been updated
    brew update
    # If Homebrew is already installed, update it to the latest version
fi

brew install elan-init
# Install elan, the Lean version manager, using Homebrew

elan toolchain install stable
# Install the latest stable version of the Lean toolchain using elan

elan default stable
# Set the installed stable version of Lean as the default version

# Install and configure VS Code
if ! which code > /dev/null; then
    # Checks if VS Code is not installed by attempting to locate the `code` command and redirects output to /dev/null
    brew install --cask visual-studio-code
    # If VS Code is not installed, install it using Homebrew Cask
fi

# Install the Lean4 VS Code extension
code --install-extension leanprover.lean4
# Installs the Lean4 extension for Visual Studio Code using the `code` command

---

related:

• How to install Lean-4 stable only?

Answer 1

I suspect (from your other question) that you're asking this because you believe you have things set up incorrectly, but hopefully my answer to your other question shows you that your set-up is fine and the misundersanding was elsewhere.

However there's no reason not to answer this question anyway, and I personally would say that the official way to uninstall Lean on mac/linux is just to remove the ~/.elan directory (and, if you like, remove $HOME/.elan/bin from $PATH), and the official way to remove all the versions of mathlib which you've collected along the way is to remove the ~/.cache/mathlib directory. Note also that any lean project you have which depends on mathlib is also taking up around 5 gigs of disc space.