Zulip Chat Archive

Stream: new members

Topic: Linking / Using mathlib and tactics


view this post on Zulip Adeeb K (Apr 21 2020 at 00:33):

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!

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:34):

import tactic

view this post on Zulip Bryan Gin-ge Chen (Apr 21 2020 at 00:35):

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.

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:35):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 00:37):

@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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:39):

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

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:39):

From the sounds of it you didn't!

view this post on Zulip Scott Morrison (Apr 21 2020 at 00:40):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 00:41):

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

view this post on Zulip Adeeb K (Apr 21 2020 at 00:48):

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!


Last updated: May 12 2021 at 04:19 UTC