## Stream: general

### Topic: importing tactic.linarith - error when algebra.group loaded

#### Joseph Corneli (Feb 12 2019 at 17:55):

I've tried to

import tactic.linarith


I then get multiple errors to this effect:

invalid import: algebra.group


If I copy the offending object into my buffer and follow to the source, I see it is defined in algebra.group alright. But why is my import invalid? I certainly don't have tactic.linarith imported yet. Shouldn't the new import slot in with whatever other files are already loaded?

#### Rob Lewis (Feb 12 2019 at 20:21):

You have something wrong with your setup. It sounds like whatever copy of linarith.lean you're finding is based on a different version of core. Are you doing anything funny with leanpkg.path or your olean files?

#### Patrick Massot (Feb 12 2019 at 20:22):

Yes, it sounds very much like the errors I had with my lean formatter when it was picking the wrong Lean version

#### Patrick Massot (Feb 12 2019 at 20:23):

If you can't figure it out, then you can post the output of lean -p run inside the project you're trying to compile

Last updated: May 08 2021 at 04:14 UTC