Zulip Chat Archive

Stream: new members

Topic: is there a way to not error on mathlib `cache get` fail?


Alok Singh (Jul 11 2025 at 17:44):

Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:nightly
  Mathlib uses leanprover/lean4:v4.22.0-rc3

The cache will not work unless your project's toolchain matches Mathlib's toolchain
This can be achieved by copying the contents of the file `.lake/packages/mathlib/lean-toolchain`
into the `lean-toolchain` file at the root directory of your project
You can use `cp .lake/packages/mathlib/lean-toolchain ./lean-toolchain`
error: mathlib: failed to fetch cache

This is fine by me, but I don't want it to error. Is there a way to make it a warning and continue with local clone/build?

Aaron Liu (Jul 11 2025 at 17:46):

I don't think that's how it works


Last updated: Dec 20 2025 at 21:32 UTC