leanprover
OSX binary depends on libgmp, missing by default
Prerequisites
- [ X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
The current lean binary for OSX depends on libgmp being installed, but this library isn't installed by default on OSX. For newbies (like my fresh undergraduate students) it's confusing and frustrating that the distribution doesn't work out of the box. The steps we've been taking to remedy the problem are (1) install XCode, which itself is problematical depending on the current version of OSX one is running; (2) install brew; (3) brew install gmp. Perhaps at a minimum the need to take such steps could be documented so that if users follow the installation instructions (beyond just downloading the darwin executable) it will just work. Thanks all. Very exciting work you're doing.
Steps to Reproduce
- download executable on vanilla OSX machine
- run executable
- boom
Expected behavior: [What you expect to happen]
Should run without error
Actual behavior: [What actually happens]
Fails on missing libgmp.10.dylib
Reproduces how often: [What percentage of the time does it reproduce?]
100%
Versions
Various version of OSX, current version of lean
You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.
Additional Information
Nope.
I've seen other projects statically link libgmp in the binary. (GHC comes to mind.)
An alternative that I would favor is making Homebrew the standard way of distributing Lean on macOS. Unfortunately, the Homebrew Lean tap has not been given attention in over a year. I briefly looked at it to see if I could update it, but it appears to need a Bintray user ID and password.
I would be willing to bring the Homebrew Lean tap up to date and help maintain it with some initial guidance on how to run the scripts.
I just discovered that the Homebrew Lean formula is up to date with 3.4.1. So, it may be that brew install lean is all you need, since it has gmp as a dependency. Note that Homebrew provides binaries, so you don't even need to build lean.
Ok this is good. The lean download and installation page should probably be updated at least to notify people of this fact. Thanks!
On Tue, Sep 4, 2018, 2:20 PM Sean Leather [email protected] wrote:
I just discovered that the Homebrew Lean formula https://formulae.brew.sh/formula/lean is up to date with 3.4.1. So, it may be that brew install lean is all you need, since it has gmp as a dependency. Note that Homebrew provides binaries, so you don't even need to build lean.
— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/leanprover/lean/issues/1971#issuecomment-418468517, or mute the thread https://github.com/notifications/unsubscribe-auth/ACpL9Yp_zqEGISpk59eOkUIidNUSNOuLks5uXsRmgaJpZM4WT1Lf .