Zulip Chat Archive

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
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 (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: Aug 03 2023 at 10:10 UTC