Skip to content

Commit

Permalink
Add comment about obtaining precompiled files for Mathlib
Browse files Browse the repository at this point in the history
  • Loading branch information
Daniel Britten committed Oct 7, 2024
1 parent 704b244 commit e6bdeef
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit e6bdeef

Please sign in to comment.