-
Notifications
You must be signed in to change notification settings - Fork 303
Using mathlib4 as a dependency
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.
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.
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.
You can use the VS Code menu ∀ → Project Actions → Project: Update Dependency...:
and then click the "Update Lean Version" button if prompted.
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
.
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 othercache
commands) from the root directory of your project - If your project depends on
std4
orquote4
, letmathlib4
pull them transitively. That is, don'trequire
them on yourlakefile.lean
- Make sure that your project uses the same Lean 4 toolchain as the one used in
mathlib4