Zulip Chat Archive

Stream: lean4

Topic: Weird error when getting cache.


Wrenna Robson (Aug 26 2025 at 07:55):

When running lean exe cache get on a fresh clone of my repo synced to the main repo, I get a bunch of errors (the last of which I have copied here but there are more like this).

 [18/19] Building Cache.Requests:c.o
trace: .> /home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/clang -c -o /home/wrobson/repos/mathlib4/.lake/build/ir/Cache/Requests.c.o.export /home/wrobson/repos/mathlib4/.lake/build/ir/Cache/Requests.c -I /home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2 -nostdinc -isystem /home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
/home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/clang: symbol lookup error: /home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/clang: undefined symbol: _ZN4llvm3sys2fs17getMainExecutableEPKcPv, version LLVM_19.1
error: external command '/home/wrobson/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/clang' exited with code 127
Some required targets logged failures:
- Cache.Main:c.o
- Batteries.Data.Array.Match:c.o
- Batteries.Data.String.Basic:c.o
- Batteries.Data.String.Matcher:c.o
- Cache.Lean:c.o
- Cache.IO:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o

This has worked fine previously. I'm trying to work out if I've changed something in my system but other than installing some objective C runtimes, I don't think I have. Any idea what could be up?

Wrenna Robson (Aug 26 2025 at 08:00):

OK, no, I think it might have been a GNUStep thing because after removing a line from my .profile and restarting it appears to have fixed itself.


Last updated: Dec 20 2025 at 21:32 UTC