Using mathlib4 as a dependency

Using mathlib4 as a dependency

In a new project

To start a new project that uses mathlib4 as a dependency, first check that your elan installation is up to date. elan --version should show 2.0.0 or newer; if it is older, use elan self update.

Then run

lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math

Note: this initializes a git repository in your_project_name.

You now have a folder named your_project_name that contains a new Lake project. The lakefile.lean file is configured with the mathlib4 dependency. Continue with "Getting started" below.

In an existing project

If you already have a project and you want to use mathlib4, add these lines to your lakefile.toml:

[[require]]
name = "mathlib"
scope = "leanprover-community"

or, if you are still using a lakefile.lean:

require "leanprover-community" / "mathlib"

Then run

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

in order to set your project's Lean 4 version to the one used by mathlib4.

Getting started

In order to save time compiling all of mathlib and its dependencies, run lake exe cache get. This should output a line like

Decompressing 5000 file(s)

with a similar or larger number. Now try adding import Mathlib or a more specific import to a project file. This should take insignificant time and not rebuild any mathlib files.

Updating mathlib4

In VS Code

You can use the VS Code menu ∀ → Project Actions → Project: Update Dependency...:

and then click the "Update Lean Version" button if prompted.

From the command line

Run all of these commands in sequence:

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update

(Note that running lake update in mathlib4 itself is only useful if you are planning on making a PR to mathlib4 with this change. These instructions are only about running lake update in your downstream project which depends on mathlib4.) Running lake update triggers a hook that executes lake exe cache get.

Dealing with breakages from updating

Mathlib moves quickly, and declarations get moved or renamed. We try to add @[deprecated] attributes where possible to assist downstream users to adapt.

• If you find that a declaration seems to have disappeared, try adding import Mathlib at the top of the file, in case it has been moved to a different file. You can use #min_imports again afterwards to automatically suggest minimal imports.
• It may be helpful not to update to Mathlib master in a single step, particularly if your project is large, or a long way behind current master. Instead, update to the tagged releases of Mathlib corresponding to the stable releases and release candidates of Lean, by changing your lakefile.toml to say, for example:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0-rc1"

and then running lake update mathlib. You can then step through each version between the one you are currently on, and the one that Mathlib is now on, fixing problems incrementally. (If you are still using lakefile.lean, the syntax is require "leanprover-community" / "mathlib" @ git "v4.15.0-rc1".)

On lake exe cache

Lake projects inherit executables declared with lean_exe from their dependencies. It means that you can call lake exe cache on your project if you're using mathlib4 as a dependency. However, make sure to follow these guidelines:

• Call lake exe cache get (or other cache commands) from the root directory of your project
• If your project depends on std4 or quote4, let mathlib4 pull them transitively. That is, don't require them on your lakefile.lean
• Make sure that your project uses the same Lean 4 toolchain as the one used in mathlib4
• cache will not store and retrieve build artifacts for your project: only Mathlib and other upstream projects.