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.lean:

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

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.

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