can't import tactic

Stream: mathlib4

[alex van tilburg]

I am trying to install lean so I can do the exercise sheets from ImperialCollegeLondon /M40001_lean. However for this I need to install mathlib. For this I used the pip install but yet it still doesn't recognize import tactic. I have installed elan because I have the Lean Infoview in VS code. Could someone help me? How can I check if mathlib is correctly installed outside of pip freeze.

[Henrik Böving]

Sounds to me like you're in the wrong stream to my knowledge Imperial College doesn't use mathlib4 yet, you'll most likely have more luck with this question in general.

[alex van tilburg]

Thank you for your reply. I have sent the question in general however isn't the way you have to install the same for mathlib4 as for mathlib?

[Henrik Böving]

No, mathlib4 doesn't involve any pip or python at all right now and uses tooling that doesn't even exist with Lean 3 yet, namely the new Lake build system.

[alex van tilburg]

Okay I didn't know that thank you