Lean installation issue with homebrew

Stream: new members

[Brandon Werbel]

I'm trying to install Lean on a new Macbook. I was able to install elan and mathlib tools through homebrew, but when I try to run leanproject new, I get the following error:

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/brandon/.elan/toolchains/stable/bin/lean
  Reason: image not found
Command '['leanpkg', 'init', 'lean_sandbox']' died with <Signals.SIGABRT: 6>.

I've run brew install gmp and brew link gmp, but I think the problem is that homebrew is installed locally to evade admin privileges, and therefore can't create a symlink to /usr/local/opt. In other words, the library from the error message is on my computer but in the wrong place. Any ideas what I can do?

[Mauricio Collares]

There's a workaround at https://github.com/leanprover-community/lean/issues/118#issuecomment-695750332, allowing you to use your brew-installed local copy of gmp (remember to replace /opt/pkg/lib/libgmp.10.dylib by the correct location on your computer, of course).

[Brandon Werbel]

That worked perfectly, thank you so much!