Mathlib Import Error

Stream: new members

[Shash Comandur]

Hi there! Hope this is the right place for a question like this. When I put import Mathlib.Data.String.Basic at the top of my file, I get a very long and complicated error in the infoview that says that it exited with code 1. Does anyone know where to start fixing an error like this? I can provide more information as needed. Thanks in advance.

[Mauricio Collares]

It looks like a toolchain mismatch. Did you update the mathlib version on your project? If so, you should ensure your lean-toolchain file matches mathlib's.

[Shash Comandur]

I just ran leanproject upgrade-mathlib to update Mathlib. My lean-toolchain file reads leanprover/lean4:nightly-2023-04-11. Where can I check if it matches Mathlib?

[Mauricio Collares]

You can look inside the lake-packages directory, which should contain your copy of mathlib (including mathlib's lean-toolchain file). I guess you upgraded to a version which uses the 2023-04-20 nightly.

[Eric Wieser]

leanproject does not work with Lean 4

[Shash Comandur]

Updating the Mathlib toolchain worked! Thank you so much @Mauricio Collares !