Setting up lean on Mac

Stream: new members

[Big john]

Yo whats up gang I'm having trouble with installing lean. I used the usual code to paste in terminal, and we're stuck on this screen for ages:
Screenshot-2024-03-21-at-02.36.45.png
Do I just need to wait for longer or should I do something else?

[Johan Commelin]

Which "usual code" do you mean?

[Shanghe Chen]

emm，it seems you are running brew install elan-init . It does take some time to setup the llvm and clang stuffs in this way

[Big john]

Hi, so I actually did get further than this, but it asks me to update my OS and I don't wanna do that :( is there any other way around it?

[Yaël Dillies]

You can use gitpod.io

[Big john]

Yaël Dillies said:

You can use gitpod.io

How does this work? Sorry, completely new to this :sweat_smile:

[Yaël Dillies]

This is an online instance of vscode, so you don't need to install anything on your old and unupgradable OS

[Matthew Ballard]

Is this the “usual code”?

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

[Big john]

Matthew Ballard said:

Is this the “usual code”?

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

I'm using this: https://leanprover-community.github.io/install/macos.html

[Big john]

Yaël Dillies said:

This is an online instance of vscode, so you don't need to install anything on your old and unupgradable OS

Ooh ok does it have all the same functionality as the lean download? For example I want to start contribute to mathlib, can I do this just as easily like that? Sorry if this is an obvious question haha

[Big john]

Great, thank you all, I will try using it