lake exe cache get error

Stream: mathlib4

[María Inés de Frutos Fernández]

I am getting the error below when running lake exe cache get on a mathlib branch. I tried running lake clean first, but it did not solve the issue.

lake exe cache get
✖ [10/10] Building cache
trace: .> /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export
info: stderr:
ld.lld: error: undefined symbol: __dladdr
>>> referenced by dladdr.o:(dladdr) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: __dlsym
>>> referenced by dlsym.o:(dlsym) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: _dl_deallocate_tls
>>> referenced by allocatestack.c:277
>>>               pthread_create.o:(free_stacks) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__deallocate_stack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__free_tcb) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 1 more times

ld.lld: error: undefined symbol: _dl_make_stack_executable
>>> referenced by allocatestack.c:814
>>>               pthread_create.o:(__make_stacks_executable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_stack_flags
>>> referenced by allocatestack.c:525
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:647
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls_init
>>> referenced by allocatestack.c:247
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls
>>> referenced by allocatestack.c:502
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:622
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __tunable_get_val
>>> referenced by elision-conf.c:110 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:110)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:112 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:112)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:114 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:114)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 3 more times

ld.lld: error: undefined symbol: _dl_x86_cpu_features
>>> referenced by elision-conf.c:66 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:66)
>>>               elision-lock.o:(_dl_tunable_set_elision_enable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __libc_stack_end
>>> referenced by nptl-init.c:272
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:98
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:125
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_get_tls_static_info
>>> referenced by nptl-init.c:311
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_pagesize
>>> referenced by nptl-init.c:335
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:344
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:393
>>>               nptl-init.o:(__pthread_get_minstack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 2 more times

ld.lld: error: undefined symbol: _dl_init_static_tls
>>> referenced by nptl-init.c:360
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_wait_lookup_done
>>> referenced by nptl-init.c:362
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __dlopen
>>> referenced by dlopen.o:(dlopen) in archive /lib/x86_64-linux-gnu/libdl.a

[Sebastian Ullrich]

That's a puzzling (and novel) error. Could you check it (still) works with older mathlib commits? What does

/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export -v

print?

[María Inés de Frutos Fernández]

/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/clang -I /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -nostdinc -isystem /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/include/clang -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export -v -L /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib -L /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc/libc_nonshared.a /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lpthread -ldl -lrt -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/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 -Wno-unused-command-line-argument
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-unknown-linux-gnu
Thread model: posix
InstalledDir: /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/9
Selected GCC installation: /usr/lib/gcc/x86_64-linux-gnu/9
Candidate multilib: .;@m64
Selected multilib: .;@m64
 "/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/ld.lld" -pie -z relro --hash-style=gnu --eh-frame-hdr -m elf_x86_64 -dynamic-linker /lib64/ld-linux-x86-64.so.2 -o ././.lake/build/bin/cache /lib/x86_64-linux-gnu/Scrt1.o /lib/x86_64-linux-gnu/crti.o /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/clang_rt.crtbegin.o -L/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib -L/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc -L/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/lean -L/usr/lib/gcc/x86_64-linux-gnu/9 -L/usr/lib/gcc/x86_64-linux-gnu/9/../../../../lib64 -L/lib/x86_64-linux-gnu -L/lib/../lib64 -L/usr/lib/x86_64-linux-gnu -L/usr/lib/../lib64 -L/home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/../lib -L/lib -L/usr/lib ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc/libc_nonshared.a /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/glibc/libpthread_nonshared.a --as-needed -Bstatic -lgmp -lunwind -luv -lpthread -ldl -lrt -Bdynamic --no-as-needed --start-group -lleancpp -lLean --end-group -lStd --start-group -lInit -lleanrt --end-group -Bstatic -lc++ -lc++abi -Bdynamic -lLake --as-needed -lgmp -luv -lpthread -ldl -lrt --no-as-needed -lm -ldl /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/libclang_rt.builtins.a -lpthread -lc /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/libclang_rt.builtins.a /home/foo/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/clang_rt.crtend.o /lib/x86_64-linux-gnu/crtn.o
ld.lld: error: undefined symbol: l_IO_println___at_Lean_instEval___spec__1
>>> referenced by Main.c
>>>               ././.lake/build/ir/Cache/Main.c.o.export:(l_main___lambda__4)
>>> referenced by Main.c
>>>               ././.lake/build/ir/Cache/Main.c.o.export:(l_main___lambda__4)
>>> referenced by Main.c
>>>               ././.lake/build/ir/Cache/Main.c.o.export:(l_main___lambda__7)
>>> referenced 38 more times

ld.lld: error: undefined symbol: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_2633____spec__1
>>> referenced by Requests.c
>>>               ././.lake/build/ir/Cache/Requests.c.o.export:(l_Cache_Requests_downloadFiles___lambda__5)
>>> referenced by Requests.c
>>>               ././.lake/build/ir/Cache/Requests.c.o.export:(l_Cache_Requests_downloadFiles___lambda__7)
>>> referenced by Requests.c
>>>               ././.lake/build/ir/Cache/Requests.c.o.export:(l_Cache_Requests_downloadFiles___lambda__7)
>>> referenced 1 more times

ld.lld: error: undefined symbol: __dladdr
>>> referenced by dladdr.o:(dladdr) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: __dlsym
>>> referenced by dlsym.o:(dlsym) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: _dl_deallocate_tls
>>> referenced by allocatestack.c:277
>>>               pthread_create.o:(free_stacks) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__deallocate_stack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__free_tcb) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 1 more times

ld.lld: error: undefined symbol: _dl_make_stack_executable
>>> referenced by allocatestack.c:814
>>>               pthread_create.o:(__make_stacks_executable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_stack_flags
>>> referenced by allocatestack.c:525
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:647
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls_init
>>> referenced by allocatestack.c:247
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls
>>> referenced by allocatestack.c:502
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:622
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __tunable_get_val
>>> referenced by elision-conf.c:110 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:110)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:112 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:112)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:114 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:114)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 3 more times

ld.lld: error: undefined symbol: _dl_x86_cpu_features
>>> referenced by elision-conf.c:66 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:66)
>>>               elision-lock.o:(_dl_tunable_set_elision_enable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __libc_stack_end
>>> referenced by nptl-init.c:272
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:98
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:125
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_get_tls_static_info
>>> referenced by nptl-init.c:311
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_pagesize
>>> referenced by nptl-init.c:335
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:344
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:393
>>>               nptl-init.o:(__pthread_get_minstack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 2 more times

ld.lld: error: undefined symbol: _dl_init_static_tls
>>> referenced by nptl-init.c:360
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_wait_lookup_done
>>> referenced by nptl-init.c:362
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __dlopen
>>> referenced by dlopen.o:(dlopen) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: __dlerror
>>> referenced by dlerror.o:(dlerror) in archive /lib/x86_64-linux-gnu/libdl.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)

[María Inés de Frutos Fernández]

I noticed the error in #18172 and I also get it in the current Mathlib master, but I do not get it for instance in #18388 (from last week, and in which I have not merged master).

[Kevin Buzzard]

I just updated FLT and got the same error. I tried

buzzard@buster:~/.elan/toolchains$ rm -rf leanprover--lean4---v4.14.0-rc1

and

buzzard@buster:~/.elan/update-hashes$ rm -rf leanprover--lean4---v4.14.0-rc1

and

buzzard@buster:~/lean-projects/FLT$ rm -rf .lake

and I get

buzzard@buster:~/lean-projects/FLT$ lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '././.lake/packages/mathlib'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git to '././.lake/packages/checkdecls'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: plausible: cloning https://github.com/leanprover-community/plausible to '././.lake/packages/plausible'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
✖ [10/10] Building cache
trace: .> /home/buzzard/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc -o ././.lake/packages/mathlib/.lake/build/bin/cache ././.lake/packages/mathlib/.lake/build/ir/Cache/Main.c.o.export ././.lake/packages/mathlib/.lake/build/ir/Cache/IO.c.o.export ././.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c.o.export ././.lake/packages/mathlib/.lake/build/ir/Cache/Requests.c.o.export
info: stderr:
ld.lld: error: undefined symbol: __dladdr
>>> referenced by dladdr.o:(dladdr) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: __dlsym
>>> referenced by dlsym.o:(dlsym) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: _dl_deallocate_tls
>>> referenced by allocatestack.c:277
>>>               pthread_create.o:(free_stacks) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__deallocate_stack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:804
>>>               pthread_create.o:(__free_tcb) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 1 more times

ld.lld: error: undefined symbol: _dl_make_stack_executable
>>> referenced by allocatestack.c:814
>>>               pthread_create.o:(__make_stacks_executable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_stack_flags
>>> referenced by allocatestack.c:525
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:647
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls_init
>>> referenced by allocatestack.c:247
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_allocate_tls
>>> referenced by allocatestack.c:502
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by allocatestack.c:622
>>>               pthread_create.o:(__pthread_create_2_1) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __tunable_get_val
>>> referenced by elision-conf.c:110 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:110)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:112 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:112)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by elision-conf.c:114 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:114)
>>>               elision-lock.o:(elision_init) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 3 more times

ld.lld: error: undefined symbol: _dl_x86_cpu_features
>>> referenced by elision-conf.c:66 (../sysdeps/unix/sysv/linux/x86/elision-conf.c:66)
>>>               elision-lock.o:(_dl_tunable_set_elision_enable) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __libc_stack_end
>>> referenced by nptl-init.c:272
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:98
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by pthread_getattr_np.c:125
>>>               pthread_getattr_np.o:(pthread_getattr_np) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_get_tls_static_info
>>> referenced by nptl-init.c:311
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_pagesize
>>> referenced by nptl-init.c:335
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:344
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced by nptl-init.c:393
>>>               nptl-init.o:(__pthread_get_minstack) in archive /lib/x86_64-linux-gnu/libpthread.a
>>> referenced 2 more times

ld.lld: error: undefined symbol: _dl_init_static_tls
>>> referenced by nptl-init.c:360
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: _dl_wait_lookup_done
>>> referenced by nptl-init.c:362
>>>               nptl-init.o:(__pthread_initialize_minimal_internal) in archive /lib/x86_64-linux-gnu/libpthread.a

ld.lld: error: undefined symbol: __dlopen
>>> referenced by dlopen.o:(dlopen) in archive /lib/x86_64-linux-gnu/libdl.a

ld.lld: error: undefined symbol: __dlerror
>>> referenced by dlerror.o:(dlerror) in archive /lib/x86_64-linux-gnu/libdl.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/buzzard/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc' exited with code 1
Some required builds logged failures:
- cache
error: build failed
buzzard@buster:~/lean-projects/FLT$

[Yaël Dillies]

There is now lean4#5966 to fix it

[Kevin Buzzard]

I am surprised that I'm getting the error locally but CI is passing in FLT

[Kevin Buzzard]

Can I not work on FLT any more until this fix makes it to mathlib?

[Kim Morrison]

Should be fixed in mathlib in a few hours.

[Kim Morrison]

#18682

[Kevin Buzzard]

As ever, thank you to our amazing community for getting things back up and running so quickly!

[Kevin Buzzard]

And I can confirm that we're back on track! Many thanks again.

[María Inés de Frutos Fernández]

It worked for me too. Thanks!

[Rémy Degenne]

I just cloned mathlib, entered the folder and tried lake exe cache get. I get a warning about an unused argument in clang and the cache is not downloaded.
This is on windows.

Here is the output of lake exe cache get

$ lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '1622a8693b31523c8f82db48e01b14c74bc1f155'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '9cb79405471ae931ac718231d6299bfaffef9087'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '07f60e90998dfd6592688a14cd67bd4e384b77b2'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '79402ad9ab4be9a2286701a9880697e2351e4955'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'b2e8b6868397fcd93c00aca7278b933c16c0ffb3'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Ô£ö [2/10] Built Cache.IO
Ô£ö [3/10] Built Cache.Hashing
Ô£ö [4/10] Built Cache.IO:c.o
Ô£ö [5/10] Built Cache.Requests
Ô£ö [6/10] Built Cache.Hashing:c.o
Ô£ö [7/10] Built Cache.Main
Ô£ö [8/10] Built Cache.Requests:c.o
Ô£ö [9/10] Built Cache.Main:c.o
Ôä╣ [10/10] Built cache
info: stderr:
clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]

Any idea of what the issue is, and how I can get a cache?

[Rémy Degenne]

That's on 4.16.0-rc1. I tried lake exe cache get on a branch on 4.15.0 and it works fine (I don't see any warning and I get a download).

[Mauricio Collares]

I assume this happens on Windows?

[Rémy Degenne]

Yes, this is on windows

[Mauricio Collares]

Oh, you had already mentioned that, sorry

[Mauricio Collares]

If I had to guess, I'd say this is a regression from lean4#6176, which probably exposes problems with other toolchain setups. See, for example, #mathlib4 > lake exe cache get error on NixOS

[Rémy Degenne]

I tested it on ubuntu as well, and I have no problem there.

[Mauricio Collares]

The flags passed to the linker are in script/prepare-llvm-mingw.sh (they're defined as CMake variables which are substituted into src/util/ffi.cpp). But this should just be a compiler warning. I guess Mathlib treats any noise as an error and doesn't run the cache binary? Do you see any lines starting with error instead of warning?

[Mauricio Collares]

I think Lake wanted to pass -Wno-unused-command-line-argument to suppress these warnings, but I couldn't follow the code to see if it does that for the bundled compiler

[Junyan Xu]

I got the following error on Windows last night after checking out latest master; it looks different than yours, but may be caused by the same change on master.

PS ...\mathlib4> lake exe cache get
info: downloading component 'lean'
252.2 MiB / 252.2 MiB (100 %)  18.8 MiB/s ETA:   0 s
info: installing component 'lean'
error: compiled configuration is invalid; run with '-R' to reconfigure

I tried lake exe cache clean! but I got the same error. After searching the error message on Zulip, I found a message suggesting to delete the .lake folder. I did that and then lake exe cache get worked normally, but I'm not sure why it solved the problem.

[Rémy Degenne]

Same error after I deleted .lake (which is not very surprising, since I got the error on a fresh clone)

[Mauricio Collares]

That seems like a different problem, but lake should just recompile the configuration on its own if it detects an invalid lakefile.olean

[Sébastien Gouëzel]

I also get failure to download cache on mathlib master, on Windows. Here is my error:

PS C:\Users\Sebastien\Desktop\mathlib4> lake exe cache get
info: downloading component 'lean'
260.5 MiB / 260.5 MiB (100 %)  85.0 MiB/s ETA:   0 s
info: installing component 'lean'
info: plausible: checking out revision '1622a8693b31523c8f82db48e01b14c74bc1f155'
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: checking out revision '9cb79405471ae931ac718231d6299bfaffef9087'
info: proofwidgets: checking out revision '07f60e90998dfd6592688a14cd67bd4e384b77b2'
info: aesop: checking out revision '79402ad9ab4be9a2286701a9880697e2351e4955'
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: checking out revision 'b2e8b6868397fcd93c00aca7278b933c16c0ffb3'
Ô£û [10/10] Building cache
trace: .> c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.16.0-rc1/lib -static-libgcc -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread
info: stderr:
clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]
ld.lld: error: undefined symbol: __mingw_init_ehandler
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(__tmainCRTStartup)

ld.lld: error: undefined symbol: __security_init_cookie
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_startw)
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_start)

ld.lld: error: undefined symbol: mingw_app_type
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_app_type)

ld.lld: error: undefined symbol: mingw_initcharmax
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initcharmax)

ld.lld: error: undefined symbol: mingw_initltssuo_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltssuo_force)

ld.lld: error: undefined symbol: mingw_initltsdyn_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdyn_force)

ld.lld: error: undefined symbol: mingw_initltsdrot_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdrot_force)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\Sebastien\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\bin\clang.exe' exited with code 1
Some required builds logged failures:
- cache
error: build failed

[Sébastien Gouëzel]

Removing from the path the directory c:/Strawberry/c/bin (which contains a copy of ld) fixes the build. I still get the warning that a flag is not used, but it's not an error, and cache works fine afterwards:

Ôä╣ [10/10] Built cache
info: stderr:
clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]
Attempting to download 5824 file(s)
Downloaded: 5824 file(s) [attempted 5824/5824 = 100%] (100% success)
Decompressing 5824 file(s)
Unpacked in 13100 ms
Completed successfully!

[Mauricio Collares]

So lake doesn't treat noise as an error. I wonder why @Rémy Degenne doesn't see proper errors then.

[Junyan Xu]

To be clear, I was on commit a36b4f2f1dc49c3c40c95b80d96fbba3f1ec98f1 (21 hours ago), which is before #20464 was merged (12 hours ago).

[Sebastian Ullrich]

lean#6535 tests if we can just remove the linted linker argument

[Kim Morrison]

I can reproduce

clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]

on my windows box at the tag v4.16.0-rc1, and confirm that changing the lean-toolchain to leanprover/lean4-pr-releases:pr-release-6535 makes it go away again!

So I think we will be merging lean#6535 soon, and I'll cut a v4.16.0-rc2 with (at least!!) that.

[Sebastian Ullrich]

Awesome, thanks for testing!

[Mauricio Collares]

I'm still surprised that that warning, with no other errors, is enough to stop lake exe cache get from working in some cases. Is that really what's happening on Windows? Regardless, fixing the warning is much appreciated, of course.

[Mauricio Collares]

Ah, perhaps it's a combination of this and the other bug for projects depending on mathlib: you get this warning, then cache runs but doesn't actually produce a working cache because of the trace mismatch

[Sebastian Ullrich]

The warning is likely completely independent of the cache fetch failure given the latter happens on any platform

[Eric Wieser]

Is the issue that the warning gets recorded in a data file somewhere so that lake can replay it later, and is therefore incorporated into the hash?

[Eric Wieser]

So platforms with the warning get a different hash to CI which did not have the warning

[Kim Morrison]

I'm not sure if that is correct or not, but if it is, I will release v4.16.0-rc2 asap (without waiting for other fixes which might take until next week when Mac is back).

[Kim Morrison]

So far I can not reproduce the failure of lake exe cache get on my windows box. My guess is that lean#6535 is independent of the cache failure, and so we are not justified in making v4.16.0-rc2 just for lean#6535.

(@Johan Commelin, so we won't try out the release checklist today!)

[Kim Morrison]

We will need to make an rc2 later for the cache problems in downstream projects, but that still needs a solution!

[Joachim Breitner]

Eric Wieser said:

Is the issue that the warning gets recorded in a data file somewhere so that lake can replay it later, and is therefore incorporated into the hash?

That's a good question. I had assumed that the trace hash is based only on inputs (file contents of the file source and it's dependencies' source, toolchain versions, flags) so that it can be computed ahead of time for the whole tree of jobs (like nix works). In that architecture, the output of one job (whether messages or actual build artifacts) can't affect the trace of depending jobs. But maybe I'm wrong and the trace really takes the dependencies' build artifacts into account.

[Edward van de Meent]

i also have issues with getting cache... i'm not sure if this is the same error or not though, as i haven't seen part of my error message here yet...

$ lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '1622a8693b31523c8f82db48e01b14c74bc1f155'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '9cb79405471ae931ac718231d6299bfaffef9087'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '07f60e90998dfd6592688a14cd67bd4e384b77b2'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '79402ad9ab4be9a2286701a9880697e2351e4955'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'b2e8b6868397fcd93c00aca7278b933c16c0ffb3'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Γ£û [10/10] Building cache
trace: .> c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.16.0-rc1/lib -static-libgcc -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld -L c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread
info: stderr:
clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]
ld.lld: error: C:/MinGW/lib/crt2.o: machine type x86 conflicts with x64
ld.lld: error: C:/MinGW/lib/gcc/mingw32/6.3.0/crtbegin.o: machine type x86 conflicts with x64
ld.lld: error: C:/MinGW/lib/gcc/mingw32/6.3.0/crtend.o: machine type x86 conflicts with x64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\bin\clang.exe' exited with code 1
Some required builds logged failures:
- cache
error: build failed

my machine runs windows.

[Sébastien Gouëzel]

Same issue as I had above: building cache tries to use your own compiler or linker (probably on the path) instead of the one shipped with Lean. Removing your compiler from the path should probably fix it.

[Edward van de Meent]

it's not on my path not anymore

[Edward van de Meent]

at least now cache compiles

[Sebastian Ullrich]

What exactly do you mean by "not anymore"? Changing the path in the system settings requires a reboot afaik

[Edward van de Meent]

no, you can just edit them

[Sébastien Gouëzel]

No, not a reboot: just reopening the terminal once you have changed the path is enough.

[Edward van de Meent]

i had to reopen VScode

[Edward van de Meent]

but that might be because of how VScode handles terminals

[Sebastian Ullrich]

lean#6547 might fix this issue

[Robin Carlier]

I don’t know if this is the same issue/related (but the timing is suspicious): after updating my lean stuff today after a while, cache also fails to build on NixOS. Tested on mathlib as well as on an other mathlib-dependent project. I see no sign of it picking up the wrong linker or compiler though. Full build failure log is too big for zulip so here’s a gist.

[Sebastian Ullrich]

You need to use elan from recent nixpkgs-unstable (and then reinstall the toolchain), see #mathlib4 > lake exe cache get error on NixOS

[Robin Carlier]

Oh, unrelated then, I could have scrolled a bit more in the topic list :sweat_smile:, thanks! I’ll use the toolchain from that pr

[Kim Morrison]

@Sébastien Gouëzel or @Edward van de Meent are either of you able to provide instructions for reproducing this problem? Presumably such instructions should including modifying the windows PATH to include some system compiler and/or linker?

I would love to be able to reproduce your issue, and verify that lean#6547 fixes it, but despite having a (virtual) windows box available I don't know what to do yet.

[Sébastien Gouëzel]

It would involve installing MingW or Strawberry Perl or whatever contains gcc and ld, and adding it to the path. A simpler way of testing things would be that you give me precise instructions (for dummies :-) on how to test the branch on my own computer.

[Edward van de Meent]

@Kim Morrison it seems @Asei Inoue has a CI step failing because of this, see the link at #general > Updating to 4.16.0-rc1

[Edward van de Meent]

i suspect that at the very least is reproducable

[Edward van de Meent]

maybe not minimal, but it's something

[Kim Morrison]

Sébastien Gouëzel said:

It would involve installing MingW or Strawberry Perl or whatever contains gcc and ld, and adding it to the path. A simpler way of testing things would be that you give me precise instructions (for dummies :-) on how to test the branch on my own computer.

@Sébastien Gouëzel, it should just be a matter of checking out lean-pr-testing-6547. Hopefully on master adding or removing the executables from from path makes a difference, but on lean-pr-testing-6547 it always works.

[Sébastien Gouëzel]

No, it is still failing.

PS C:\Users\Sebastien\Desktop\mathlib4> git checkout lean-pr-testing-6547
Switched to a new branch 'lean-pr-testing-6547'
Branch 'lean-pr-testing-6547' set up to track remote branch 'lean-pr-testing-6547' from 'origin'.
PS C:\Users\Sebastien\Desktop\mathlib4> git pull
Already up to date.
PS C:\Users\Sebastien\Desktop\mathlib4> lake exe cache get
info: downloading component 'lean'
335.2 MiB / 335.2 MiB (100 %)   2.7 MiB/s ETA:   0 s
info: installing component 'lean'
info: plausible: checking out revision '7a6030b92f001a0e08c59c8f39a97cdf32f627ed'
info: batteries: checking out revision '8ab7504dc86b82d7e15c0ad52412e85932e7d4db'
Ô£û [10/10] Building cache
trace: .> c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/lib -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld --ld-path=c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread
info: stderr:
ld.lld: error: undefined symbol: __mingw_init_ehandler
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(__tmainCRTStartup)

ld.lld: error: undefined symbol: __security_init_cookie
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_startw)
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_start)

ld.lld: error: undefined symbol: mingw_app_type
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_app_type)

ld.lld: error: undefined symbol: mingw_initcharmax
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initcharmax)

ld.lld: error: undefined symbol: mingw_initltssuo_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltssuo_force)

ld.lld: error: undefined symbol: mingw_initltsdyn_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdyn_force)

ld.lld: error: undefined symbol: mingw_initltsdrot_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdrot_force)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\bin\clang.exe' exited with code 1
Some required builds logged failures:
- cache
error: build failed

[Sebastian Ullrich]

@Sébastien Gouëzel Could you please run the traced cmdline with -v appended?

c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/lib -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld --ld-path=c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld -L c:\Users\Sebastien\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread -v

[Sébastien Gouëzel]

C:\Users\sgouezel_A\Desktop\mathlib4>c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/lib -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld --ld-path=c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld -L c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread -v
clang version 15.0.1
Target: x86_64-w64-windows-gnu
Thread model: posix
InstalledDir: c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/bin
 "c:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld" -m i386pep -Bdynamic -o ".\\.\\.lake\\build\\bin\\cache.exe" C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o C:/Strawberry/c/lib/gcc/x86_64-w64-mingw32/8.3.0/crtbegin.o "-Lc:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547/lib" "-Lc:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547\\lib\\lean" -LC:/Strawberry/c/lib/gcc/x86_64-w64-mingw32/8.3.0 -LC:/Strawberry/c/x86_64-w64-mingw32/lib -LC:/Strawberry/c/x86_64-w64-mingw32/mingw/lib -LC:/Strawberry/c/lib -LC:/Strawberry/c/x86_64-w64-mingw32/sys-root/mingw/lib -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows ".\\.\\.lake\\build\\ir\\Cache\\Main.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\IO.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\Hashing.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\Requests.c.o.noexport" -Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Bdynamic --start-group -lleancpp -lLean --end-group -lStd --start-group -lInit -lleanrt --end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase --stack 104857600 -licu -lm -lbcrypt -lmingw32 c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows/libclang_rt.builtins-x86_64.a -lmoldname -lmingwex -lpthread -ladvapi32 -lshell32 -luser32 -lkernel32 -lmingw32 c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows/libclang_rt.builtins-x86_64.a -lmoldname -lmingwex -lkernel32 C:/Strawberry/c/lib/gcc/x86_64-w64-mingw32/8.3.0/crtend.o
ld.lld: error: undefined symbol: __mingw_init_ehandler
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(__tmainCRTStartup)

ld.lld: error: undefined symbol: __security_init_cookie
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_startw)
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.l_start)

ld.lld: error: undefined symbol: mingw_app_type
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_app_type)

ld.lld: error: undefined symbol: mingw_initcharmax
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initcharmax)

ld.lld: error: undefined symbol: mingw_initltssuo_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltssuo_force)

ld.lld: error: undefined symbol: mingw_initltsdyn_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdyn_force)

ld.lld: error: undefined symbol: mingw_initltsdrot_force
>>> referenced by C:/Strawberry/c/x86_64-w64-mingw32/lib/crt2.o:(.refptr.mingw_initltsdrot_force)
clang: error: linker command failed with exit code 1 (use -v to see invocation)

[Sébastien Gouëzel]

I can try as many command lines as you want to see if you can find a combination of flags ensuring the Strawberry directories are not included in the search path :-)

[Sébastien Gouëzel]

(Don't be surprised by the change from Sebastien to sgouezel_A directory, I am on a different computer -- but the very same problem shows up)

[Sébastien Gouëzel]

(A hack would be to empty the path before compiling :-)

[Sebastian Ullrich]

Wow, I'm surprised LLVM would use PATH to look up object files...?

[Sébastien Gouëzel]

Just for the record, emptying the path works fine:

C:\Users\sgouezel_A\Desktop\mathlib4>set PATH=

C:\Users\sgouezel_A\Desktop\mathlib4>c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\bin\clang.exe -o .\.\.lake\build\bin\cache.exe .\.\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake\build\ir\Cache\Requests.c.o.noexport -L c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/lib -Wl,-Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Wl,-Bdynamic -fuse-ld=lld --ld-path=c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld -L c:\Users\sgouezel_A\.elan\toolchains\leanprover--lean4-pr-releases---pr-release-6547\lib\lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt -pthread -v
clang version 15.0.1
Target: x86_64-w64-windows-gnu
Thread model: posix
InstalledDir: c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/bin
 "c:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547/bin/ld.lld" -m i386pep -Bdynamic -o ".\\.\\.lake\\build\\bin\\cache.exe" c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/crt2.o c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/crtbegin.o "-Lc:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547/lib" "-Lc:\\Users\\sgouezel_A\\.elan\\toolchains\\leanprover--lean4-pr-releases---pr-release-6547\\lib\\lean" -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/x86_64-w64-mingw32/lib -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/x86_64-w64-mingw32/mingw/lib -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/x86_64-w64-mingw32/sys-root/mingw/lib -Lc:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows ".\\.\\.lake\\build\\ir\\Cache\\Main.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\IO.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\Hashing.c.o.noexport" ".\\.\\.lake\\build\\ir\\Cache\\Requests.c.o.noexport" -Bstatic -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lunwind -Bdynamic --start-group -lleancpp -lLean --end-group -lStd --start-group -lInit -lleanrt --end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32 -lshell32 -lucrtbase --stack 104857600 -licu -lm -lbcrypt -lmingw32 c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows/libclang_rt.builtins-x86_64.a -lmoldname -lmingwex -lpthread -ladvapi32 -lshell32 -luser32 -lkernel32 -lmingw32 c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/clang/15.0.1/lib/windows/libclang_rt.builtins-x86_64.a -lmoldname -lmingwex -lkernel32 c:/Users/sgouezel_A/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-6547/lib/crtend.o

[Sebastian Ullrich]

@Sébastien Gouëzel Could you please try lean-pr-testing-6574 instead?

[Sébastien Gouëzel]

It works!

[Sebastian Ullrich]

Thanks!

[Junyan Xu]

Something strange happening (on Windows) today after mergin latest mathlib (4e6cc37012f75c9de40476ad722f02512a8b1f09, probably already happening with 89f60e1045dca9bba5a7d8706ec160706782d7ef):

PS C:\Users\xujys\mathlib4> lake exe cache get
info: downloading component 'lean'
260.5 MiB / 260.5 MiB (100 %) 24.4 MiB/s ETA: 0 s
info: installing component 'lean'
error: toolchain 'leanprover/lean4:v4.16.0-rc1' does not have the binary C:\Users\xujys\.elan\toolchains\leanprover--lean4---v4.16.0-rc1\bin\lake.exe

PS C:\Users\xujys\mathlib4> elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.15.0
info: downloading component 'lean'
252.2 MiB / 252.2 MiB (100 %) 39.2 MiB/s ETA: 0 s
info: installing component 'lean'
error: could not remove 'toolchain directory' directory: 'C:\Users\xujys\.elan\toolchains\leanprover--lean4---stable'

leanprover/lean4:stable update failed - Lean (version 4.2.0, commit 0d7051497ea0, Release)

error: could not create link from 'C:\Users\xujys\.elan\bin\elan.exe' to 'C:\Users\xujys\.elan\bin\lake.exe'

[Junyan Xu]

Eventually, I found a folder leanprover--lean4---v4.16.tmp under .elan/toolchains and copied its content into leanprover--lean4---v4.16.0-rc1, then lake exe cache get works again.

[Sebastian Ullrich]

We've had this error before but the tmp information is new, thanks! Unfortunately it is still mysterious to me: what we are doing is to unpack the toolchain into the tmp directory, then rename it: https://github.com/leanprover/elan/blob/master/src/elan-dist/src/manifestation.rs#L108-L132. Your first cmdline doesn't show any error in this part of the code. So how could we end up with a whole tmp and a partial final directory?

[Junyan Xu]

I'm not sure; leanprover--lean4---v4.16.0-rc1 contained only a src folder.

[Michael Stoll]

I haven't followed the discussion in detail; sorry if this is obvious:
Is it safe now to update to the latest Mathlib in a project that depends on it (without having to then build all of Mathlib locally)?

[Sébastien Gouëzel]

No. You should stay on 4.15.0 for now.

[Michael Stoll]

Is there some indication regarding how long it will take for the problem to be resolved?

[Sébastien Gouëzel]

I don't even know if the cause of the problem has been identified...

[Mauricio Collares]

The change that caused the problem is very likely lean4#6388. It extensively refactored the trace calculation

[Mauricio Collares]

But reverting it is a bit annoying since it includes tons of API changes

[Mauricio Collares]

Lake code is very hard to understand (architecturally speaking) in a few hours, so if I understand correctly the current status is "waiting for Mac to come back from holidays"

[Kim Morrison]

Hoping for a fix and then a v4.16.0-rc2 early next week.

[Kim Morrison]

Note that if the CI adjustment #20532 had been in place, we would have caught this well before releasing v4.16.0-rc1. If anyone can think of further ways to more robustly test the behaviour of Mathlib with respect to downstream projects, within Mathlib CI, I would love to see these implemented!

[Sebastian Ullrich]

Do also consider having your project follow Mathlib stable instead of master if you don't want to be among the first to be exposed to new issues from either Lean or Mathlib :)

[Michael Stoll]

My use case is that I'm developing stuff that I want to get into Mathlib successively, so that whenever one of the PRs gets merged, I want to update Mathlib in my project so that I can remove the parts that have been upstreamed. For this it doesn't help so much to be restricted to the once-in-a-while stable releases; I need the finer granularity.

[Junyan Xu]

Small update: I've nuked the .lake directory 3-4 times in the last few days, each time after checking out some branch with recent master merged into it. Error messages are like this:

PS C:\Users\xujys\mathlib4> lake exe cache get
info: plausible: checking out revision '1622a8693b31523c8f82db48e01b14c74bc1f155'
info: importGraph: checking out revision '9cb79405471ae931ac718231d6299bfaffef9087'
info: proofwidgets: checking out revision '07f60e90998dfd6592688a14cd67bd4e384b77b2'
error: compiled configuration is invalid; run with '-R' to reconfigure

Compared to my previous report there's no "info: installing component 'lean'" step but these "checking out revision" info were new.

[Edward van de Meent]

Junyan Xu said:

I've nuked the .lake directory 3-4 times in the last few days,

by running lake exe cache get or before running it?

[Junyan Xu]

Each time I ran lake exe cache get, got the error

error: compiled configuration is invalid; run with '-R' to reconfigure

and my current solution to the error is to nuke .lake.

[Floris van Doorn]

I also got the same error after merging an old PR into the latest Mathlib master just now (on version leanprover/lean4:v4.17.0-rc1)