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

(Despite the +leanprover/lean4:nightly-2023-02-04 argument apparently referencing an old version of Lean, this will set the Lean version in your new project to match the current version used by mathlib4.)

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

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

(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.)

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