Leanc failing to link properly

Stream: lean4

[Anders Christiansen Sørby]

For this source code

import Ipld.UnsignedVarint
import Ipld.Multihash
import Ipld.Multibase
import Ipld.Cid
import Ipld.Ipld
import Blake3 -- removing this fixes the error

def main : IO Unit := do
  println! "Hello, world!"

Leanc fails to link the symbols from libBinaryTools.a in this call

mkdir -p $out/bin
leanc /nix/store/zh2lk0sc0r8gv6bgpmlzsdp1zhh8g4fj-Ipld-lib/* /nix/store/mdrqr6204ni9gqn4438y2wv06zmvq2hm-BinaryTools-lib/*.a /nix/store/7ngnwn99zxmzzc3ga89dglgx5shmdhgb-Blake3-lib/*.a /nix/store/zj7l3salqgxlbz1fvg2gnzngxn8yra3v-Init-lib/*.a /nix/store/pqzkmj46czc9fhphbj2rsfgdcan1wb92-Lean-lib/*.a /nix/store/173d6zazfdz3bh2pd0ig0lq519ax2caa-Leanpkg-lib/*.a /nix/store/r3n8byk5k8mfj4dm6qvxp4bwnzr142yb-Neptune-lib/*.a /nix/store/ndd7wpbfczakimdlnrzzzm0wdr18smhj-Std-lib/*.a  -o $out/bin/ipld  -L/nix/store/sk2ha5f6q0djgpxgd54cq96mqphd5als-libleanblake3.so -lleanblake3 -L/nix/store/kwr3pqmqkapccggqrfb3ij19ynbsrcg4-libblake3.so -lblake3
/nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/kxwymh6h7s2625xfx99s03sq4qlwjinw-Blake3-cc/Blake3.o: in function `l_Std_Range_forIn_loop___at_Blake3_instIntoStringBlake3Hash___spec__2':
src.c:(.text+0x3f4): undefined reference to `l_Alphabet_base64'
/nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/kxwymh6h7s2625xfx99s03sq4qlwjinw-Blake3-cc/Blake3.o: in function `initialize_Blake3':
src.c:(.text+0x1525): undefined reference to `initialize_BinaryTools'
clang-13: error: linker command failed with exit code 1 (use -v to see invocation)

This however works fine when changing the lean source code to include a function call in Blake3

import Ipld.UnsignedVarint
import Ipld.Multihash
import Ipld.Multibase
import Ipld.Cid
import Ipld.Ipld
import Blake3

def main : IO Unit := do
  println! "Hello, world! {Blake3.hash "hello"}"

@Gabriel Barreto
I suspect some over eager optimization that ignores some symbols if they are not mentioned at the top level file? @Sebastian Ullrich

[Sebastian Ullrich]

Linking is not done by Lean, so this is likely not a Lean issue. The cmdline is a bit too long to verify at a glance, but I suspect wrong linker flag order, which is significant.

[Anders Christiansen Sørby]

I didn't know the liker flag order was significant. But that can't be the issue because the error does not appear in the latter case and it has the same order.

[Sebastian Ullrich]

If you have ld a.o b.a c.o, it will work iff all object files in b.a needed by c.o have been included by the linker when searching for symbols referenced by a.o. So an independent file can very much change whether a later file succeeds to link. The correct solution is to always put dependencies behind dependents in the cmdline.

[Sebastian Ullrich]

...I think. It's a bit of black magic.

[Reid Barton]

there's also --start-group/--end-group if you don't know/don't care to figure out the correct order and don't mind longer link times

[Sebastian Ullrich]

Yes, we use those for -lleancpp -lLean etc.. Which is a cyclic dependency :laughter_tears: .

[Anders Christiansen Sørby]

Adding -Wl,--start-group fixed it