REPOSITORY DEPRECATION NOTICE

Lake has been merged into the main Lean repository (at the time of writing, in src/lake). This repository exists solely as an archive of its state prior to that merge.

Lake

Lake (Lean Make) is a new build system and package manager for Lean 4. With Lake, the package's configuration is written in Lean inside a dedicated lakefile.lean stored in the root of the package's directory.

Each lakefile.lean includes a package declaration (akin to main) which defines the package's basic configuration. It also typically includes build configurations for different targets (e.g., Lean libraries and binary executables) and Lean scripts to run on the command line (via lake script run).

This README provides information about Lake relative to the current commit. If you are looking for documentation for the Lake version shipped with a given Lean nightly, you should look at the README of that version.

Table of Contents

• Getting Lake
• Creating and Building a Package
• Glossary of Terms
• Package Configuration Options
  • Layout
  • Build & Run
  • Cloud Releases
• Defining Build Targets
  • Lean Libraries
  • Binary Executables
  • External Libraries
  • Custom Targets
• Defining New Facets
• Adding Dependencies
  • Syntax of require
• GitHub Release Builds
• Writing and Running Scripts
• Building and Running Lake from the Source
  • Building with Nix Flakes
  • Augmenting Lake's Search Path

Getting Lake

Lake is part of the lean4 repository and is distributed along with its official releases (e.g., as part of the elan toolchain). So if you have installed a semi-recent Lean 4 nightly, you should already have it!

Note that the Lake included with Lean is not updated as frequently as this repository, so some bleeding edge features may be missing. If you want to build the latest version from the source yourself, check out the build instructions at the bottom of this README.

Creating and Building a Package

To create a new package, either run lake init <package-name> [<template>] to setup the package in the current directory or lake new <package-name> [<template>] to create it in a new directory. For example, we could create the package hello like so:

$ mkdir hello
$ cd hello
$ lake init hello

or like so:

$ lake new hello
$ cd hello

Either way, Lake will initialize a git repository in the package directory with a basic .gitignore that ignores the build directory (i.e., build) where Lake outputs build files.

It will also create the root Lean file for the package's library, which uses the capitalized version of the package's name (e.g., Hello.lean in this example), and the root file for the package's binary Main.lean. They contain the following dummy "Hello World" program split across the two files:

Hello.lean

def hello := "world"

Main.lean

import «Hello»

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

Lake also creates a basic lakefile.lean for the package along with a lean-toolchain file that contains the version string of the currently active Lean, which tells elan to use that Lean toolchain for the package.

lakefile.lean

import Lake
open Lake DSL

package «hello» {
  -- add package configuration options here
}

lean_lib «Hello» {
  -- add library configuration options here
}

@[default_target]
lean_exe «hello» {
  root := `Main
}

The command lake build can then be used to build the package (and its dependencies, if it has them) into a native executable. The result will be placed in build/bin. The command lake clean deletes build.

$ lake build
...
$ ./build/bin/hello
Hello, world!

Examples of different package configurations can be found in the examples folder of this repository. You can also specified a particular configuration file template when using lake init or lake new to control what files Lake creates. See lake help init or lake help new for details.

Glossary of Terms

Lake uses a lot of terms common in software development -- like workspace, package, library, executable, target, etc. -- and some more esoteric ones -- like facet. However, whether common or not, these terms mean different things to different people, so it is important to elucidate how Lake defines these terms:

• A package is the fundamental unit of code distribution in Lake. Packages can be sourced from the local file system or downloaded from the web (e.g., via Git). The package declaration in package's lakefile names it and defines its basic properties.

• A lakefile is the Lean file that configures a package. It defines how to view, edit, build, and run the code within it, and it specifies what other packages it may require in order to do so.

• A dependency is a package required by another package and the package requiring it is its dependent. See the Adding Dependencies section for details on how to specify dependencies.

• A workspace is the broadest organizational unit in Lake. It bundles together a package (termed the root), its transitive dependencies, and Lake's environment. Every package can operate as the root of a workspace and the workspace will derive its configuration from this root.

• A module is the smallest unit of code visible to Lake's build system. It is generally represented by a Lean source file and a set of binary libraries (i.e., a Lean olean and ilean plus a system shared library if precompileModules is turned on). Modules can import one another in order to use each other's code and Lake exists primarily to facilitate this process.

• A Lean library is a collection of modules that share a single configuration. Its modules are defined by its source directory, a set of module roots, and a set of module globs. See the Lean Libraries section for more details.

• A Lean binary executable is a binary executable (i.e., a program a user can run on their computer without Lean installed) built from a Lean module termed its root (which should have a main definition). See the Binary Executables section for more details.

• An external library is a native (static) library built from foreign code (e.g., C) that is required by a package's Lean code in order to function (e.g., because it uses @[extern] to invoke code written in a foreign language). An extern_lib target is used to inform Lake of such a requirement and instruct Lake on how to build requisite library. Lake then automatically links the external library when appropriate to give the Lean code access to the foreign functions (or, more technically, the foreign symbols) it needs. See the External Libraries section for more details.

• A target is the fundamental build unit of Lake. A package can defining any number of targets. Each target has a name, which is used to instruct Lake to build the target (e.g., through lake build <target>) and to keep track internally of a target's build status. Lake defines a set of builtin target types -- Lean libraries, binary executables, and external libraries -- but a user can define their own custom targets as well. Complex types (e.g., packages, libraries, modules) have multiple facets, each of which count as separate buildable targets. See the Defining Build Targets section for more details.

• A facet is an element built from another organizational unit (e.g., a package, module, library, etc.). For instance, Lake produces olean, ilean, c, and o files all from a single module. Each of these components are thus termed a facet of the module. Similarly, Lake can build both static and shared binaries from a library. Thus, libraries have both static and shared facets. Lake also allows users to define their own custom facets to build from modules and packages, but this feature is currently experimental and not yet documented.

• A trace is a piece of data (generally a hash) which is used to verify whether a given target is up-to-date. If the trace stored with a built target matches the trace computed during build, then a target is considered up-to-date. A target's trace is derived from its various inputs (e.g., source file, Lean toolchain, imports, etc.).

Package Configuration Options

Lake provides a large assortment of configuration options for packages.

Layout

• packagesDir: The directory to which Lake should download remote dependencies. Defaults to lake-packages.
• manifestFile: The path of a package's manifest file, which stores the exact versions of its resolved dependencies. Defaults to lake-manifest.json.
• srcDir: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to lean as the -R option.)
• buildDir: The directory to which Lake should output the package's build results. Defaults to build.
• leanLibDir: The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., .olean, .ilean files). Defaults to lib.
• nativeLibDir: The build subdirectory to which Lake should output the package's native libraries (e.g., .a, .so, .dll files). Defaults to lib.
• binDir: The build subdirectory to which Lake should output the package's binary executables. Defaults to bin.
• irDir: The build subdirectory to which Lake should output the package's intermediary results (e.g., .c, .o files). Defaults to ir.

Build & Run

• precompileModules: Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked @[extern]. Defaults to false.
• moreServerArgs: Additional arguments to pass to the Lean language server (i.e., lean --server) launched by lake serve.
• buildType: The BuildType of targets in the package (see CMAKE_BUILD_TYPE). One of debug, relWithDebInfo, minSizeRel, or release. Defaults to release.
• moreLeanArgs: An Array of additional arguments to pass to lean while compiling Lean source files.
• weakLeanArgs: An Array of additional arguments to pass to lean while compiling Lean source files. Unlike moreLeanArgs, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild.
• moreLeancArgs: An Array of additional arguments to pass to leanc while compiling the C source files generated by lean. Lake already passes some flags based on the buildType, but you can change this by, for example, adding -O0 and -UNDEBUG.
• moreLinkArgs: An Array of additional arguments to pass to leanc when linking (e.g., binary executables or shared libraries). These will come after the paths of extern_lib targets.
• extraDepTargets: An Array of target names that the package should always build before anything else.

Cloud Releases

• releaseRepo?: The optional URL of the GitHub repository to upload and download releases of this package. If none (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses gh's default.
• buildArchive?: The name of the build archive on GitHub. Defaults to none. The archive's full file name will end up being nameToArchive buildArchive?.
• preferReleaseBuild: Whether to prefer downloading a prebuilt release (from GitHub) rather than building this package from the source when this package is used as a dependency.

Defining Build Targets

A Lake package can have many build targets, such as different Lean libraries and multiple binary executables. Any number of these declarations can be marked with the @[default_target] attribute to tell Lake to build them on a bare lake build of the package.

Lean Libraries

A Lean library target defines a set of Lean modules available to import and how to build them.

Syntax

lean_lib «target-name» {
  -- configuration options go here
}

Configuration Options

• srcDir: The subdirectory of the package' source directory containing the library's source files. Defaults to the package's srcDir. (This will be passed to lean as the -R option.)
• roots: An Array of root module Name(s) of the library. Submodules of these roots (e.g., Lib.Foo of Lib) are considered part of the library. Defaults to a single root of the library's upper camel case name.
• globs: An Array of module Globs to build for the library. Defaults to a Glob.one of each of the library's roots. Submodule globs build every source file within their directory. Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built.
• libName: The String name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the upper camel case name of the target.
• defaultFacets: An Array of library facets to build on a bare lake build of the library. For example, setting this to #[LeanLib.sharedLib] will build the shared library facet.
• nativeFacets: An Array of module facets to build and combine into the library's static and shared libraries. Defaults to #[Module.oFacet] (i.e., the object file compiled from the Lean source).
• precompileModules, buildType, moreLeanArgs, weakLeanArgs, moreLeancArgs, moreLinkArgs: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (debug is the lowest, and release is the highest)

Binary Executables

A Lean executable target builds a binary executable from a Lean module with a main function.

Syntax

lean_exe «target-name» {
  -- configuration options go here
}

Configuration Options

• root: The root module Name of the binary executable. Should include a main definition that will serve as the entry point of the program. The root is built by recursively building its local imports (i.e., fellow modules of the workspace). Defaults to the name of the target.
• exeName: The String name of the binary executable. Defaults to the target name with any . replaced with a -.
• supportInterpreter: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via Lean.Elab.runFrontend). Implementation-wise, this passes -rdynamic to the linker when building on a non-Windows systems. Defaults to false.
• buildType, moreLeanArgs, weakLeanArgs, moreLeancArgs, moreLinkArgs: Augments the package's corresponding configuration option. The executable's arguments come after and the build type is the minimum of the two (debug is the lowest, and release is the highest).

External Libraries

A external library target is a non-Lean static library that will be linked to the binaries of the package and its dependents (e.g., their shared libraries and executables).

Important: For the external library to link properly when precompileModules is on, the static library produced by an extern_lib target must following the platform's naming conventions for libraries (i.e., be named foo.a on Windows and libfoo.a on Unix). To make this easy, there is the Lake.nameToStaticLib utility function to convert a library name into its proper file name for the platform.

Syntax

extern_lib «target-name» (pkg : Package) :=
  -- a build function that produces its static library

The declaration is essentially a wrapper around a System.FilePath target. Like such a target, the pkg parameter and its type specifier are optional and body should be a term of type IndexBuildM (BuildJob System.FilePath) function that builds the static library.

Custom Targets

A arbitrary target that can be built via lake build <target-name>.

Syntax

target «target-name» (pkg : Package) : α :=
  -- a build function that produces a `BuildJob α`

The pkg parameter and its type specifier are optional and the body should be a term of type IndexBuildM (BuildJob α).

Defining New Facets

A Lake package can also define new facets for packages, modules, and libraries. Once defined, the new facet (e.g., facet) can be built on any current or future object of its type (e.g., through lake build pkg:facet for a package facet). Module facets can also be provided to LeanLib.nativeFacets to have Lake build and use them automatically when producing shared libraries.

Syntax

package_facet «facet-name» (pkg : Package) : α :=
  -- a build function that produces a `BuildJob α`

module_facet «facet-name» (mod : Module) : α :=
  -- a build function that produces a `BuildJob α`

library_facet «facet-name» (lib : LeanLib) : α :=
  -- a build function that produces a `BuildJob α`

In all of these, the object parameter and its type specifier are optional and the body should be a term of type IndexBuildM (BuildJob α).

Adding Dependencies

Lake packages can have dependencies. Dependencies are other Lake packages the current package needs in order to function. They can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositories. For example, one can depend on the Lean 4 port of mathlib like so:

package hello

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

The next run of lake build (or refreshing dependencies in an editor like VSCode) will clone the mathlib repository and build it. Information on the specific revision cloned will then be saved to lake-manifest.json to enable reproducibility. To update mathlib after this, you will need to run lake update -- other commands do not update resolved dependencies.

For a theorem proving packages which depend on mathlib, you can also run lake new <package-name> math to generate a package configuration file that already has the mathlib dependency (and no binary executable target).

Syntax of require

The require command has two forms:

require foo from "path"/"to"/"local"/"package" with NameMap.empty
require bar from git "url.git"@"rev"/"optional"/"path-to"/"dir-with-pkg"

The first form adds a local dependency and the second form adds a Git dependency. For a Git dependency, the revision can be a commit hash, branch, or tag. Also, the @"rev" and /"path-to"/"term" parts of the require are optional.

Both forms also support an optional with clause to specify arguments to pass to the dependency's package configuration (i.e., same as args in a lake build -- <args...> invocation). The elements of both the from and with clauses are proper terms so normal computation is supported within them (though parentheses made be required to disambiguate the syntax).

GitHub Release Builds

Lake supports uploading and downloading build artifacts (i.e., the archived build directory) to/from GitHub releases of packages to enable end users to fetch pre-built artifacts from the cloud without needed to rebuild the package from the source themselves.

Downloading

To download artifacts, one should configure the package options releaseRepo? and buildArchive? as necessary to point to the GitHub repository hosting the release and the correct artifact name within it (if the defaults are not sufficient). Then, set preferReleaseBuild := true to tell Lake to fetch and unpack it as an extra package dependency.

Lake will only fetch release builds as part of its standard build process if the package wanting it is a dependency (as the root package is expected to modified and thus not often compatible with this scheme). However, should one wish to fetch a release for a root package (e.g., after cloning the release's source but before editing), one can manually do so via lake build :release.

Lake internally uses curl to download the release and tar to unpack it, so the end user must have both tools installed to use this feature. If Lake fails to fetch a release for any reason, it will move on to building from the source. Also note that this mechanism is not technically limited to GitHub, any Git host that uses the same URL scheme works as well.

Uploading

To upload a built package as an artifact to a GitHub release, Lake provides the lake upload <tag> command as a convenient shorthand. This command uses tar to pack the package's build directory into an archive and uses gh release upload to attach it to a pre-existing GitHub release for tag. Thus, in order to use it, the package uploader (but not the downloader) needs to have gh, the GitHub CLI, installed and in PATH.

Writing and Running Scripts

A configuration file can also contain a number of scripts declaration. A script is an arbitrary (args : List String) → ScriptM UInt32 definition that can be run by lake script run. For example, given the following lakefile.lean:

import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

The script greet can be run like so:

$ lake script run greet
Hello, world!
$ lake script run greet me
Hello, me!

You can print the docstring of a script with lake script doc:

$ lake script doc greet
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.

Building and Running Lake from the Source

If you already have a Lean installation with lake packaged with it, you can build a new lake by just running lake build.

Otherwise, there is a pre-packaged build.sh shell script that can be used to build Lake. It passes it arguments down to a make command. So, if you have more than one core, you will probably want to use a -jX option to specify how many build tasks you want it to run in parallel. For example:

$ ./build.sh -j4

After building, the lake binary will be located at build/bin/lake and the library's .olean files will be located in build/lib.

Building with Nix Flakes

It is also possible to build Lake with the Nix setup buildLeanPackage from the lean4 repository. To do so, you need to have Nix installed with flakes enabled. It is recommended to also set up the Lean 4 binary cache as described in the Lean 4 repository.

It is then possible to build Lake with nix build . or run it from anywhere with nix run github:leanprover/lake.

A development environment with Lean 4 installed can be loaded automatically by running nix develop or automatically on cd with direnv by running direnv allow.

The versions of nixpkgs and lean4 are fixed to specific hashes. They can be updated by running nix flake update.

Thank Anders Christiansen Sørby (@Anderssorby) for this support!

Augmenting Lake's Search Path

The lake executable needs to know where to find the Lean library files (e.g., .olean, .ilean) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and lean.

Specifically, if Lake is co-located with lean (i.e., there is lean executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in <sysroot>/bin, their Lean libraries in <sysroot>/lib/lean, Lean's source files in <sysroot>/src/lean, and Lake's source files in <sysroot>/src/lean/lake. Otherwise, it will run lean --print-prefix to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that lake is at <lake-home>/build/bin/lake with its Lean libraries at <lake-home>/build/lib and its sources directly in <lake-home>.

This search path can be augmented by including other directories of Lean libraries in the LEAN_PATH environment variable (and their sources in LEAN_SRC_PATH). This can allow the user to correct Lake's search when the files for Lean (or Lake itself) are in non-standard locations. However, such directories will not take precedence over the initial search path. This is important during development, as this prevents the Lake version used to build Lake from using the Lake version being built's Lean libraries (instead of its own) to elaborate Lake's lakefile.lean (which can lead to all kinds of errors).