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 packages can depend on other Lake packages. A dependency can come from Reservoir (the official Lean package registry), a Git repository URL, or a local path on disk. Lake records the exact resolved revision of every dependency in lake-manifest.json, ensuring reproducible builds across machines and time.
Adding a Dependency
Lean DSL — require
The require keyword in a Lean lakefile has the following general form:
require ["<scope>" /] <pkg-name> [@ <version>]
[from <source>] [with <options>]
from clause specifies where Lake should find the package. Without a from clause, Lake looks up the package in the default registry (Reservoir).
-- From Reservoir (no 'from' clause needed)
require "leanprover-community" / "mathlib"
-- Specific version from Reservoir
require "leanprover-community" / "mathlib" @ "4.14.0"
-- Specific Git revision from Reservoir
require "leanprover-community" / "mathlib" @ git "abc123def"
-- From a local path
require mylib from "../mylib"
-- From a Git URL
require mylib from git "https://github.com/myorg/mylib" @ "main"
-- From a Git URL with a subdirectory
require mylib from git "https://github.com/myorg/monorepo" @ "v2.0.0" / "packages/mylib"
-- With configuration options passed to the dependency
require mylib from "../mylib" with { "someOption" = "value" }
TOML — [[require]]
In lakefile.toml, each dependency is an entry in the [[require]] array:
# Reservoir dependency (version range)
[[require]]
name = "mathlib"
scope = "leanprover-community"
version = "4.14.0"
# Reservoir dependency (specific Git revision)
[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "abc123def456"
# Local path dependency
[[require]]
name = "mylib"
path = "../mylib"
# Git URL dependency
[[require]]
name = "mylib"
git = "https://github.com/myorg/mylib"
rev = "main"
# Git URL with subdirectory
[[require]]
name = "mylib"
git = "https://github.com/myorg/monorepo"
rev = "v2.0.0"
subDir = "packages/mylib"
Dependency Source Types
Reservoir (Default Registry)
If no from/path/git clause is given, Lake looks up the package in Reservoir and downloads the version matching the constraint.
require "leanprover-community" / "mathlib"
[[require]]
name = "mathlib"
scope = "leanprover-community"
For Mathlib specifically, always run lake exe cache get before lake build after adding or updating the dependency. Otherwise Mathlib will be compiled from source, which can take hours.lake exe cache get
lake build
Local Path Dependencies
Lake loads a package from a fixed path relative to the requiring package’s directory:
require mylib from "../mylib"
[[require]]
name = "mylib"
path = "../mylib"
lake-manifest.json.
Git Dependencies
Lake clones a Git repository at a specified URL and checks out a revision (commit hash, branch, or tag):
require mylib from git "https://github.com/myorg/mylib" @ "v1.2.3"
require mylib from git "https://github.com/myorg/mylib" @ "main"
[[require]]
name = "mylib"
git = "https://github.com/myorg/mylib"
rev = "v1.2.3"
rev is given, Lake defaults to master.
The URL of the Git repository.
The Git revision to check out — a commit hash, branch name, or tag.
A subdirectory within the Git repository that contains the package. Useful for monorepos.[[require]]
name = "mylib"
git = "https://github.com/myorg/monorepo"
rev = "main"
subDir = "packages/mylib"
The lake-manifest.json File
When Lake first resolves a dependency (e.g. on the first lake build or after lake update), it writes the resolved revision of every Git dependency to lake-manifest.json in the package root. This file ensures that every subsequent build — on any machine — uses exactly the same versions.
{
"version": "0.1.2",
"packagesDir": ".lake/packages",
"packages": [
{
"type": "git",
"name": "mathlib",
"url": "https://github.com/leanprover-community/mathlib4",
"rev": "abc123def456...",
"inputRev": "v4.14.0",
"subDir": null
}
],
"directDependencies": ["mathlib"]
}
Always commit lake-manifest.json to source control. Without it, different contributors may end up with different versions of your dependencies, causing build inconsistencies.
lake update — Update the Manifest
lake update [<package>...]
lake update (aliased as lake upgrade) refreshes lake-manifest.json, resolving dependencies to the latest compatible versions:
lake update # upgrade all dependencies
lake update mathlib # upgrade only mathlib to the latest compatible version
lake update mathlib foo # upgrade mathlib and foo
lake build does not update dependencies. Package dependencies are only updated when you explicitly run lake update. This prevents unexpected version changes during builds.
packagesDir (default: .lake/packages/<name>).
Version Specification
In the require statement you can constrain the version Lake will accept from Reservoir:
-- Accept any version compatible with 4.14.0
require "leanprover-community" / "mathlib" @ "4.14.0"
-- Accept a specific Git revision
require "leanprover-community" / "mathlib" @ git "abc123def"
# Accept version 4.14.0 or compatible
[[require]]
name = "mathlib"
scope = "leanprover-community"
version = "4.14.0"
# Accept a specific Git revision
[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "abc123def"
Use version for Reservoir-hosted packages (which have proper semver releases) and rev for pinning to an exact commit or branch.
Passing Options to Dependencies
Both require forms support passing NameMap String options to configure the dependency. This is equivalent to passing -K key=value on the command line for that dependency:
require mylib from "../mylib" with { "featureFlag" = "true" }
[[require]]
name = "mylib"
path = "../mylib"
options = { featureFlag = "true" }
Reservoir — The Lean Package Index
Reservoir is the official Lean package registry. It indexes open-source Lake packages and makes them discoverable and downloadable. When you require a package without a from clause, Lake queries Reservoir to resolve the name and version.
Packages are identified on Reservoir by a scope/name pair (e.g. leanprover-community/mathlib).
To list your own package on Reservoir, make sure your lakefile.toml (or lakefile.lean) includes name, version, description, license, and keywords. Reservoir will index public GitHub repositories automatically.To opt a package out of Reservoir’s index, set reservoir = false in the lakefile.
GitHub Release Builds (Cloud Releases)
Lake can download pre-built artefacts from a GitHub release instead of building a dependency from source. This is configured via the dependency package’s own lakefile:
# In the dependency's lakefile.toml
releaseRepo = "https://github.com/myorg/mypackage"
preferReleaseBuild = true
lake build, Lake will attempt to download the pre-built archive from GitHub and unpack it into the build directory. If the download fails for any reason, Lake falls back to building from source.
Release builds require curl and tar on the end user’s machine. To upload a release archive, the publisher needs the GitHub CLI (gh) installed.# Build and upload a release for tag v1.0.0
lake build
lake upload v1.0.0
Complete Dependency Example
name = "myproject"
version = "0.1.0"
# Mathlib from Reservoir
[[require]]
name = "mathlib"
scope = "leanprover-community"
version = "4.14.0"
# A local utility library
[[require]]
name = "myutils"
path = "../myutils"
# A library from a specific Git commit
[[require]]
name = "somelib"
git = "https://github.com/example/somelib"
rev = "v2.3.1"
[[lean_lib]]
name = "MyProject"
import Lake
open Lake DSL
package "myproject" where
version := v!"0.1.0"
-- Mathlib from Reservoir
require "leanprover-community" / "mathlib" @ "4.14.0"
-- A local utility library
require myutils from "../myutils"
-- A library from a specific Git commit
require somelib from git "https://github.com/example/somelib" @ "v2.3.1"
lean_lib MyProject
