Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lake provides two commands for creating new packages: lake new creates a package in a new subdirectory, while lake init sets up a package in the current directory. Both commands generate the same set of starter files; the only difference is whether they create the directory for you.

​
lake new vs lake init

Creates a new directory named after the package, changes into it, and generates the project scaffold:
lake new hello
cd hello
This is equivalent to:
mkdir hello
cd hello
lake init hello
If you are using Lake through elan, you can create a package pinned to a specific Lean version using the + syntax:
lake +leanprover/lean4:v4.14.0 new hello

​
Templates

Both commands accept an optional template argument that controls which starter files are generated. The template is specified after the package name: 
lake new <name> [<template>][.<language>]
lake init [<name>] [<template>][.<language>]

​
Available Templates

TemplateWhat it creates
stdLibrary and executable (default)
exeExecutable only
libLibrary only
math-laxLibrary only with a Mathlib dependency
mathLibrary with Mathlib standards for linting and workflows

​
Configuration Language Suffix

Append .toml or .lean to any template name to choose the format of the generated lakefile. The default is TOML. 
lake new hello          # std template, TOML config (default)
lake new hello std      # same as above
lake new hello std.toml # same as above, explicit
lake new hello std.lean # std template, Lean DSL config
lake new hello lib.lean # lib template, Lean DSL config
lake new hello math     # math template, TOML config

​
Generated Directory Structure

Running lake new hello (default std template, TOML) creates the following layout: 
hello/
  .lake/              # Lake output directory (auto-managed)
  Hello/
    Basic.lean        # example library module
  Hello.lean          # library root; imports Hello.Basic
  Main.lean           # executable entry point (contains def main)
  lakefile.toml       # Lake package configuration
  lean-toolchain      # Lean version pin for elan
  .gitignore          # excludes .lake/ from Git
Lake also initialises a Git repository in the package directory via git init. If Git is not installed, this step is skipped silently.

​
Generated Source Files

Hello/Basic.lean — An example module with a simple definition: 
def hello := "world"
Hello.lean — The library root. Downstream code imports this module: 
-- This module serves as the root of the `Hello` library.
-- Import modules here that should be built as part of the library.
import «Hello».Basic
Main.lean — The executable entry point: 
import «Hello»

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

​
Generated lakefile.toml

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

[[lean_lib]]
name = "Hello"

[[lean_exe]]
name = "hello"
root = "Main"
  • name — the package name
  • version — the initial version (0.1.0)
  • defaultTargets — targets built by a bare lake build
  • [[lean_lib]] — declares the Hello library
  • [[lean_exe]] — declares the hello executable whose root module is Main

​
Generated lean-toolchain

leanprover/lean4:v4.x.x
This file contains the name of the Lean toolchain that Lake belongs to. elan reads this file to automatically switch to the correct Lean version when you work in the package directory.
Commit lean-toolchain to source control. It ensures every contributor and CI environment uses the same version of Lean.

​
Step-by-Step Walkthrough

1

Create the package

lake new hello
Lake creates the hello/ directory, generates all starter files, and runs git init.
2

Enter the directory

cd hello
3

Build the project

lake build
Lake compiles the Hello library and the hello executable. Outputs go to .lake/build/.
4

Run the executable

./.lake/build/bin/hello

Hello, world!
Or use lake exe to build-and-run in a single command:
lake exe hello

​
Using the math Template

For projects that depend on Mathlib, use the math or math-lax template: 
lake new myproject math
cd myproject
The generated lakefile.toml will already include a mathlib dependency: 
name = "myproject"
version = "0.1.0"

[[require]]
name = "mathlib"
scope = "leanprover-community"
After adding or updating a Mathlib dependency, always run lake exe cache get before lake build. Mathlib takes hours to build from source; the prebuilt cache saves you that time.
lake exe cache get
lake build

​
Choosing a Configuration Format

If you prefer the Lean DSL over TOML, pass the .lean suffix to any template: 
lake new hello std.lean
The generated lakefile.lean uses the Lake.DSL syntax: 
import Lake
open Lake DSL

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

lean_lib Hello

@[default_target]
lean_exe hello where
  root := `Main
You can always convert an existing TOML config to Lean DSL later: 
lake translate-config lean

Build docs developers (and LLMs) love

Get started for freeTalk to us