lake exe cache get error on NixOS

Stream: mathlib4

[Mauricio Collares]

I am getting errors running lake exe cache get on NixOS:

✖ [3/10] Building Cache.IO:c.o
trace: .> /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang -c -o ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/IO.c -I /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument -nostdinc -isystem /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXStack dump:
0.  Program arguments: /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang -c -o ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/IO.c -I /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument -nostdinc -isystem /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
Stack dump without symbol names (ensure you have llvm-symbolizer in your PATH or set the environment var `LLVM_SYMBOLIZER_PATH` to point to it):
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamEi+0x23) [0x7f6ce60e4953]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so(_ZN4llvm3sys17RunSignalHandlersEv+0xee) [0x7f6ce60e292e]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so(+0x16e4dff) [0x7f6ce60e4dff]
/nix/store/65h17wjrrlsj2rj540igylrx7fqcd6vq-glibc-2.40-36/lib/libc.so.6(+0x40a70) [0x7f6ce4640a70]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so(_ZN4llvm3sys4path16reverse_iteratorppEv+0x155) [0x7f6ce60d5fb5]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so(_ZN4llvm3sys4path8filenameENS_9StringRefENS1_5StyleE+0x29) [0x7f6ce60d86c9]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang(_Z10clang_mainiPPc+0x22bb) [0x56204a27760b]
/nix/store/65h17wjrrlsj2rj540igylrx7fqcd6vq-glibc-2.40-36/lib/libc.so.6(+0x2a1fc) [0x7f6ce462a1fc]
/nix/store/65h17wjrrlsj2rj540igylrx7fqcd6vq-glibc-2.40-36/lib/libc.so.6(__libc_start_main+0x89) [0x7f6ce462a2b9]
/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang(_start+0x2a) [0x56204a27502a]
error: external command '/home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang' exited with code 139

Just executing ~/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/clang dies with the same error. gdb isn't super helpful:

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff20d5fb5 in llvm::sys::path::reverse_iterator::operator++() () from /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so
(gdb) bt
#0  0x00007ffff20d5fb5 in llvm::sys::path::reverse_iterator::operator++() () from /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so
#1  0x00007ffff20d86c9 in llvm::sys::path::filename(llvm::StringRef, llvm::sys::path::Style) () from /home/collares/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/../lib/libLLVM-15.so
#2  0x000055555556260b in clang_main(int, char**) ()
#3  0x00007ffff062a1fc in __libc_start_call_main (main=main@entry=0x55555556f7d0 <main>, argc=argc@entry=1, argv=argv@entry=0x7fffffffc288) at ../sysdeps/nptl/libc_start_call_main.h:58
#4  0x00007ffff062a2b9 in __libc_start_main_impl (main=0x55555556f7d0 <main>, argc=1, argv=0x7fffffffc288, init=<optimized out>, fini=<optimized out>, rtld_fini=<optimized out>, stack_end=0x7fffffffc278) at ../csu/libc-start.c:360
#5  0x000055555556002a in _start ()

[Mauricio Collares]

Ah, fun, the bundled clang also crashes like that in old versions (tried v4.0.0, v4.8.0, and v4.15.0), but lake exe cache get works in v4.15.0 and below because pre lean4#6176 it used leanc instead of clang, which just defers compilation to the system compiler (gcc in my case)

(these are all freshly installed toolchains, it's not a garbage collection problem)

[Mauricio Collares]

There are two problems here:

1) The bundled compiler shouldn't be used on NixOS. As the leanc wrapper on NixOS says, compilation of C files by Lean should "use bundled libraries, but not bundled compiler that doesn't know about NIX_LDFLAGS". To put it more succinctly, the Nixpkgs patch probably needs a new approach after lean4#6176.
2) The bundled compiler shouldn't be crashing on startup. This is less relevant for NixOS users (see point 1), but it might be causing problems on other platforms as well (unless, of course, it only crashes on NixOS due to some patchelf/glibc-related reason).

[Notification Bot]

3 messages were moved here from #mathlib4 > lake exe cache get error by Mauricio Collares.

[Joachim Breitner]

Can you try https://github.com/NixOS/nixpkgs/pull/362062?

[Mauricio Collares]

It works, thanks! Given the myriad of Windows problems, I'd bet lean4#6176 will be reverted soon. But this is probably still worth merging, right?

[Joachim Breitner]

Thanks for merging! I’m in the process of fixing live and loogle.lean-lang.org using that.

[Joachim Breitner]

Although it seems that on mathlib master, the cache isn’t used. It downloaded lots of file, but lake build still rebuilds mathlib. Mathlib stable worked fine, even with the patched elan, so maybe not an elan-related issue.

Ah, probably just what others are experiencing in #general > Updating to 4.15.0

[Alex Keizer]

For others experiencing the same issue: the fix mentioned above got merged and has been backported to NixOS 24.11, so as long as you're running that version you just need to update to get the fix. However you also have to delete and redownload any version of the Lean toolchain that fail to run lake exe cache get before it finally works again