Zulip Chat Archive

Stream: new members

Topic: Uninstall Lean


view this post on Zulip 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 ?

view this post on Zulip Johan Commelin (Sep 21 2020 at 13:45):

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

view this post on Zulip Johan Commelin (Sep 21 2020 at 13:45):

which elan

view this post on Zulip Vincent Siles (Sep 21 2020 at 13:46):

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

view this post on Zulip 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

view this post on Zulip Anne Baanen (Sep 21 2020 at 13:47):

Does elan self update work?

view this post on Zulip 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) ?

view this post on Zulip Vincent Siles (Sep 21 2020 at 13:47):

info: elan updated successfully to 0.10.2

view this post on Zulip Anne Baanen (Sep 21 2020 at 13:47):

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

view this post on Zulip Johan Commelin (Sep 21 2020 at 13:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 21 2020 at 13:50):

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

view this post on Zulip Johan Commelin (Sep 21 2020 at 13:50):

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

view this post on Zulip 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

view this post on Zulip Vincent Siles (Sep 21 2020 at 13:51):

that's a start :) thank you

view this post on Zulip 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