Zulip Chat Archive

Stream: general

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

view this post on Zulip 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
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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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