Joseph Corneli (Feb 12 2019 at 17:55):
I've tried to
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: May 08 2021 at 04:14 UTC