From 7d80b8c6dd9d21a1665129452512cd4a08837e2c Mon Sep 17 00:00:00 2001 From: Lukas Gerlach <12497479+monsterkrampe@users.noreply.github.com> Date: Mon, 19 Feb 2024 08:03:20 +0100 Subject: [PATCH] Update Mathlib Note in README.md --- README.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 32505c7..8ba434b 100644 --- a/README.md +++ b/README.md @@ -5,9 +5,12 @@ The project started and still emerges mostly through student projects. You are w ## Notes on Setup: -Using `elan` / `lake`: +Using [`elan`](https://github.com/leanprover/elan) / `lake`: ``` lake build ``` -This will download mathlib4 and build the project. Currently it might still break, because -mathlib4 has no releases yet. (Todo: update this when mathlib4 has a release) \ No newline at end of file +This will download mathlib4 and build the project. +To prevent building mathlib yourself, you can run the following to fetch precompiled files. +``` +lake exe cache get +```