This is the work in progress port of mathlib to Lean 4.
A guide on how to port a file from mathlib3 to mathlib4 can be found in the wiki.
The porting effort is coordinated through zulip,
if you want to contribute to the port please come to the mathlib4
stream.
- Make sure Lean is not running, and close all instances of VSCode running Lean processes.
- Get the newest version of
elan
. If you already have installed a version of Lean, you can runIf the above command fails, or if you need to installelan self update
elan
, runIf this also fails, follow the instructions undercurl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Regular install
here. - To build
mathlib4
runlake build
. To build and run all tests, runmake
. - You can use
lake build +Mathlib.Import.Path
to build a particular file, e.g.lake build +Mathlib.Algebra.Group.Defs
. - If you added a new file, run the following command to update
Mathlib.lean
find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
Run lake exe cache get
to download cached build files that are computed by mathlib4
's automated workflow.
If tar
terminates with an error, it means that you might have ended up with corrupted files.
In this case, run lake exe cache get!
to overwrite them (get
won't try to download the same file again).
Call lake exe cache
to see its help menu.
Building HTML documentation locally is straightforward:
lake -Kdoc=on build Mathlib:docs
The HTML files can then be found in build/doc
.
If you want to update dependencies, use lake update -Kdoc=on
.
This will update the lake-manifest.json
file correctly.
You will need to make a PR after committing the changes to this file.
To start a new project that uses mathlib4 as a dependency, run elan run leanprover/lean4:nightly-2023-02-04 lake 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.
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.
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.
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
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