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, run

lake +leanprover/lean4:nightly-2023-02-04 new <your_project_name> math

This uses the Lake version with the most recent new math implementation independent of your default elan toolchain. 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. lean-toolchain points to the same version of Lean 4 as used by mathlib4. 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 -L 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 2342 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

Run these commands in sequence:

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

More 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