Starting a Project

As a program written in Lean becomes more serious, an ahead-of-time compiler-based workflow that results in an executable becomes more attractive. Like other languages, Lean has tools for building multiple-file packages and managing dependencies. The standard Lean build tool is called Lake (short for "Lean Make"), and it is configured in Lean. Just as Lean contains a special-purpose language for writing programs with effects (the do language), Lake contains a special-purpose language for configuring builds. These languages are referred to as embedded domain-specific languages (or sometimes domain-specific embedded languages, abbreviated EDSL or DSEL). They are domain-specific in the sense that they are used for a particular purpose, with concepts from some sub-domain, and they are typically not suitable for general-purpose programming. They are embedded because they occur inside another language's syntax. While Lean contains rich facilities for creating EDSLs, they are beyond the scope of this book.

First steps

To get started with a project that uses Lake, the command lake new greeting in a directory that does not already contain a file or directory called greeting. This creates a directory called greeting that contains the following files:

  • Main.lean is the file in which the Lean compiler will look for the main action.
  • Greeting.lean is the scaffolding of a support library for the program.
  • lakefile.lean contains the configuration that lake needs to build the application.
  • lean-toolchain contains an identifier for the specific version of Lean that is used for the project.

Additionally, lake new initializes the project as a Git repository and configures its .gitignore file to ignore intermediate build products. Typically, the majority of the application logic will be in a collection of libraries for the program, while Main.lean will contain a small wrapper around these pieces that does things like parsing command lines and executing the central application logic. To create a project in an already-existing directory, run lake init instead of lake new.

By default, the library file Greeting.lean contains a single definition:

def hello := "world"

while the executable source Main.lean contains:

import Greeting

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

The import line makes the contents of Greeting.lean available in Main.lean.

To build the package, run the command lake build. After a number of build commands scroll by, the resulting binary has been placed in build/bin. Running ./build/bin/greeting results in Hello, world!.

Lakefiles

A lakefile.lean describes a package, which is a coherent collection of Lean code for distribution, analogous to an npm or nuget package or a Rust crate. A package may contain any number of libraries or executables. While the documentation for Lake describes the available options in a lakefile, it makes use of a number of Lean features that have not yet been described here. The generated lakefile.lean contains the following:

import Lake
open Lake DSL

package greeting {
  -- add package configuration options here
}

lean_lib Greeting {
  -- add library configuration options here
}

@[default_target]
lean_exe greeting {
  root := `Main
}

This initial Lakefile consists of three items:

  • a package declaration, named greeting,
  • a library declaration, named Greeting, and
  • an executable, also named greeting.

Each Lakefile will contain exactly one package, but any number of libraries or executables. Additionally, Lakefiles may contain external libraries, which are libraries not written in Lean to be statically linked with the resulting executable, custom targets, which are build targets that don't fit naturally into the library/executable taxonomy, dependencies, which are declarations of other Lean packages (either locally or from remote Git repositories), and scripts, which are essentially IO actions (similar to main), but that additionally have access to metadata about the package configuration. The items in the Lakefile allow things like source file locations, module hierarchies, and compiler flags to be configured. Generally speaking, however, the defaults are reasonable.

Libraries, executables, and custom targets are all called targets. By default, lake build builds those targets that are annotated with @[default_target]. This annotation is an attribute, which is metadata that can be associated with a Lean declaration. Attributes are similar to Java annotations or C# and Rust attributes. They are used pervasively throughout Lean. To build a target that is not annotated with @[default_target], specify the target's name as an argument after lake build.

Libraries and Imports

A Lean library consists of a hierarchically organized collection of source files from which names can be imported, called modules. By default, a library has a single root file that matches its name. In this case, the root file for the library Greeting is Greeting.lean. The first line of Main.lean, which is import Greeting, makes the contents of Greeting.lean available in Main.lean.

Additional module files may be added to the library by creating a directory called Greeting and placing them inside. These names can be imported by replacing the directory separator with a dot. For instance, creating the file Greeting/Smile.lean with the contents:

def expression : String := "a big smile"

means that Main.lean can use the definition as follows:

import Greeting
import Greeting.Smile

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

The module name hierarchy is decoupled from the namespace hierarchy. In Lean, modules are units of code distribution, while namespaces are units of code organization. That is, names defined in the module Greeting.Smile are not automatically in a corresponding namespace Greeting.Smile. Modules may place names into any namespace they like, and the code that imports them may open the namespace or not. import is used to make the contents of a source file available, while open makes names from a namespace available in the current context. In the Lakefile, the line import Lake makes the contents of the Lake module available, while the line open Lake DSL makes the contents of the Lake and DSL namespaces available without any prefixes. The Lake module places names into both the Lake and DSL namespaces.