Installation instructions for macOS High Sierra

Stream: general

[Marc Masdeu]

Hi all,
We are installing Lean and all the related tools on a bunch of students' computers by following the instructions in the community site. Most of the computers did fine, but there is one who has MacOS High Sierra and we didn't manage to make it work. I have no idea on how to use a Mac (I use linux myself) and I have no other similar Mac to test anything, so I'd be very grateful if someone can give me a concrete list of commands that I can run to get Lean working there...
Thank you!

[Floris van Doorn]

I'm also not used to MacOS, but for people that are, it is probably useful if you tell what you tried and why it didn't work (what error you got).
The one-step solution on https://leanprover-community.github.io/install/macos.html doesn't work?

[Marc Masdeu]

I know, but I don't have the computer with me right now so I can't tell, and when I have the computer the time is limited... The one-step solution is for newer MacOS's as far as I understand (it gave an error saying that the version was too old). We will try the longer step-by-step approach and report what errors we get.

[Julian Berman]

High Sierra is end-of-lifed so not supported neither by Homebrew nor by Apple. I'd expect you could get such a system working if really necessary. (Of course there's decent risk though in running an EOL'ed system, so if the hardware supports it, an upgrade is the best idea, but that's besides the point, especially if it doesn't). Probably doing so will mean quite a different install mechanism though, I suspect given Homebrew probably won't run at this point that you'll have to install fully manually.

[Julian Berman]

Post the error messages certainly, or where they get stuck, and we can try to help.

[Julian Berman]

In particular, don't follow this page even: https://leanprover-community.github.io/install/macos_details.html

[Julian Berman]

I'd go straight to the elan README https://github.com/leanprover/elan#manual-installation and follow that for fully manual installation.

[Alistair Tucker]

You can use MacPorts instead of Homebrew on an older Mac. It does much the same.

[Marc Masdeu]

Thanks for the help! We tried a couple of things but we didn't succeed. I'm quite sure it's possible to get it working, but it's hard with the current setup, where I would dictate commands and the student would be typing them, while none of us knew enough of how a Mac works...

[Julian Berman]

Perhaps having the student use Gitpod is a decent third option? I think @Eric Wieser speaks pretty highly of it. I take it your course has some custom Lean files that may need setting up in it but I think that can be done without the student needing to do anything IIRC.

[Eric Wieser]

The only hazard with gitpod is having students (or you) using up the 50 hours/mo included in the free tier

[Eric Wieser]

(which isn't a problem for me because they grant unlimited hours for open source software maintainers)