Uninstall Lean

Stream: new members

[Vincent Siles]

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]

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

[Johan Commelin]

which elan

[Vincent Siles]

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

[Johan Commelin]

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]

Does elan self update work?

[Vincent Siles]

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]

info: elan updated successfully to 0.10.2

[Anne Baanen]

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

[Johan Commelin]

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

[Vincent Siles]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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]

that's a start :) thank you

[Kevin Buzzard]

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