Linking / Using mathlib and tactics

Stream: new members

[Adeeb K]

Hello everybody! I am pretty new to using Lean - I just installed via the extension on VScode a few weeks ago. I was collaborating with an instructor remotely, and I downloaded a file they had been editing. It used the linarith tactic (specifically unknown identifier 'linarith' ). However, I have been getting errors from its use, and it does not seem like I can import anything to make them go away. Is there anything I can do? Thank you!

[Scott Morrison]

import tactic

[Bryan Gin-ge Chen]

Installing via the extension won't get you everything you need to use mathlib. You should follow the instructions here for your OS and then proceed to the projects doc.

[Scott Morrison]

(If that doesn't work, can you tell us which installation instructions you followed?)

[Adeeb K]

@Scott Morrison unfortunately, import tactic is giving me this error: file 'tactic' not found in the LEAN_PATH
@Bryan Gin-ge Chen I followed installation for the supporting tools for macOS, but I didn't touch anything related to elan

[Scott Morrison]

Did you follow the "You're not done yet" link at the bottom of the macOS page?

[Scott Morrison]

From the sounds of it you didn't!

[Scott Morrison]

linarith, along with almost everything else, is in mathlib, not Lean itself, and you need to install it too.

[Adeeb K]

Ah, makes sense. I'll do that now and report back!

[Adeeb K]

It works! I have a few questions about the content of the thing I'm working on, but I'll make a new topic for that. Thank you both so much for all the help!