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

The lake new command scaffolds a complete project. Which files you get depends on the template:

bash

1# std  (default) - a library AND an executable
2lake new myproject
3
4# exe  - executable only
5lake new myapp exe
6
7# lib  - library only
8lake new mylib lib
9
10# math - library preconfigured with Mathlib, linting, and CI
11lake new myproofs math
12
13# Same thing, but in the CURRENT directory instead of a new one
14lake init myproject
15
16# Pin the Lean version at creation time (via elan)
17lake +leanprover/lean4:v4.32.1 new myproject

💡

Append .lean or .tomlto a template name to choose the configuration file format — lake new myproject std.lean gives you a lakefile.lean. TOML is the default in current Lake, and is what you should prefer unless you need to compute something in the config.

This creates a project structure:

text

1myproject/
2├── lakefile.toml            # Build configuration
3├── lean-toolchain           # Pinned version, e.g. leanprover/lean4:v4.32.1
4├── Main.lean                # Entry point for the executable
5├── Myproject.lean           # Library root: usually just imports the modules below
6├── Myproject/
7│   └── Basic.lean           # Library code
8├── .github/workflows/       # CI that runs lake build
9└── .gitignore               # Ignores .lake/

ℹ

Note the pair Myproject.lean and Myproject/. That is Lean's module convention: the file is the module Myproject, and everything in the directory is Myproject.Something. The root file typically contains nothing but import lines, so a user can write import Myproject and get everything.

The lakefile

This is what lake new myproject actually generates:

toml|lakefile.toml

1name = "myproject"
2version = "0.1.0"
3defaultTargets = ["myproject"]
4
5[[lean_lib]]
6name = "Myproject"
7
8[[lean_exe]]
9name = "myproject"
10root = "Main"

The same configuration in the Lean DSL, which you get with the .lean template suffix:

lean|lakefile.lean

1import Lake
2open Lake DSL
3
4package myproject where
5  leanOptions := #[⟨`autoImplicit, false⟩]
6
7@[default_target]
8lean_lib Myproject
9
10lean_exe myproject where
11  root := `Main

Key Takeaway

A lakefile defines packages (the project as a whole), libraries (importable module trees), and executables (things with a main). Use the TOML form for ordinary projects; reach for the Lean DSL only when you need custom targets, scripts, or computed options.

Basic Lake Commands

These commands handle everyday development tasks. Run them from the project root directory.

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 the Reservoir registry, pinned to a tag or revision
8require "leanprover-community" / "mathlib" @ git "v4.32.0"
9
10-- Batteries (formerly std4 - the old name no longer resolves)
11require "leanprover-community" / "batteries" @ git "main"
12
13-- Local dependency
14require localLib from ".." / "local-lib"
15
16@[default_target]
17lean_lib Myproject

Or, equivalently, in lakefile.toml:

toml|lakefile.toml

1[[require]]
2name = "mathlib"
3scope = "leanprover-community"
4rev = "v4.32.0"

⚠

Pin dependencies to a tag or commit, not to main. Mathlib and Lean move in lockstep: a Mathlib revision only builds against the Lean version it was written for. If you see hundreds of errors in library code after a lake update, your lean-toolchainand your Mathlib revision have drifted apart.

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.

Understanding .lake

The .lake directory stores build artifacts, downloaded dependencies, and generated files. You can safely delete it to force a clean rebuild.

Project Targets

Libraries

A library target makes modules available for import by other code. Specify which modules belong to this library using the roots field.

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

An executable target produces a runnable program. The root field points to the module containing the main function.

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|lean-toolchain

1leanprover/lean4:v4.32.1

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.32.1
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-- Scripts live in lakefile.lean (the TOML format has no equivalent).
2-- A script returns a UInt32 exit code.
3script test do
4  IO.println "Running tests..."
5  -- Your test logic here
6  return 0
7
8script format do
9  IO.println "Formatting code..."
10  return 0

bash

1# List the scripts a project defines
2lake script list
3
4# Run one. "lake run" is an alias for "lake script run".
5lake run test
6lake script run format

Exercise: Add a Script

Create a script that prints the Lean version used by your project.

lean

1script showVersion do
2  IO.println s!"Lean toolchain: {(← IO.FS.readFile "lean-toolchain").trimAscii}"
3  return 0

Common Workflows

Starting a New Project

bash

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

Adding Mathlib

By far the easiest route is to let the template do it:

bash

1lake new myproofs math
2cd myproofs
3lake exe cache get     # Download prebuilt .olean files - do this FIRST
4lake build

To add Mathlib to an existing project, put the dependency in your lakefile and then:

bash

1# 1. Match lean-toolchain to the Mathlib revision you are requiring
2# 2. Fetch the dependency
3lake update mathlib
4# 3. Download prebuilt artifacts instead of compiling Mathlib yourself
5lake exe cache get
6# 4. Build
7lake build

💡

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