perf: garbage-collect dead sections

[Kha]

Benchmarks: https://github.com/leanprover/lean4/pull/1689#issuecomment-1268175703

[Kha]

Very interesting, so -dead_strip on linking lake is sufficient to break it. That sounds straightforward enough that one could isolate the failure and report it to LLVM if one was sufficiently motivated...

[Kha]

I took another look at why bin/lake is not affected: as with libleanshared, the exported symbols are holding all sections alive. If I temporarily remove -rdynamic, --gc-sections brings us from 3.2MB down to 2.2MB (or 60MB -> 46MB when linking core statically) with something like the following log:

removing unused section '.rodata.cst4' in file '/nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210/lib/crt1.o'
removing unused section '.data' in file '/nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210/lib/crt1.o'
removing unused section '.data' in file '/nix/store/jf217yacqd074ypqp2rxs66i29nxi4rn-gcc-11.3.0/lib/gcc/x86_64-unknown-linux-gnu/11.3.0/crtbegin.o'
removing unused section '.text.l_Lake_BuildData_toJob___rarg___lambda__1' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_BuildData_toJob' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_BuildData_toJob___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_mkBuildSpec___rarg' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_mkBuildSpec' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_mkConfigBuildSpec___rarg' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_mkConfigBuildSpec' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_mkConfigBuildSpec___rarg___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_BuildSpec_build___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Array_mapMUnsafe_map___at_Lake_buildSpecs___spec__1___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Array_foldlMUnsafe_fold___at_Lake_buildSpecs___spec__4___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_parsePackageSpec___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_resolveModuleTarget___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_resolveLibTarget___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_RBNode_dFind___at_Lake_resolveTargetInPackage___spec__1' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_RBNode_dFind___at_Lake_resolveTargetInPackage___spec__1___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_resolveTargetInPackage___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Lake_resolveDefaultPackageTarget' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
removing unused section '.text.l_Array_mapMUnsafe_map___at_Lake_resolveDefaultPackageTarget___spec__1___boxed' in file '/nix/store/l4j5jf9z0x29p41qijsjsza4rsynjjs0-Lake.CLI.Build-cc/Lake/CLI/Build.o'
...

So for Lean binaries not linked for interpreter use, this can still result in a good amount of binary size savings. The cost of this change is that the static archives have grown by 15MB/20MB on Linux/Windows, but compression brings that back down to 1MB/4MB.