Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

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

Mathlib4 uses Lake — Lean 4’s official build system and package manager — for all build, test, and tooling tasks. Because Mathlib is a large library with hundreds of thousands of lines of Lean code, building it from scratch takes several hours on modern hardware. The precompiled .olean cache makes iterative development practical by letting you download the artifacts already built by CI. This page is a complete reference for every build and test command you will need as a contributor.

​
Prerequisites

  • Lean 4 and elan installed via the community getting-started guide. elan manages Lean toolchain versions; it automatically activates the correct version when you cd into the mathlib4 directory.
  • lake — ships with every elan-managed Lean installation. No separate installation is needed.
  • Git — to clone the repository and manage branches.
  • GitHub CLI gh (optional) — needed only for the autolabel tool.
Run lean --version and lake --version inside the mathlib4 directory to confirm you are using the pinned toolchain. If the versions do not match the lean-toolchain file, run elan toolchain install leanprover/lean4:$(cat lean-toolchain | cut -d: -f2).

​
Standard Build Workflow

1
Clone the repository (first-time setup)
2
git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
3
If you are contributing, clone your fork instead:
4
git clone https://github.com/<your-username>/mathlib4.git
cd mathlib4
5
Fetch the precompiled .olean cache
6
Always run this first. Skipping it means the next build step will recompile everything from scratch, which takes hours:
7
lake exe cache get
8
This downloads .olean and .ilean files produced by Mathlib’s CI pipeline. The cache is keyed to the exact commit hash of your working tree, so you may need to re-run it after rebasing or after pulling upstream changes.
9
Build Mathlib
10
With the cache in place, a full build should complete in a few minutes as Lake only needs to compile files not covered by the cache:
11
lake build
12
A successful build produces no error output. Warnings may appear but do not indicate failure.
13
Build a specific file
14
To build (and type-check) a single Lean module, pass its dot-separated import path:
15
lake build Mathlib.Algebra.Group.Defs
lake build Mathlib.Data.List.Basic
lake build Mathlib.Topology.Basic
16
This is the fastest way to iterate on a single file during development — you do not need to wait for the full library to build.
17
Run the test suite
18
lake test
19
This runs all tests defined under MathlibTest/ using the MathlibTest test driver declared in lakefile.lean. A clean pass is required before opening a PR.
20
Run the style linter
21
lake exe lint-style
22
This executes both the Python-based text linters (from scripts/lint-style.py) and the Lean-based style linters. All reported issues must be resolved before requesting review. See the Style Guide for the full list of rules being checked.
23
Register any new files
24
If you added a new .lean source file to the library, regenerate the top-level Mathlib.lean import file so the new module is included in the build:
25
lake exe mk_all
26
Commit the updated Mathlib.lean as part of the same PR as your new file.

​
Command Reference

​
Fetching and Managing the Cache

CommandDescription
lake exe cache getDownload precompiled .olean files for the current commit
lake exe cache get!Force re-download even if local files are present
lake exe cachePrint the full cache help menu
If a build fails with mysterious errors after a rebase, run lake clean followed by lake exe cache get to start fresh. This resolves most cases of stale artifacts.

​
Building

CommandDescription
lake buildBuild all of Mathlib (fast with cache, slow without)
lake build Mathlib.X.Y.ZBuild a specific module and its dependencies
lake build ArchiveBuild the Archive library
lake build CounterexamplesBuild the Counterexamples library
lake cleanRemove all build artifacts under .lake/build
lake clean deletes all cached build outputs. After running it, you must run lake exe cache get again before building, or the next lake build will recompile everything from scratch.
Alternatively, remove the entire .lake directory for a fully clean slate: 
rm -rf .lake
lake exe cache get
lake build

​
Testing and Linting

CommandDescription
lake testRun the full Mathlib test suite
lake exe lint-styleRun text-based and Lean-based style linters
lake exe check-yamlVerify all declarations referenced in docs/*.yaml exist
lake exe mk_allRegenerate Mathlib.lean to include all source files
lake exe autolabel <PR>Auto-assign topic labels to a GitHub PR

​
Checking PR Titles

The check_title_labels executable validates that a PR title obeys Mathlib’s formatting requirements: 
lake exe check_title_labels
This is run automatically by CI but can be tested locally before opening a PR.

​
Cleaning Build Artifacts

Two levels of cleaning are available depending on how thoroughly you want to reset: 
# Level 1: remove build outputs, keep the cache index
lake clean

# Level 2: remove everything, including the downloaded cache
rm -rf .lake
After a Level 2 clean, always re-fetch the cache: 
lake exe cache get

​
Building HTML Documentation Locally

The mathlib4_docs repository is responsible for generating and publishing the official HTML documentation at leanprover-community.github.io/mathlib4_docs. To build the docs locally, clone that repository alongside your mathlib4 checkout: 
git clone https://github.com/leanprover-community/mathlib4_docs.git
cd mathlib4_docs
cp ../mathlib4/lean-toolchain .
lake exe cache get
lake build Mathlib:docs
The final lake build Mathlib:docs step can take 20 minutes or more even with the cache. The generated HTML files are placed in .lake/build/doc/ and can be viewed in any browser.

​
Continuous Integration

Mathlib’s CI is powered by GitHub Actions. The primary workflow is defined in .github/workflows/build.yml. Every push to a PR branch triggers:
  1. A full lake build across Linux runners.
  2. The test suite (lake test).
  3. The style linter (lake exe lint-style).
  4. The YAML checker (lake exe check-yaml).

​
Bors Merge Queue

Mathlib does not allow direct pushes to master. All merges go through Bors, an automated merge bot. When a reviewer approves a PR, they post: 
bors r+
Bors batches approved PRs, runs a final CI build, and merges passing batches atomically. This ensures master is always in a passing state.

​
Downstream Testing

The DownstreamTest/ directory contains tests that verify Mathlib’s compatibility with downstream projects. These are run periodically rather than on every PR, but failures there can block releases.

​
Dependency Management

Mathlib’s upstream dependencies (Batteries, Aesop, Qq, ProofWidgets, importGraph, LeanSearchClient, plausible) are declared in lakefile.lean. To update them: 
lake update
To update only a subset: 
lake update batteries aesop
This modifies lake-manifest.json. Commit that file and open a PR to land the dependency update.
Do not run lake update -Kdoc=on. Documentation-related dependencies are only included when CI builds documentation, and running that command locally will produce an incorrect lake-manifest.json.

​
Gitpod and GitHub Codespaces

If you prefer a browser-based development environment with Lean and Lake pre-installed:
  • GitHub Codespaces: click the “Open in GitHub Codespaces” badge on the repository homepage.
  • Gitpod: click the “Open in Gitpod” badge, or navigate to gitpod.io/#https://github.com/leanprover-community/mathlib4.
Both environments run lake exe cache get automatically on startup so you can begin editing immediately.

Build docs developers (and LLMs) love

Get started for freeTalk to us