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