leanc doesn't find bundled libgmp

[gebner]

leanc complains about the missing libgmp (even though it is bundled). For example, this happens when building lake:

 leanc -o "build/bin/lake" build/temp/Lake/Attributes.o build/temp/Lake/Cli.o build
/temp/Lake/Help.o build/temp/Lake/LeanVersion.o build/temp/Lake/CliT.o build/temp/Lake/Compile.o build/temp/La
ke/Resolve.o build/temp/Lake/Task.o build/temp/Lake/BuildTop.o build/temp/Lake/Git.o build/temp/Lake/BuildMona
d.o build/temp/Lake/Main.o build/temp/Lake/LeanConfig.o build/temp/Lake/Target.o build/temp/Lake/Package.o bui
ld/temp/Lake/SearchPath.o build/temp/Lake/InstallPath.o build/temp/Lake/BuildBin.o build/temp/Lake/BuildPackag
e.o build/temp/Lake/BuildTarget.o build/temp/Lake/Async.o build/temp/Lake/Glob.o build/temp/Lake/DSL.o build/t
emp/Lake/Init.o build/temp/Lake/Version.o build/temp/Lake/Trace.o build/temp/Lake/BuildTargets.o build/temp/La
ke/BuildModule.o build/temp/Lake.o -rdynamic
/nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: cannot find -lgmp
collect2: error: ld returned 1 exit status

(This is on NixOS, but I suspect you get the same error on other distributions if you don't have gmp installed.)

The reason is that while libgmp is bundled, the libgmp.so symlink is missing. If you create the symlink, then leanc works again:

$ cd .elan/toolchains/leanprover--lean4---nightly-2021-10-07/lib/
$ ln -s libgmp.so.10 libgmp.so

If you have gmp installed, then presumably leanc links against two different GMPs (the bundled one and the system installation). Not sure which one is actually used then, or if this could cause any issues.

Versions

Nightly from October 7.

[Kha]

I hate bundling 😀

[Kha]

Resolved with #795

[chadbrewbaker]

I didn't work for me - I though I built from source. Had to do this:

sudo cp /opt/homebrew/Cellar/gmp/6.2.1_1/lib/libgmp.10.dylib /usr/local/lib/libgmp.dylib