Merge pull request #12 from NethermindEth/readme-edit

Add comment about obtaining precompiled files for Mathlib
NethermindEth · Oct 16, 2024 · 7907bc9 · 7907bc9
2 parents a8862bf + e6bdeef
commit 7907bc9
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -13,6 +13,11 @@ There are two parts.
 ## The Lean framework
 Download and install Lean 4. One can follow https://lean-lang.org/lean4/doc/quickstart.html.
 
+To obtain precompiled files for the dependency Mathlib, run the following in the root directory (this is optional, it saves time): 
+```
+lake exe cache get
+```
+
 Then simply run the following in the root directory:
 ```
 lake build