1.2 Project Structure with Lean and Lake

Lean development is organized around projects. A project defines a closed environment: it fixes the Lean version, declares dependencies, and specifies how code is compiled. The structure is simple, but small details determine whether imports resolve, builds succeed, and tooling behaves predictably.

Problem

You want a project layout that supports reproducible builds, clear module boundaries, and predictable imports.

Solution

Create and work inside a Lake project. The default layout produced by:

lake new myproj

has the following structure:

myproj/
├── lakefile.lean
├── lean-toolchain
├── Myproj/
│   └── Basic.lean
├── Main.lean
└── lake-manifest.json

Each file has a precise role.

File Roles

The directory Myproj/ corresponds to a namespace. The file:

-- Myproj/Basic.lean
namespace Myproj

def hello : String :=
  "hello"

end Myproj

is imported using:

import Myproj.Basic

The mapping between file paths and module names is strict. A mismatch between directory names and namespaces leads to unresolved imports.

Lake Configuration

The file lakefile.lean defines the build graph. A minimal configuration looks like:

import Lake
open Lake DSL

package «myproj» where

lean_lib Myproj

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

This declares:

• a package named myproj
• a library Myproj
• an executable whose root module is Main

The executable is built and run with:

lake build
lake exe myproj

Module System

Lean uses a hierarchical module system. A file path:

Myproj/Data/List.lean

corresponds to module:

import Myproj.Data.List

Within the file, you typically declare:

namespace Myproj.Data

Namespaces do not have to match directories exactly, but keeping them aligned avoids ambiguity and reduces the need for qualification.

Imports and Visibility

Imports are explicit. A file only sees definitions from modules it imports.

import Myproj.Basic

brings all public declarations from Myproj.Basic into scope.

You can control visibility:

open Myproj

to avoid prefixing names.

Or keep names qualified:

Myproj.hello

This choice affects readability and conflict resolution in larger projects.

Dependency Management

Dependencies are declared in lakefile.lean. For example, adding mathlib:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

Then update:

lake update
lake build

The resolved versions are stored in lake-manifest.json. This file should be committed for reproducibility.

Build Model

Lake compiles modules incrementally. A change in one file triggers recompilation of dependent modules only.

Key properties:

• compilation is deterministic under fixed toolchain and dependencies
• imports define the dependency graph
• build artifacts are cached

This model supports large developments without full rebuilds.

Minimal Working Example

Library file:

-- Myproj/Math.lean
namespace Myproj

def double (n : Nat) : Nat :=
  n + n

end Myproj

Executable:

-- Main.lean
import Myproj.Math

def main : IO Unit := do
  IO.println (toString (Myproj.double 10))

Run:

lake exe myproj

Expected output:

20

Common Pitfalls

If import Myproj.X fails, check that the file path is Myproj/X.lean.

If the editor shows unresolved imports, ensure you opened the project root, not a subdirectory.

If builds use the wrong Lean version, inspect lean-toolchain.

If dependencies fail to fetch, run lake update explicitly.

If names collide, avoid open and use qualified names.

Takeaway

A Lean project is a controlled environment defined by lean-toolchain and lakefile.lean. Files map directly to modules, and imports define all visibility. Keeping directory structure, module names, and namespaces aligned removes a large class of errors and makes larger systems manageable.