trouble running lean on mac

Stream: new members

[Yuhan Du]

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

[Mario Carneiro]

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

[Kevin Buzzard]

This is the current nightly

[Kevin Buzzard]

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

[Kevin Buzzard]

(or indeed how to do anything on a mac)

[Yulia Zaplatina]

Homebrew solves the problem

[Yulia Zaplatina]

https://brew.sh

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sean Leather]

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

[Sean Leather]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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).

[Kevin Buzzard]

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

[Sean Leather]

IIRC, git comes with the Xcode command line tools.