From e6bdeefea54708b3fadb95d7834314ecbd1d4722 Mon Sep 17 00:00:00 2001
From: Daniel Britten <daniel.britten@nethermind.io>
Date: Mon, 7 Oct 2024 17:24:33 +1300
Subject: [PATCH] Add comment about obtaining precompiled files for Mathlib

---
 README.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/README.md b/README.md
index 121178b..cba314e 100644
--- 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