## Stream: new members

### Topic: Uninstall Lean

#### Vincent Siles (Sep 21 2020 at 13:43):

Hi ! I installed Lean some time ago (using https://leanprover-community.github.io/install/macos.html) and I have to admit I don't remember which version I installed or if was given instructions to uninstall at the time. I'd like to uninstall Lean to make sure my setup is clean before re-installing it (or a patched version of it). Is there a documentation on how to uninstall lean ?

#### Johan Commelin (Sep 21 2020 at 13:45):

@Vincent Siles Do you have elan installed on your system?

#### Johan Commelin (Sep 21 2020 at 13:45):

which elan

#### Vincent Siles (Sep 21 2020 at 13:46):

yes: /Users/vsiles/.elan/bin/elan

#### Johan Commelin (Sep 21 2020 at 13:46):

If you do, then I recommend not uninstalling, but just let elan do its thing. It can manage your custom lean installations, as well as prebuilt versions by the community

#### Anne Baanen (Sep 21 2020 at 13:47):

Does elan self update work?

#### Vincent Siles (Sep 21 2020 at 13:47):

Is there some doc on elan about custom installations ? So far I only cloned the lean3 github, and built it locally (so my binaries are in ...path/to/lean/build/releases/shell) ?

#### Vincent Siles (Sep 21 2020 at 13:47):

info: elan updated successfully to 0.10.2

#### Anne Baanen (Sep 21 2020 at 13:47):

If so, you can use elan to download the latest version of elan itself.

#### Johan Commelin (Sep 21 2020 at 13:49):

We should really add to the docs on how to use elan for custom installations.

#### Vincent Siles (Sep 21 2020 at 13:50):

I'll fix my setup (leanproject is nowhere to be found), then I'll dig in how to use a custom install

#### Johan Commelin (Sep 21 2020 at 13:50):

elan toolchain link local <path/to/lean/> should do the job, I think.

#### Johan Commelin (Sep 21 2020 at 13:50):

But I'm not a "run local lean" expert

#### Reid Barton (Sep 21 2020 at 13:51):

Yes, and then you can run elan override set local in the directory where you want to set the lean version, without having to edit the leanpkg file

#### Vincent Siles (Sep 21 2020 at 13:51):

that's a start :) thank you

#### Kevin Buzzard (Sep 21 2020 at 16:34):

If you have elan then getting leanproject might be as simple as somethlng like pip install mathlibtools except possibly with a hyphen

Last updated: May 08 2021 at 17:33 UTC