leanprover-community
libgmp should be linked statically or distributed with Lean on macOS
There are other possible options.
If the user has already installed libgmp, an ad hoc fix is using the install_name_tool available from macOS to patch the binary executable, and write this part into the installation script. For example what I use for patching the binary after installation is
$ install_name_tool -change /usr/local/opt/gmp/lib/libgmp.10.dylib /opt/pkg/lib/libgmp.10.dylib lean
Another solution could be passing proper -rpath flag when building Lean executable if it is on macOS so macOS users can resolve the library location via the dyld interface provided by macOS, and mention this in the installation instructions. See https://wincent.com/wiki/@executable_path,@load_path_and@rpath , and man ld on macOS.
Users having to install libgmp themselves is just the bad status quo, not a solution. Though I don't know why you have to set the rpath yourself when for the users in the linked thread that was not the case.
I think elan can be extended to have the ability fetch libgmp and by default lean should point to libgmp using a relative path. In addition to this elan can just create a symbol link if the user has already installed it.