search

leanprover-community / lean

Lean 3 Theorem Prover (community fork)
http://leanprover-community.github.io/
Apache License 2.0
434 stars 80 forks source link

libgmp should be linked statically or distributed with Lean on macOS #118

Open Kha opened 4 years ago

Kha commented 4 years ago

See https://github.com/Kha/elan/issues/20

LdBeth commented 4 years ago

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.

Kha commented 4 years ago

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.

LdBeth commented 4 years ago

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.