Installing lean on MacOS

Stream: new members

[Dan Roffey]

Hi, I'm new here and am struggling to set up a lean environment. I have tried following the instructions on https://leanprover-community.github.io/install/macos.html, but I keep encountering errors. In particular I get the following:

info: downloading component 'lean'
error: binary package was not provided for 'darwin'

[Kevin Buzzard]

Does elan self update fix the problem? (sorry, I originally wrote update self which doesn't work)

[Dan Roffey]

No, it does not, and I have tried uninstalling and reinstalling elan through brew

[Kevin Buzzard]

What does elan --version report? Are you on an M1/M2 Mac or one of the older ones? What does elan self update do?

[Dan Roffey]

ah wait, I didn't see the edit. I have just performed the edited version and it gets the error 'failed to parse latest release tag'

[Dan Roffey]

Kevin Buzzard said:

What does elan --version report? Are you on an M1/M2 Mac or one of the older ones? What does elan self update do?

elan 0.10.3 (4687a92d0 2021-01-15)

[Kevin Buzzard]

Well that's your problem

[Kevin Buzzard]

or at least, that's one of your problems; you're many years out of date.

[Kevin Buzzard]

Can you answer the M1/M2 question?

[Kevin Buzzard]

What does which elan give you?

[Dan Roffey]

I do not know what this means or how to check.

[Kevin Buzzard]

You can google for how to find this out. The installation procedure depends very strongly on what the answer is.

[Dan Roffey]

/Users/danielroffey/.elan/bin/elan

[Kevin Buzzard]

(I'm not being obscure BTW, I have no idea how macs work; I'm sure it's easy to find out but I don't know how)

[Kevin Buzzard]

(maybe just click on an apple symbol somewhere on the top line and then click on "about" or something? I'm sure google will do a better job than me telling you how to do this)

[Dan Roffey]

Ok, I am on an intel mac, not an M1 or M2 mac

[Kevin Buzzard]

So I would recommend uninstalling elan via brew, and then checking that which elan now says "you don't have any elan". Can you get this far?

[Dan Roffey]

hm... when I do brew uninstall elan I get Error: Cask 'elan' is not installed. and when I do which elan, it says /Users/danielroffey/.elan/bin/elan

[Kevin Buzzard]

OK then I would recommend typing rm -rf /Users/danielroffey/.elan -- that's another way of uninstalling it :-)

[Dan Roffey]

ok, now got to elan not found

[Kevin Buzzard]

And after you've done this, hopefully typing

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

will install Lean 3 for you.

[Kevin Buzzard]

(this is just the thing it says here )

[Dan Roffey]

well, it is not getting to an error as quickly, so hopefully it will finish this time

[Kevin Buzzard]

oh nice. The way to check that it's worked is that when it's all finished, hopefully there aren't any errors, and you should be able to type something like leanproject get mathlib and then you'll have a fresh copy of the maths library (after the system spends quite some time downloading it). You do _want_ the maths library, of course? :-)

[Dan Roffey]

dammit, my early attempts on VScode seem to have broken something:
Error: It seems there is already an App at '/Applications/Visual Studio Code.app'.

[Dan Roffey]

or is that just that visual studio code is already installed?

[Kevin Buzzard]

Yes, hopefully that's nothing to worry about.

[Dan Roffey]

ah, ok, I think it's working now (installed the mathlib and now it's working on vscode)

[Dan Roffey]

thanks

[Julian Berman]

FWIW the package name on macOS is elan-init not elan, which you likely still have "installed" as far as homebrew is concerned.

[Julian Berman]

(Though hopefully IIRC the install_macos.sh script is fine with that and just went on using it, so you shouldn't have anything else left to do)