linker errors

Stream: lean4

[James Gallicchio]

Hey, just putting these here to document my linker debugging saga :)

[jgallicc@bridges2-login014 lean]$ lake build
info: found libstdc++.so: at /usr/lib64/libstdc++.so.6
Linking Std.Classes.BEq
Linking Std.Tactic.OpenPrivate
Linking Std.Classes.Collections.Fold
Linking Std.Lean.Tactic
Linking Std.Lean.Meta
Linking Std.Tactic.ByCases
Linking Std.Classes.Dvd
Linking Std.Lean.NameMapAttribute
Linking Std.Tactic.GuardExpr
Linking Std.Util.TermUnsafe
Linking Std.Data.List.Init.Lemmas
Linking Std.Lean.Parser
Linking Std.Data.Option.Init.Lemmas
Linking Std.Data.Fin.Lemmas
Linking Std.Data.DList
Linking Std.Lean.Command
Linking Std.Util.LibraryNote
Linking Std.Tactic.TryThis
Linking Std.Tactic.HaveI
Linking Std.Tactic.CoeExt
Linking Std.Util.ExtendedBinder
Linking Std.Tactic.RCases
error: > /jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/bin/leanc -shared -o ./lean_packages/std/build/lib/libStd-Tactic-TryThis.so ./lean_packages/std/build/ir/Std/Tactic/TryThis.o -L./lean_packages/std/build/lib
error: > /jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/bin/leanc -shared -o ./lean_packages/std/build/lib/libStd-Data-Option-Init-Lemmas.so ./lean_packages/std/build/ir/Std/Data/Option/Init/Lemmas.o -L./lean_packages/std/build/lib
error: > /jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/bin/leanc -shared -o ./lean_packages/std/build/lib/libStd-Util-LibraryNote.so ./lean_packages/std/build/ir/Std/Util/LibraryNote.o -L./lean_packages/std/build/lib
error: > /jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/bin/leanc -shared -o ./lean_packages/std/build/lib/libStd-Classes-BEq.so ./lean_packages/std/build/ir/Std/Classes/BEq.o -L./lean_packages/std/build/lib
error: > /jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/bin/leanc -shared -o ./lean_packages/std/build/lib/libStd-Tactic-HaveI.so ./lean_packages/std/build/ir/Std/Tactic/HaveI.o -L./lean_packages/std/build/lib
error: stderr:
libc++abi: terminating due to uncaught exception of type std::__1::system_error: thread constructor failed: Resource temporarily unavailable
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace.
 #0 0x00007efe44e05953 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libLLVM-15.so+0x16e4953)
 #1 0x00007efe44e0392e llvm::sys::RunSignalHandlers() (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libLLVM-15.so+0x16e292e)
 #2 0x00007efe44e05dff (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libLLVM-15.so+0x16e4dff)
 #3 0x00007efe47244dd0 __restore_rt (/lib64/libpthread.so.0+0x12dd0)
 #4 0x00007efe42dfc70f raise (/lib64/libc.so.6+0x3770f)
 #5 0x00007efe42de6b25 abort (/lib64/libc.so.6+0x21b25)
 #6 0x00007efe47534b16 (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++abi.so.1+0x38b16)
 #7 0x00007efe4751823b demangling_terminate_handler() (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++abi.so.1+0x1c23b)
 #8 0x00007efe47533dd3 std::__terminate(void (*)()) (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++abi.so.1+0x37dd3)
 #9 0x00007efe47536a46 (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++abi.so.1+0x3aa46)
#10 0x00007efe475369df (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++abi.so.1+0x3a9df)
#11 0x00007efe475d743b std::__1::__throw_system_error(int, char const*) (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libc++.so.1+0x9843b)
#12 0x00007efe44d7da33 (/jet/home/jgallicc/.elan/toolchains/leanprover--lean4---nightly-2022-10-27/lib/libLLVM-15.so+0x165ca33)
#13 0x00007efe4723a2de start_thread (/lib64/libpthread.so.0+0x82de)
#14 0x00007efe42ec0e83 clone (/lib64/libc.so.6+0xfbe83)
clang: error: unable to execute command: Aborted (core dumped)
clang: error: linker command failed due to signal (use -v to see invocation)
error: stderr:
... (hundred lines of the same error repeated)

[James Gallicchio]

It seems like this might actually be a bug in clang (?)

[James Gallicchio]

Oh, hm, it didnt occur once i turned off precompileModule

[Gabriel Ebner]

My impression is that you're running this on a very restricted user account on some shared university machine. There's probably a limit on the number of processes you can create, and the linker runs into that limit.