Zulip Chat Archive

Stream: general

Topic: path issues?

Jakob von Raumer (Mar 12 2018 at 12:19):

I'm getting the following error whenever I run lean from the console instead of vscode:

/usr/local/lib/lean/library/init/data/default.lean:1:0: error: ambiguous import, it can be '/usr/local/lib/lean/library/init/data/ordering/default.lean' or '/usr/local/lib/lean/library/init/data/ordering.lean'

Jakob von Raumer (Mar 12 2018 at 12:19):

Any ideas?

Jakob von Raumer (Mar 12 2018 at 12:21):

Hm, okay, removing /usr/local/lib/lean and re-installing helped

Sebastian Ullrich (Mar 12 2018 at 12:24):

Yeah, this is a known general issue with make install. I don't recommend using it.

Jakob von Raumer (Mar 12 2018 at 13:53):

Because it just doesn't clear the directories?

Sebastian Ullrich (Mar 12 2018 at 13:56):

Yes

Sebastian Ullrich (Mar 12 2018 at 13:56):

And I don't recommend using it because adjusting PATH is so much easier :)

Last updated: Dec 20 2023 at 11:08 UTC