Lake: Lean 4 Build System and Package Manager Overview

Lake (Lean Make) is the official build system and package manager bundled with every Lean 4 installation. It reads a configuration file — called a lakefile — from the root of your project, resolves dependencies, compiles Lean source files in the correct order, and links the resulting artifacts into libraries or executables. If you have installed Lean 4 through elan, you already have Lake. Lake configuration files can be written in TOML (the default for new projects) or in the Lean DSL itself. Both formats support the same feature set; TOML is more approachable for beginners while the Lean DSL gives you the full power of metaprogramming for advanced use cases.

The lakefile is conventionally stored in the root directory of a package and is named lakefile.toml (TOML) or lakefile.lean (Lean DSL). Lake automatically discovers it when you run any lake command in or below that directory.

Key Concepts

Understanding Lake requires familiarity with a handful of well-defined terms. The table below gives a concise definition; the accordion sections that follow provide additional detail.

Term	One-line definition
Package	The fundamental unit of code distribution in Lake
Lakefile	The configuration file that describes a package
Workspace	A root package together with all of its transitive dependencies
Module	The smallest build unit — typically one Lean source file
Library	A named collection of modules with a shared configuration
Executable	A binary built from a single Lean module that has a `main` definition
Target	Any named, buildable unit — libraries, executables, and custom targets
Facet	One specific build product of a target (e.g. the `static` facet of a library)
Dependency	Another package that the current package requires
Manifest	`lake-manifest.json` — records the exact resolved revisions of all dependencies
Trace	A hash used to determine whether a target is up-to-date
Reservoir	The official Lean package registry at reservoir.lean-lang.org

Package

A package is the fundamental unit of code distribution in Lake. Packages can be sourced from the local file system or downloaded from the web (for example, via Git). A package is identified by the name field in its lakefile. Package names must be unique across all packages in a dependency graph.

Workspace

A workspace is the broadest organisational unit in Lake. It bundles together a root package, its transitive dependencies, and Lake’s environment. Every package can operate as the root of a workspace and the workspace derives its packagesDir configuration from this root. When you run lake build inside a package directory, that package becomes the workspace root.

Module

A module is the smallest unit of code visible to Lake’s build system. It is generally represented by a single Lean source file (.lean). Lake builds a set of binary artefacts for each module: a .olean (Lean data for importers), an .ilean (metadata for the LSP), and optionally a compiled C file and native object. Modules can import one another; Lake resolves the import graph automatically.

Library

A Lean library is a collection of modules that share a single build configuration. Its configuration defines a set of module roots (determining which modules belong to the library) and module globs (selecting which modules are built on lake build). Libraries produce static and shared binary facets in addition to their Lean artefacts.

Executable

A Lean binary executable is a binary that users can run without Lean installed. It is built from a Lean module called its root, which must contain a main definition. The root’s transitive local imports are built and linked automatically.

Target and Facet

A target is the fundamental build unit of Lake. Each target has a name used to identify it on the command line (e.g. lake build MyLib). Complex build products like packages and libraries have multiple facets — for example, a library has a leanArts facet (.olean/.ilean files), a static facet (.a), and a shared facet (.so/.dll/.dylib).Targets and facets are referenced with the syntax:

[@[<package>]/][<target>|[+]<module>][:<facet>]

Specifier	Meaning
`MyLib`	Default facet(s) of target `MyLib`
`@myPkg`	Default target(s) of package `myPkg`
`+MyModule`	Default facet(s) of module `MyModule`
`@myPkg/+MyModule:c`	The C file facet of `MyModule` in package `myPkg`

Dependency and Manifest

A dependency is another Lake package that the current package needs in order to build. Dependencies can come from a local path, a Git repository URL, or Reservoir. Once resolved, the exact Git revision (or local path) of each dependency is recorded in lake-manifest.json. This manifest ensures reproducible builds — every developer and CI run uses the same versions. Running lake update is the only command that modifies the manifest.

Trace

A trace is a hash derived from all the inputs to a build target — its source file, the Lean toolchain version, its imports, compiler flags, etc. Lake stores the trace alongside each built artefact. On subsequent builds, Lake recomputes the trace and compares it to the stored value; if they match the target is up-to-date and is not rebuilt.

The `.lake/` Directory

Lake stores all build outputs and downloaded packages inside a .lake/ directory at the root of the package:

.lake/
  build/          # compiled artefacts
    bin/          # binary executables
    lib/          # native libraries (.a, .so, .dll)
    lib/lean/     # Lean binary artifacts (.olean, .ilean)
    ir/           # intermediate results (.c, .o files)
  packages/       # downloaded dependencies

Add .lake/ to your .gitignore. Lake creates and manages this directory automatically; its contents should not be committed to source control (except for lake-manifest.json, which should always be committed).

Configuration File Formats

Lake accepts configuration files in two formats. Both are functionally equivalent.

TOML (lakefile.toml)
Lean DSL (lakefile.lean)

name = "hello"
version = "0.1.0"
defaultTargets = ["hello"]

[[lean_lib]]
name = "Hello"

[[lean_exe]]
name = "hello"
root = "Main"

TOML is the default format for lake new and lake init. It uses standard TOML array-of-tables syntax ([[lean_lib]], [[lean_exe]], [[require]]) for multi-valued entries.

import Lake
open Lake DSL

package "hello" where
  version := v!"0.1.0"

lean_lib Hello

@[default_target]
lean_exe hello where
  root := `Main

The Lean DSL imports Lake and opens the Lake.DSL namespace. It enables the full Lean language for computed configuration values and custom build targets.

You can convert between formats at any time with the lake translate-config command:

# Convert the current lakefile.lean to lakefile.toml
lake translate-config toml

# Convert the current lakefile.toml to lakefile.lean
lake translate-config lean

Translation is lossy — comments and formatting are not preserved.

Next Steps

Ready to create your first package? Head over to the Creating Packages guide to scaffold a new project with lake new or lake init.

Getting Started with Lake

Configuration

CLI Reference

Lake: Lean 4 Build System and Package Manager Overview

Key Concepts

The `.lake/` Directory

Configuration File Formats

Next Steps

Build docs developers (and LLMs) love

Getting Started with Lake

Configuration

CLI Reference

Documentation Index

​Key Concepts

​The .lake/ Directory

​Configuration File Formats

​Next Steps

Build docs developers (and LLMs) love

Key Concepts

The `.lake/` Directory

Configuration File Formats

Next Steps