Set up

Stream: lean4

[Dan Velleman]

I have been using Lean 3. I am trying to set up Lean 4 on a Mac, following the instructions here:
https://leanprover.github.io/lean4/doc/setup.html
It doesn't seem to be working. My guess is that my version of elan is too old. (I think I have version 1.1.0.) When I try elan self update I get the message self update is disabled for this build of elan. So then I tried to install a new version of elan by following the instructions here:
https://github.com/leanprover/elan
The curl command doesn't work--I get the message

info: downloading installer
error: it looks like you have an existing installation of Lean at:
error: /usr/local/bin
error: elan cannot be installed alongside Lean. Please uninstall first
error: if this is what you want, restart the installation with `-y'
error: cannot install while Lean is installed

So now I need to uninstall, but I don't know how to do that. Any suggestions?

[Dan Velleman]

I would be glad to add -y to the installation command, if I knew where to add it. Does it go after sh at the end?

[Alex J. Best]

Ddi you install lean/elan using your system package manager perhaps? Can you try and uninstall with your system packager manager and see what happens

[Sebastian Ullrich]

If you installed elan via Homebrew (likely given the update error), you just have to update it. Homebrew has the latest version.

[Dan Velleman]

I don't remember how I installed it. Perhaps homebrew?
Part of the problems with all of the installation instructions is that they assume you know unix. I know a little about unix, but not much. In particular, I don't know how to use a package manager. I don't know how to use homebrew.

[Sebastian Ullrich]

I'm not a regular macOS user, but I think re-running brew install elan-init should do it.

[Dan Velleman]

OK, I'll try that. Thanks.

[Dan Velleman]

Nope, that didn't work. I got the message "Error: homebrew-core is a shallow clone. To brew update, first run" and that's followed by a long git command. I could do that, but I wonder if I'd be better off uninstalling everything and starting from scratch.

[Sebastian Ullrich]

Yikes. If you're planning to use Homebrew in the future, you should probably follow the instructions or uninstall & reinstall Homebrew. Otherwise, I'd hope that at least brew remove elan-init would work. If it does, you should be able to follow our official instructions again.

[Sebastian Ullrich]

New users really shouldn't need to know Unix to follow the quickstart. Your case is just a bit more special since you had a conflicting prior setup.

[Dan Velleman]

So I wonder if I'm best off completely removing my prior setup, so that I can follow the quickstart. Will brew remove elan-init remove everything, or just elan? If the elan installer is complaining that elan can't be installed alongside an existing Lean installation, do I need to uninstall more than just elan?

[Sebastian Ullrich]

That command should remove only elan and elan's lean binary the installer was complaining about. After that, you should be able to follow the quickstart.

[Dan Velleman]

OK, I think that worked!
One more question: The instructions say that I can use the command elan override set leanprover/lean4:stable to activate Lean 4 in the current directory only. I'm not sure I know exactly what that means. If I create a folder called "Lean 4" on my mac, navigate to that folder, and give the elan override command, does that mean that any Lean project I create inside that folder will use Lean 4? Or do I create a folder for a particular project and run the command in that folder to have that project use Lean 4? What's the best way to be able to use Lean 3 for some projects and Lean 4 for others?

[Sebastian Ullrich]

You don't have to worry about that. For Lean 3 projects created with leanpkg and Lean 4 projects created with lake, your editor will automatically choose the correct version.

[Dan Velleman]

Still not working. Here are my latest error messages:

djvelleman@Dans-MBP Lean_4 % elan default leanprover/lean4:stable
info: using existing install for 'leanprover/lean4:stable'
info: default toolchain set to 'leanprover/lean4:stable'

  leanprover/lean4:stable unchanged - (lean does not exist)

djvelleman@Dans-MBP Lean_4 % lake help
error: toolchain 'leanprover/lean4:stable' does not have the binary `/Users/djvelleman/.elan/toolchains/leanprover--lean4---stable/bin/lake`

The "lean does not exist" message doesn't sound encouraging. And it looks like "lake" has not been installed.

[Dan Velleman]

Perhaps I need to uninstall the leanprover/lean4:stable toolchain? I think I saw a command somewhere for doing that but now I can't find it.

[Sebastian Ullrich]

It's elan toolchain uninstall leanprover/lean4:stable

[Dan Velleman]

I think that did it. After the uninstall, I did elan show, expecting just to see that the leanprover/lean4:stable toolchain had been removed, and instead I got messages saying that lean was being downloaded. Now I seem to have lake.
Thanks very much for all your help.

[Chris Lovett]

See also the VS Code based https://leanprover.github.io/lean4/doc/quickstart.html which might be easier to recommend in the future.

[Alexandre Rademaker]

I am getting

error: toolchain 'leanprover/lean4:nightly' does not have the binary `/Users/ar/.elan/toolchains/leanprover--lean4---nightly/bin/lean`

In the VS Code. I followed the steps of the Video, removed the elan first, reinstalled it with brew.

[Sebastian Ullrich]

If something went wrong during the toolchain download, you can try uninstalling it as above