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 structure. Useexe for programs you want to run, or omit it for libraries.

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

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

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

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

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").trim}"

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