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
   

   OR, if that command fails, then you're on the older version of lake, and should run:

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

2. Clean cache to make sure everything goes fine

   rm -rf lake-packages
   rm -rf build // Or whatever the location of your build files is, depends on your lake version!
   

   lake exe cache clean!
   

3. Get cached built files

   lake exe cache get
   

   EXPECTED RUNTIME: for my project that includes mathlib this takes 20 seconds.

4. Finally, build

   lake build
   

   EXPECTED RUNTIME: for my project that's just a few files it takes 0 seconds. The runtime here depends on the size of your project, Mathlib shouldn't be contributing to it anymore.