Building Projects

• So far we have run Lean files one at a time
• Real projects have multiple files, dependencies, and build steps
• DEBT: explain doc comments

Single-File Programs

def main : IO Unit := do
  IO.println "Hello from a single file!"
  IO.println s!"2 + 2 = {2 + 2}"

• Run a single Lean file from the terminal with lean filename.lean
  • Like python script.py
• def main : IO Unit is the entry point
  • Lean executes main when you run the compiled file
• For experiments and learning, single files are fine
  • For anything larger, use Lake

What Is Lake?

• Lake is Lean's build system and package manager
  • Like Python's uv, Rust's cargo, or Node's npm
• A lakefile called lakefile.lean describes the project
  • Name, source files, and dependencies
  • It is a Lean file that uses the Lake DSL
• import Lake and open Lake DSL bring the build language into scope
• package names the project; lean_exe defines an executable target

Creating a Project

-- Contents of lakefile.lean created by: lake new MyProject
import Lake
open Lake DSL

package «MyProject» where
  name := "MyProject"

lean_exe «MyProject» where
  root := `Main

• lake new MyProject creates a fresh project directory
  • Generates a lakefile.lean, a Main.lean, and a .lake/ cache directory
  • Like uv init or cargo new
• lake init does the same thing inside an existing directory
• The workspace is the directory that contains lakefile.lean
  • All build commands are run from the workspace root

Minimal Lake File

• package names the project; the «» angle-quote syntax allows spaces in names
  • Type \f<< and \f>> to get the angle quotes
• lean_exe defines an executable target (a compiled binary you can run)
  • root := \Maintells Lake to look fordef maininMain.lean`
    • The backtick before Main is Lean's syntax for a Name literal
    • It's like writing "Main" but using Lean's internal name type instead of a string

Building from the Command Line

-- Main.lean: entry point for the compiled executable
def main : IO Unit := do
  IO.println "Built with Lake!"

• lake build compiles all targets in the project
  • Like cargo build or uv run python -m build
• The compiled binary lands in .lake/build/bin/
• Lake only recompiles files that have changed
  • Fast for large projects because the .lake/ directory caches intermediate results
• Lake also accepts a target name: lake build MyTarget

Running an Executable

• lake exe targetname builds and runs an executable in one step
  • Like cargo run in Rust
• If the project is already built, lake exe skips the compile step
• The executable name is whatever you wrote after lean_exe in lakefile.lean

Multiple Source Files

-- Helpers.lean: a helper module in the same project
namespace Helpers

def greet (name : String) : String :=
  s!"Hello, {name}!"

def shout (msg : String) : String :=
  msg.toUpper ++ "!!!"

end Helpers

• Split large projects into multiple .lean files
  • Each file becomes a module that other files can import
• File names must start with a capital letter
  • Helpers.lean → module MyProject.Helpers
  • The project name prefix comes from package in lakefile.lean
• Use namespace … end to group related definitions within a file

Importing Your Own Modules

-- Main.lean: imports and uses the Helpers module
import MyProject.Helpers

def main : IO Unit := do
  IO.println (Helpers.greet "Lake")
  IO.println (Helpers.shout "lean")

Build completed successfully (0 jobs).
Hello, Lake!
LEAN!!!

• import MyProject.Helpers brings Helpers.lean into scope
  • The full path is PackageName.FileName (no .lean extension)
• After importing, call functions with the namespace prefix: Helpers.greet
  • Or open Helpers in greet to drop the prefix for one expression
• Import order matters: Lean processes files top to bottom
  • Cannot have circular imports

Libraries vs. Executables

import Lake
open Lake DSL

package «myproject» where
  name := "myproject"

-- A library target: compiled but not directly runnable
lean_lib «MathUtils» where
  srcDir := "lib"

-- An executable target: produces a runnable binary
lean_exe «myproject» where
  root := `Main

warning: /private/var/folders/jn/dg894s5542dbrw7ry6sks0r80000gn/T/tmp.c62TtdrWr9/lakefile.lean:5:2: unknown 'PackageConfig' field 'name'
info: myproject: no previous manifest, creating one from scratch
info: toolchain not updated; no toolchain information found
Build completed successfully (0 jobs).

• lean_lib compiles source files into a reusable library
  • Produces .olean files (pre-compiled Lean objects) but no binary
  • Other packages can depend on it with require
  • Lake knows to create a library because you used lean_lib: the keyword determines the target type
• lean_exe links source files into a runnable binary
  • Must have a def main : IO Unit in the root file
• One project can define both: libraries and executables are separate targets

Running Lean in Project Context

-- script.lean: a standalone script that uses project modules
import MyProject.Helpers

#eval Helpers.greet "world"

Build completed successfully (0 jobs).
"Hello, world!"

• lake env lean file.lean runs lean with the project's modules on the path
  • Without lake env, imports that refer to your project's modules fail
  • Like Python's uv run python script.py vs. bare python script.py
• Use lake env lean for one-off scripts that need project modules but aren't targets

Adding a Dependency

import Lake
open Lake DSL

package «myproject» where
  name := "myproject"

-- Add an external dependency from a git repository
require Std from git
    "https://github.com/leanprover/std4" @ "main"

lean_exe «myproject» where
  root := `Main

warning: /private/var/folders/jn/dg894s5542dbrw7ry6sks0r80000gn/T/tmp.dMhSDydxYA/lakefile.lean:5:2: unknown 'PackageConfig' field 'name'
info: myproject: no previous manifest, creating one from scratch
info: Std: cloning https://github.com/leanprover/std4
info: Std: checking out revision '708b057842c4cd0845fba132bd94b08493f6fc42'
info: updating toolchain to 'leanprover/lean4:v4.31.0-rc1'
info: restarting Lake via Elan
info: Version 4.2.2 of elan is available! Use `elan self update` to update.
info: downloading https://releases.lean-lang.org/lean4/v4.31.0-rc1/lean-4.31.0-rc1-darwin_aarch64.tar.zst
info: installing /Users/gvwilson/.elan/toolchains/leanprover--lean4---v4.31.0-rc1
warning: /private/var/folders/jn/dg894s5542dbrw7ry6sks0r80000gn/T/tmp.dMhSDydxYA/lakefile.lean:5:2: unknown 'PackageConfig' field 'name'
info: myproject: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date

• require PackageName from git "url" @ "ref" declares an external dependency
  • Lake fetches the package and caches it in .lake/packages/
• After editing lakefile.lean, run lake update to download the dependency
  • Then import its modules just like your own
• Std is the Lean standard library extension; Mathlib is the math library
  • Both are added with require
• For local packages not on a git remote, use a path: lean require MyLib from "../my-lib"
  • Like a Python editable install or a Rust path dependency

Namespaces Across Files

-- MathUtils/Basic.lean
-- The module path is MyProject.MathUtils.Basic
-- The namespace should match the module path by convention
namespace MathUtils.Basic

def square (n : Int) : Int := n * n
def cube (n : Int) : Int := n * n * n

end MathUtils.Basic

• By convention, namespace names should match the module import path
  • File MathUtils/Basic.lean → module MyProject.MathUtils.Basic
  • Namespace inside that file: MathUtils.Basic
• This isn't enforced by the compiler, but it makes code easier to navigate
  • Like Python's module names matching the file names
• open Namespace in expr uses the namespace for one expression without open polluting the whole file

-- Fix: this file uses Utils.greet but forgets to import it
-- Add the missing import at the top

def main : IO Unit := do
  IO.println (Utils.greet "world")

-- Fix: this target should be an executable, not a library
import Lake
open Lake DSL

package «app» where
  name := "app"

lean_lib «app» where
  root := `Main

-- Fix: the module name is wrong — Lean module names match the filename
-- The file is 'Helpers.lean' but the import uses a lowercase name
import MyProject.helpers

def main : IO Unit := do
  IO.println (Helpers.greet "world")

-- Fix: executables need a 'main' function
-- This file is set as the root of a lean_exe but has no main

def greet : String := "Hello!"

-- Fix: the function is defined in namespace 'Foo' but called as 'Bar.func'
namespace Foo

def func : String := "from Foo"

end Foo

def main : IO Unit := do
  IO.println Bar.func

-- Fix: srcDir points to the wrong location
-- The .lean files are in 'src/' but lakefile says 'source/'
import Lake
open Lake DSL

package «myapp» where
  name := "myapp"

lean_exe «myapp» where
  root := `Main
  srcDir := "source"

-- Write: fill in the blanks to create a lakefile for an executable called 'greeter'
import Lake
open Lake DSL

package «greeter» where
  name := "greeter"

-- TODO: add a lean_exe target called 'greeter' with root `Main

-- Write: add a main function that prints "Hello, Lake!"
-- def main : IO Unit := ???

-- Write: implement greet using string interpolation
namespace Greeter

def greet (name : String) : String :=
  ""  -- replace with s!"Hello, {name}!"

end Greeter

#eval Greeter.greet "world"

-- Write: add the missing import and fix the main function
-- Assume MyProject.Greeter defines Greeter.greet

def main : IO Unit := do
  IO.println (Greeter.greet "World")

-- Write: add a lean_lib target called 'MathLib'
import Lake
open Lake DSL

package «myproject» where
  name := "myproject"

lean_exe «myproject» where
  root := `Main

-- TODO: add a lean_lib target named 'MathLib'

-- Write: the namespace should match the module name 'StringUtils'
-- Currently it's 'StrUtil' — fix it
namespace StrUtil

def shout (s : String) : String := s.toUpper ++ "!!!"

end StrUtil

#eval StrUtil.shout "hello"