Lean Installation

Lean is a powerful theorem prover and programming language. This guide provides various methods to install Lean on a system.

1. Using Docker
2. Using elan (Lean Version Manager)
3. Via Package Managers
4. Building from Source
Development Environment
- VSCode Integration
- Testing
Documentation

1. Using Docker

Docker is the modern way to run applications in isolated environments. Using Docker for Lean ensures a consistent setup across different systems without worrying about “it works on my machine” issues.

Install Docker:
- On Linux:
```
curl -fsSL https://get.docker.com -o get-docker.sh && sh get-docker.sh
```
- On macOS and Windows: Download and install Docker Desktop from the official Docker website
Pull the latest Lean image:
```
docker pull leanprover/lean:latest
```

Run the Docker container:

docker run -it -v /path/to/local/directory:/lean leanprover/lean:latest

Inside the container, Lean can now be used:
```
lean --version
```

2. Using elan (Lean Version Manager)

elan is the recommended tool for installing and managing Lean versions.

Install elan:

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

Install the latest stable version of Lean:
```
elan default stable
```
Verify the installation:
```
lean --version
```

elan can also be used to manage multiple versions of Lean:

elan install <version>  # Install a specific version of Lean
elan default <version>  # Set the default version of Lean
elan list               # List installed Lean versions

3. Via Package Managers

Homebrew (macOS and Linux)

brew install lean

yay (Arch, Manjaro)

yay -S lean4-bin

Nix (NixOS and other systems)

nix-env -i lean

4. Building from Source

For the latest development version or specific customizations:

Ensure CMake and GCC are installed.

Clone the Lean repository:

git clone https://github.com/leanprover/lean4.git
cd lean4

Build and install:
```
mkdir build && cd build
cmake ..
make
```

Development Environment

VSCode Integration

VSCode is the primary IDE for Lean development. The Lean extension provides a complete set of features required for end to end development in Lean. Other editor integrations are available such as lean-mode for Emacs and lean.vim for Vim. However, the VSCode extension is the most feature-rich and actively maintained.

Testing

Lean supports unit testing through its test command:

def double (x : Nat) : Nat := x * 2

#test double 2 = 4        -- Basic test
#test double 0 = 0        -- Edge case

Tests can be run using the lean --test command:

lean --test my_file.lean

Documentation

Lean supports documentation strings using /-! ... -/ for modules and /-- ... -/ for definitions:

/-!
# Basic Arithmetic Module
This module provides basic arithmetic operations.
-/

/--
`add` performs addition on natural numbers.
-/
#eval add 2 3  -- returns 5

Lean also supports markdown-style comments for documentation:

/- Markdown-style comment
# Heading
This is a paragraph.
-/

Documentation strings can be accessed using the #print command:

#print add

doc-gen4 is a tool that generates documentation for Lean projects and comes bundled with the Lean installation. Its setup includes creating a nested project for documentation building inside the lake project.

Create a directory called docbuild inside the project.
Create a lakefile.toml file inside the docbuild directory:

name = "docbuild"
reservoir = false
version = "0.1.0"
packagesDir = "../.lake/packages"

[[require]]
name = "MyProject"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
rev = "main"

Run lake update doc-gen4 within docbuild to pin doc-gen4 and its dependencies to the chosen versions.
If the parent project has dependencies, they can be updated for building the documentation by running lake update MyProject in the docbuild directory.

Projects & Structure