How to uninstall Lean to reinstall?

Stream: new members

[mars0i]

On one of my computers, but not the other, after working for a bit, Lean gets stuck, either reporting errors that are no longer errors, or staying the "Processing file ..." state for a long time (even though I'm importing no libraries). Restarting the editor (nvim) clears up the problem, but after a while, it happens again. I've got the repo on github, and I comit and pull between the two computers in a normal manner

I've tried removing libraries from lakefile.lean, reinitializing Lean in any way I could imagine, but the problem persists. If anyone has experienced something similar, I'm open to suggestions.

However, since it happens on one computer but not the other, and I have no reason to think it's due to them having different MacOS versions, it seems like the next thing to try is to completely remove all traces of Lean from the machine that's giving me trouble, and then start over.

What do I need to do to do that: completely remove all traces of Lean?

[Julian Berman]

Checking to see whether you're on the same version of lean.nvim seems like another thing to do.

[mars0i]

Good point @Julian Berman. I'm pretty sure they're both up to date, and I think the nvim versions are also the same, but I'll check when I get to the other computer.

[Kevin Buzzard]

It's not clear to me that removing all traces of Lean will work, but on linux all your lean toolchains are in a directory called .elan in your home directory and nuking that (plus probably tidying up your $PATH) will remove Lean.

[Kevin Buzzard]

You would be better off figuring out which version of Lean you're using when the problems occur, and just nuking that version using elan

[mars0i]

Thanks @Kevin Buzzard. I'll explore these options. MacOS seems to be set up the same way.