Mathlib keeps rebuilding even after I `lake exe cache get`

Question

Despite the fact that I executed lake exe cache get, lake build keeps on building Mathlib, which takes hours.

Answer 1

This happens because lake build will keep building mathlib if your mathlib dependency uses a lean version different from yours.

So, to build everything using cache:

1. Copy your mathlib's Lean version into your project's lean-toolchain

   cp lake-packages/mathlib/lean-toolchain lean-toolchain
   

2. Clean cache to make sure everything goes fine

   rm -rf lake-packages
   rm -rf build
   lake exe cache clean!
   

3. Get cached built files

   lake exe cache get
   

4. Finally, build

   lake build