Module 6 · Lesson 1

Lake Build System

Lake is Lean's build system and package manager. It handles dependencies, compilation, and project configuration.

Creating a New Project

bash

1# Create a new library project
2lake new myproject
3
4# Create an executable project
5lake new myapp exe
6
7# Initialize in existing directory
8lake init myproject

This creates a project structure:

text

1myproject/
2├── lakefile.lean    # Build configuration
3├── lean-toolchain   # Lean version
4├── Main.lean        # Entry point (for exe)
5└── Myproject/
6    └── Basic.lean   # Library code

The lakefile.lean

The lakefile configures your project:

lean

1import Lake
2open Lake DSL
3
4package myproject where
5  -- Package-level options
6  leanOptions := #[
7    ⟨`pp.unicode.fun, true⟩
8  ]
9
10-- Library target
11@[default_target]
12lean_lib Myproject where
13  -- Library options
14  roots := #[`Myproject]
15
16-- Executable target
17lean_exe myapp where
18  root := `Main

Key Takeaway

The lakefile is written in Lean itself. It defines packages (collections of code), libraries (reusable modules), and executables (runnable programs).

Basic Lake Commands

bash

1# Build the project
2lake build
3
4# Build and run an executable
5lake exe myapp
6
7# Clean build artifacts
8lake clean
9
10# Update dependencies
11lake update
12
13# Get help
14lake help

Adding Dependencies

Add external packages to your lakefile:

lean

1import Lake
2open Lake DSL
3
4package myproject where
5  -- Dependencies go here
6
7-- From GitHub
8require mathlib from git
9  "https://github.com/leanprover-community/mathlib4" @ "main"
10
11-- With specific version
12require std from git
13  "https://github.com/leanprover/std4" @ "v4.3.0"
14
15-- Local dependency
16require localLib from ".." / "local-lib"
17
18@[default_target]
19lean_lib Myproject

After adding dependencies:

bash

1# Fetch and build dependencies
2lake update
3lake build

ℹ

Dependencies are cached in the .lake directory. This folder is typically gitignored.

Project Targets

Libraries

lean

1-- A library with specific root modules
2lean_lib MyLib where
3  roots := #[`MyLib]
4  
5-- Multiple root modules
6lean_lib Utilities where
7  roots := #[`Utils.String, `Utils.Math, `Utils.IO]
8
9-- Exclude certain modules from build
10lean_lib Core where
11  roots := #[`Core]
12  globs := #[.submodules `Core]

Executables

lean

1-- Basic executable
2lean_exe myapp where
3  root := `Main
4
5-- Executable with dependencies
6lean_exe cli where
7  root := `CLI.Main
8  -- This exe depends on the MyLib library
9  -- (usually automatic)

The lean-toolchain File

This file specifies the Lean version:

text

1leanprover/lean4:v4.3.0

When you run lake, it ensures the correct Lean version is used. This guarantees reproducible builds.

Deep Dive: Lean Toolchain Management

The toolchain file works with elan, Lean's version manager:

bash

1# Install elan (if not already)
2curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
3
4# List installed toolchains
5elan show
6
7# Install a specific version
8elan install leanprover/lean4:v4.3.0
9
10# Set default toolchain
11elan default leanprover/lean4:stable

Configuration Options

lean

1package myproject where
2  -- Lean compiler options
3  leanOptions := #[
4    ⟨`pp.unicode.fun, true⟩,    -- Use λ instead of fun
5    ⟨`autoImplicit, false⟩      -- Disable auto-implicit
6  ]
7  
8  -- Stricter warnings
9  moreServerOptions := #[
10    ⟨`warningAsError, true⟩
11  ]
12
13lean_lib MyLib where
14  -- Library-specific options
15  defaultFacets := #[LeanLib.sharedLib]  -- Build shared library

Scripts and Custom Commands

lean

1-- Define a custom script
2script test do
3  IO.println "Running tests..."
4  -- Your test logic here
5  return 0
6
7script format do
8  IO.println "Formatting code..."
9  return 0

bash

1# Run custom scripts
2lake run test
3lake run format

Common Workflows

Starting a New Project

bash

1lake new myproject
2cd myproject
3lake build
4lake exe myproject  # If it's an executable

Adding Mathlib

lean

1-- In lakefile.lean
2require mathlib from git
3  "https://github.com/leanprover-community/mathlib4"
4
5-- Then run:
6-- lake update
7-- lake exe cache get  # Download pre-built .olean files

Building for Release

bash

1# Build with optimizations
2lake build -Krelease

💡

Use lake exe cache get when using Mathlib to download pre-compiled files instead of building from source—saves hours of compile time.

Mutable State Next: Modules & Imports