Lean theorem prover/System/Lake and Lean projects

Plain-language version: A library of mathematics

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

A single Lean source file can be checked with the command lean. Anything larger, a library of hundreds of files or a program with dependencies, is organised as a Lake package and compiled by Lake, Lean's build tool, which ships with every version of Lean. Which version of Lean a project uses is fixed by a one-line file and enforced by elan, the toolchain manager. This page shows a minimal project as files, the commands that compile and test it, and how dependencies are pinned, all with Lean 4.34.1 and the Lake that comes with it.

The toolchain

A Lean toolchain is the set of programs and files for one version of Lean, among them lean itself, lake, a C compiler (leanc, a version of Clang), the program leanchecker, and the compiled standard library and runtime. Toolchains are installed and selected by elan. The lean and lake commands a user types are small proxies installed by elan. Each looks for a file named lean-toolchain in the current directory and its parents, reads the toolchain named there, installs it if it is missing, and runs the program from that toolchain. A command can also name a toolchain directly, as in lake +leanprover/lean4:v4.34.1 new greeting.

The file holds one line:

leanprover/lean4:v4.34.1

The part before the colon names where toolchains come from, and the part after it the version. A project's file should name an exact version, not a channel such as stable, so that everyone working on it uses the same Lean. Changing the version is a one-line edit; the new toolchain is downloaded the next time it is needed. This matters more for a proof assistant than for most languages. The elaborator, the tactics and the library change from one version of Lean to the next, and a proof that is accepted under one version may fail under another. The toolchain file records under which version a body of proofs was checked.

A minimal Lake package

lake new greeting creates a directory with a library, an executable and a configuration file. With Lean 4.34.1 the configuration it writes, lakefile.toml, is:

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

[[lean_lib]]
name = "Greeting"

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

The first lines describe the Lake package itself. Each [[lean_lib]] table declares a library, a collection of Lean modules under a root name, here Greeting; each [[lean_exe]] declares an executable, a program whose Lean module defines main. The source files follow the names. Greeting.lean is the root of the library and imports its parts:

-- This module serves as the root of the `Greeting` library.
-- Import modules here that should be built as part of the library.
import Greeting.Basic

Greeting/Basic.lean holds the one definition:

def hello := "world"

and Main.lean is the program:

import Greeting

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

A Lean module's name is its path: Greeting/Basic.lean is the Lean module Greeting.Basic, and import Greeting.Basic refers to it. Lake reads the imports to work out the order in which the Lean modules must be compiled.

The configuration can also be written in Lean, as lakefile.lean. lake new greet2 std.lean writes:

import Lake
open Lake DSL

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

lean_lib «Greet2» where
  -- add library configuration options here

@[default_target]
lean_exe "greet2" where
  root := `Main

The TOML form is purely declarative. The Lean form is a Lean program and can compute its configuration or define new kinds of target.

Compiling

lake build compiles the default targets and everything they need. In the new directory it reports:

info: greeting: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
✔ [2/8] Built Greeting.Basic (277ms)
✔ [3/8] Built Greeting.Basic:c.o (58ms)
✔ [4/8] Built Greeting (225ms)
✔ [5/8] Built Greeting:c.o (66ms)
✔ [6/8] Built Main (244ms)
✔ [7/8] Built Main:c.o (69ms)
✔ [8/8] Built greeting:exe (289ms)
Build completed successfully (8 jobs).

The first two lines appear on the first run only, and the times in brackets vary from run to run. Each Lean module is elaborated, which produces an .olean file holding its definitions and theorems in compiled form, and C code, which is compiled to an object file (:c.o); the object files are linked into the executable. lake exe greeting then prints Hello, world!.

Elaboration includes the Lean kernel's check of every definition and theorem, so a Lake build of a Lean module that finishes without errors or warnings gives the same assurance as opening it in an editor and seeing it accepted: every theorem in it, and in everything it imports, has been checked. The reference manual makes the comparison explicitly.

Running lake build again with nothing changed prints only Build completed successfully (8 jobs). Lake keeps a trace for every output, recording a digest of each input from which it was made; when no input has changed, the output is reused and its saved messages are replayed instead of being produced again. Lake keeps its working state under the directory .lake/: compiled outputs in .lake/build/ and the sources of dependencies in .lake/packages/.

Testing

lake test runs the Lake package's test driver, a target named in the configuration. Lake is not a test framework: it finds the driver, compiles it, and, for an executable, runs it and treats a non-zero exit code as failure. A library can serve as the driver, and then any elaboration error counts as a failure, including a failed #guard. Adding testDriver = "GreetingTest" and a second library to the configuration,

[[lean_lib]]
name = "GreetingTest"

with the file GreetingTest.lean

import Greeting

#guard hello == "world"
#guard hello.length == 5

makes lake test succeed. Changing the last line to claim a length of 6 makes it fail, with this among its messages:

error: GreetingTest.lean:4:0: Expression
  hello.length == 6
did not evaluate to `true`

For a library of proofs the distinction between compiling and testing is thin. A theorem that is false, or whose proof is broken, does not compile.

Dependencies

A Lake package may require others. In lakefile.toml each dependency is a [[require]] table. A dependency can come from Reservoir, an online index of Lake packages, from a Git repository at a given revision, or from a local path. The reference manual's example of a dependency taken from Reservoir is:

[[require]]
name = "example"
version = "≥2.12.0"
scope = "exampleDev"

The configuration says which dependencies are wanted. The file lake-manifest.json says exactly which versions are in use: for each dependency it records the source and the precise revision. Lake brings each dependency's local copy into line with lake-manifest.json before compiling, and creates the file if it is missing; lake update moves the recorded revisions forward. The file is meant to be kept with the source. For the minimal project, which has no dependencies, Lake wrote:

{"version": "1.2.0",
 "packagesDir": ".lake/packages",
 "packages": [],
 "name": "greeting",
 "lakeDir": ".lake",
 "fixedToolchain": false}

Together, lean-toolchain, the configuration file and lake-manifest.json fix the version of Lean and the exact source of every dependency. That is what makes a Lean project reproducible: another person, or the same person years later, can obtain the same toolchain and the same dependencies and have every proof checked again. The large mathematical libraries described in a library of mathematics are distributed in this form.

Next

Proof export and independent checkers describes how the results of a Lake build can be checked again outside the program that produced them.