Zulip Chat Archive

Stream: lean4

Topic: Leanc failing to link properly


Anders Christiansen Sørby (Nov 23 2021 at 16:47):

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 (Nov 23 2021 at 16:51):

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 (Nov 23 2021 at 17:23):

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 (Nov 23 2021 at 17:30):

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 (Nov 23 2021 at 17:31):

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

Reid Barton (Nov 23 2021 at 17:44):

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 (Nov 23 2021 at 17:46):

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

Anders Christiansen Sørby (Nov 23 2021 at 20:56):

Adding -Wl,--start-group fixed it


Last updated: Dec 20 2023 at 11:08 UTC