building dependency failure

Stream: lean4

[Arthur Paulino]

Hi all, I need some help with a dependency

I set https://github.com/argumentcomputer/Blake3.lean/tree/ap/use-c to use C bindings for BLAKE3. It works well locally. That is, I can create an executable that uses Blake3.hash, compile it and it runs just fine.

However, when I try to use that lib as a dependency of another Lean 4 repo, I'm getting some weird errors when I try to compile a file that does import Blake3:

trace: .> /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang -o ././.lake/build/bin/Tests-Blake3 ././.lake/build/ir/Tests/Blake3.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Control/DefaultRange.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Control/Random.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Gen.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Sampleable.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/SlimCheck/Checkable.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/LSpec.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec/Instances.c.o.export ././.lake/packages/LSpec/.lake/build/ir/LSpec.c.o.export ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export ././.lake/build/ir/Ix/ByteArray.c.o.export ././.lake/packages/Blake3/.lake/build/lib/libffi.a ././.lake/packages/Blake3/.lake/build/lib/libffi.a ././.lake/build/lib/libffi.a --sysroot /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0 -L /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/lib -L /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc/libc_nonshared.a /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread
info: stderr:
ld.lld: error: undefined symbol: lean_blake3_version
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_internalVersion___boxed)
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(initialize_Blake3)

ld.lld: error: undefined symbol: lean_blake3_initialize
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_Hasher_init___boxed)
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(initialize_Blake3)

ld.lld: error: undefined symbol: lean_blake3_hasher_update
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_Hasher_update___boxed)
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_hash)

ld.lld: error: undefined symbol: lean_blake3_hasher_finalize
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_Hasher_finalize___boxed)
>>> referenced by Blake3.c
>>>               ././.lake/packages/Blake3/.lake/build/ir/Blake3.c.o.export:(l_Blake3_hash)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang' exited with code 1

Help is much appreciated. Thanks in advance!

[Henrik Böving]

This is presumably happening because the linker flags in the project using blake as a dependency do not include the Blake library properly but my mental model of Lake is not strong enough to figure out what exactly to do here.

[Arthur Paulino]

I didn't set linker flags. Where should those be set and which flags?

[Arthur Paulino]

When I inspect the .lake folder, I see that the static lib from Blake3.lean is being generated

[Henrik Böving]

Arthur Paulino said:

I didn't set linker flags. Where should those be set and which flags?

I assume one of the lake options that ends up in this call to clang but I do not know which option in particular

[Arthur Paulino]

I've already tried several combinations of moreLinkArgs, weakLinkArgs and moreLeancArgs under lean_lib Blake3 and package Blake3. Idk what else to try

[Arthur Paulino]

I found the sneaky line:

@@ -31,7 +31,7 @@ def buildBlake3Obj (pkg : NPackage _package.name) (fileName : String) (addFlags
 target ffi.o pkg : System.FilePath := do
   let blake3Repo ← cloneBlake3.fetch >>= (·.await)
   let oFile := pkg.buildDir / "ffi.o"
-  let srcJob ← inputTextFile "ffi.c"
+  let srcJob ← inputTextFile $ pkg.dir / "ffi.c"

[Arthur Paulino]

For context: I was extra unlucky because the repo that uses Blake3.lean as a dependency also has an ffi.c, which was being pointed to by this buggy line.

Maybe this helps if others face this (somewhat unlikely) issue in the future.