Zulip Chat Archive

Stream: general

Topic: Installation instructions for macOS High Sierra


Marc Masdeu (Jul 06 2022 at 09:35):

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 (Jul 06 2022 at 10:14):

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 (Jul 06 2022 at 10:38):

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 (Jul 06 2022 at 10:43):

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 (Jul 06 2022 at 10:43):

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

Julian Berman (Jul 06 2022 at 10:45):

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

Julian Berman (Jul 06 2022 at 10:46):

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

Alistair Tucker (Jul 06 2022 at 20:39):

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

Marc Masdeu (Jul 09 2022 at 16:25):

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 (Jul 09 2022 at 17:17):

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 (Jul 09 2022 at 17:18):

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

Eric Wieser (Jul 09 2022 at 17:19):

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


Last updated: Dec 20 2023 at 11:08 UTC