Lake: The Build System and Package Manager for Lean 4

Just as C++ relies on CMake for build orchestration and package managers like Conan or vcpkg for dependency resolution, Lean 4 relies on Lake (Lean Make). Lake serves as a unified build system, dependency manager, and task runner designed specifically to handle module trees, compiled C backends, and precompiled proof artifacts.

1. Architecture: How Lake Compares to Traditional Tools

In C and C++, CMake generates platform-specific build files (Ninja/Makefiles) to compile source .cpp files into object files (.o) and binaries.

Lake handles a similar multi-stage process tailored to interactive theorem proving:

2. Project Scaffolding & Module Topology

When creating a new Lean 4 project, Lake enforces a strict file-to-module mapping:

# Create a default project (Library + Executable)
lake new Beejganita

This command generates the canonical directory tree:

Beejganita/
├── .devcontainer/           # Container specifications (optional)
├── .github/workflows/       # Continuous Integration workflows
├── .gitignore               # Excludes .lake/ build directory
├── Beejganita/
│   └── Basic.lean           # Submodule: maps to `Beejganita.Basic`
├── Beejganita.lean          # Library Root Module: maps to `Beejganita`
├── Main.lean                # Executable entry point (`def main : IO Unit`)
├── lakefile.toml            # Package manifest (or lakefile.lean)
├── lake-manifest.json       # Generated lockfile for pinned revisions
└── lean-toolchain           # Specifies exact Lean 4 version (e.g., leanprover/lean4:v4.15.0)

The Module Naming Convention

Lean 4 treats folder paths as dot-separated module namespaces:

• Beejganita.lean is the root module (import Beejganita).
• Beejganita/SamuhaSiddhanta/Porvapekshika.lean maps to import Beejganita.SamuhaSiddhanta.Porvapekshika.

3. Configuration Formats: TOML vs. Lean DSL

Lake supports two configuration formats: static TOML for standard projects, and a programmatic Lean DSL for advanced configuration.

Option A: Static Configuration (lakefile.toml)

Preferred for straightforward projects without dynamic build steps.

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

[[lean_lib]]
name = "Beejganita"

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

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "main"

Option B: Programmatic DSL (lakefile.lean)

Use the .lean format when custom scripts, conditional dependencies, or target facets are required.

import Lake
open Lake DSL

package «Beejganita» where
  leanOptions := #[
    ⟨`autoImplicit, false⟩,
    ⟨`pp.unicode.fun, true⟩
  ]

-- Require external libraries from Git or Reservoir
require "leanprover-community" / "mathlib"

@[default_target]
lean_lib «Beejganita» where
  roots := #[`Beejganita]

lean_exe «beejganita» where
  root := `Main

4. Managing Dependencies & Binary Caching

Mathematical formalization relies heavily on Mathlib, a massive library containing hundreds of thousands of theorems. Compiling Mathlib from source takes hours. Lake solves this bottleneck through toolchain alignment and binary caches.

The Dependency Lifecycle

1. Declare the Dependency: Add Mathlib to lakefile.lean:

require "leanprover-community" / "mathlib"

1. Align Toolchains: Because Lean 4 releases update compiler internals frequently, your project’s lean-toolchain must match Mathlib’s pinned compiler revision:

lake update
cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain

1. Fetch Precompiled .olean Artifacts: Instead of compiling millions of lines of proof code locally, download precompiled binary proof states directly:

lake exe cache get

1. Compile Your Local Modules:

lake build

5. Automation Scripts (Task Running)

Similar to npm scripts or Makefile targets, Lake allows you to write build scripts directly in Lean. Scripts must reside inside a lakefile.lean.

-- Defined in lakefile.lean
script checkVersion do
  let version ← IO.FS.readFile "lean-toolchain"
  IO.println s!"Active Project Toolchain: {version.trimAscii}"
  return 0

Execute scripts using lake run:

lake run checkVersion

6. Lake CLI Quick Reference

# Scaffolding
lake new <project-name> [math|lib|exe|std] # Create a project using a template
lake init                                  # Initialize a project in current directory

# Building & Running
lake build                                 # Compile default targets
lake build Beejganita:docs                 # Build documentation via doc-gen4
lake exe <exe-name>                        # Build and run the specified executable

# Maintenance
lake update                                # Resolve and update dependencies in lake-manifest.json
lake clean                                 # Delete output artifacts in .lake/build/
lake exe cache get                         # Fetch precompiled Mathlib binary cache

7. Foreign Function Interface (FFI) & C Integration

Just as CMake compiles C/C++ source code into native object files and links them into libraries, Lake natively supports compiling C code and embedding it into Lean packages via target facets.

Compiling C Code with Lake

When a Lean module relies on external C functions (@[extern "c_function_name"]), Lake can compile the C files using the host C compiler (clang or gcc) and link the resulting static or shared libraries automatically.

Add C targets to lakefile.lean:

import Lake
open Lake DSL

package «Beejganita» where
  -- Pass flags directly to the host C compiler
  morecflags := #["-O3", "-Wall"]

-- 1. Declare the target C object file
target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcFile := pkg.dir / "c" / "ffi.c"
  let compiler := "cc"
  let args := #["-c", srcFile.toString, "-o", oFile.toString, "-I", (← getLeanIncludeDir).toString]
  buildFileAfterDep oFile srcFile fun _ => do
    proc { cmd := compiler, args := args }

-- 2. Declare a static library containing the object file
target libffi.a pkg : FilePath := do
  let libFile := pkg.buildDir / "c" / "libffi.a"
  let oFile ← pkg.ffi.o.fetch
  buildStaticLib libFile #[oFile]

-- 3. Attach the compiled static library to the Lean library target
@[default_target]
lean_lib «Beejganita» where
  nativeFacets := fun _ => #[`static]
  moreLinkArgs := #["-L", "./.lake/build/c", "-lffi"]

8. Multi-Package Workspaces & Monorepos

For large-scale projects or monorepos containing multiple independent modules, Lake supports workspaces where a root package manages local dependencies without publishing them to an external registry.

Configuring Local Workspace Dependencies

Structure your monorepo with multiple package directories:

my-monorepo/
├── lakefile.lean            # Master workspace configuration
├── subpackages/
│   ├── CoreLib/             # Base mathematical definitions
│   │   └── lakefile.lean
│   └── AdvancedProofs/      # Depends on CoreLib
│       └── lakefile.lean

In subpackages/AdvancedProofs/lakefile.lean, require the local package using a relative file path:

import Lake
open Lake DSL

package «AdvancedProofs»

-- Require local package dependency relative to this file
require CoreLib from ".." / "CoreLib"

@[default_target]
lean_lib «AdvancedProofs»

9. Documentation Generation (doc-gen4)

Lake integrates directly with doc-gen4 to generate static HTML API documentation for Lean projects, preserving docstrings, theorem statements, and tactic proofs.

Building Project Docs Locally

1. Add the conditional doc-gen4 dependency to lakefile.lean:

meta if get_config? doc = some "on" then
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

1. Compile the HTML output for your specific package:

lake -R -Kdoc=on build Beejganita:docs

The generated HTML site will be exported to .lake/build/doc/, which can be served locally or deployed to static hosting platforms.

10. Continuous Integration Pipeline (GitHub Actions)

A production-ready GitHub Actions workflow handles binary cache retrieval, compilation, and proof verification on every commit.

Create .github/workflows/build.yml:

name: Lean 4 Lake Build

on:
  push:
    branches: [ main ]
  pull_request:
    branches: [ main ]

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout Repository
        uses: actions/checkout@v4

      - name: Install Elan (Lean Version Manager)
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Verify Toolchain Alignment
        run: lean --version

      - name: Fetch Mathlib Precompiled Cache
        run: lake exe cache get

      - name: Build Project & Verify Proofs
        run: lake build

11. Troubleshooting Common Lake Errors

12. Advanced Build Facets & Custom Target Rules

[!WARNING] Below provided code block are’tested they are generated from the GeminiAI Search

Lake’s build engine operates as a directed acyclic graph (DAG) of facets. A facet represents a specific build output derived from a module, library, or package (such as .olean files, C intermediate code, shared objects, or documentation trees).

Custom Build Facets

You can define custom facets in lakefile.lean to process build outputs, run custom preprocessors, or generate static code artifacts:

import Lake
open Lake DSL

-- Define a custom module facet that counts total lines of code
module_facet loc mod : Nat := do
  let file := mod.filePath
  let content ← IO.FS.readFile file
  return content.lines.size

-- Define a package-level target to aggregate metrics
target locReport pkg : Nat := do
  let mods ← pkg.getModuleArray
  let counts ← mods.mapM (·.loc.fetch)
  return counts.foldl (· + ·) 0

Run custom targets directly through Lake:

lake build locReport

13. CMake vs. Lake Command Reference

14. Production Best Practices for Lean 4 Repositories

• Lock lean-toolchain File: Always commit lean-toolchain and lake-manifest.json to version control. Never upgrade Lean versions independently of your Mathlib dependency revision.
• Always Download Precompiled Mathlib Caches: Run lake exe cache get inside Docker setup scripts, CI pipelines, and local environments before invoking lake build.
• Use TOML for Standard Configs: Prefer lakefile.toml unless your build requires custom scripts (script), FFI C compilation (target), or dynamic facet evaluation.
• Keep Module Names Uniform: Ensure folder paths precisely match module namespaces (e.g., Beejganita/GroupTheory/Basic.lean $\rightarrow$ import Beejganita.GroupTheory.Basic).

By combining dependency management, precompiled binary distribution, custom scripting, and C FFI compilation into a single unified tool, Lake eliminates the fragmented multi-tool workflows common in traditional compiled languages. It allows formal verification engineers to focus entirely on proof construction while ensuring reproducible, deterministic builds across Docker containers, local developer workstations, and continuous integration pipelines.