importing tactic.linarith - error when algebra.group loaded

Stream: general

[Joseph Corneli]

I've tried to

import tactic.linarith

I then get multiple errors to this effect:

invalid import: algebra.group
invalid object declaration, environment already has an object named 'to_additive_attr._main'

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]

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]

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

[Patrick Massot]

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