Zulip Chat Archive

Stream: new members

Topic: Mathlib Import Error

Shash Comandur (Apr 23 2023 at 19:01):

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 (Apr 23 2023 at 19:06):

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 (Apr 23 2023 at 19:13):

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 (Apr 23 2023 at 20:02):

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 (Apr 23 2023 at 20:19):

leanproject does not work with Lean 4

Shash Comandur (Apr 23 2023 at 20:45):

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

Last updated: Dec 20 2023 at 11:08 UTC