Zulip Chat Archive

Stream: new members

Topic: trouble running lean on mac


view this post on Zulip Yuhan Du (Aug 13 2018 at 11:00):

dyn3218-19:bin apple$ ls
lean        leanchecker leanpkg
dyn3218-19:bin apple$ ./lean
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/apple/Desktop/lean-3.4.2-nightly-2018-06-21-darwin/bin/./lean
  Reason: image not found
Abort trap: 6

can someone help with this

view this post on Zulip Mario Carneiro (Aug 13 2018 at 11:01):

I think if you are compiling it yourself there is some line to install libgmp in the readme?

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:01):

This is the current nightly

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:02):

I just don't know how to install gmp on a mac

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:02):

(or indeed how to do anything on a mac)

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 11:02):

Homebrew solves the problem

view this post on Zulip Yulia Zaplatina (Aug 13 2018 at 11:02):

https://brew.sh

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:02):

I think Homebrew solved a problem like this before. I should write this in the docs

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:06):

Can one install Lean through homebrew? I'm guessing no

view this post on Zulip Sean Leather (Aug 13 2018 at 11:09):

I used to do it with Lean 2. I don't know if it's been kept up to date, though.

view this post on Zulip Sean Leather (Aug 13 2018 at 11:22):

I just read the rest of the thread before Kevin's message. I believe Yulia is referring to installing libgmp via brew install gmp, which will probably fix Yuhan's problem.

view this post on Zulip Patrick Massot (Aug 13 2018 at 11:31):

Since Lean is currently frozen, it seems like a very good time to update that brew thing

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:32):

FWIW we have everything up and running now. On MacOS High Sierra we installed brew, and then brew install gmp (to get lean running) and brew install coreutils (to get leanpkg running).

view this post on Zulip Kevin Buzzard (Aug 13 2018 at 11:32):

Yuhan also installed git somehow, or had git already, but that was before I arrived.

view this post on Zulip Sean Leather (Aug 13 2018 at 11:43):

IIRC, git comes with the Xcode command line tools.


Last updated: May 15 2021 at 00:39 UTC