ld undefined symbol on `exe cache`

Stream: general

[Yakov Pechersky]

Starting today, when I tried to check out the new rc mathlib, I began to get ld errors. I switched to an older branch, ran lake exe cache get, and got this ld error:

$ lake exe cache get
✖ [12/12] Building cache
trace: .> /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/clang -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/Lean.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 --sysroot /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1 -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc/libc_nonshared.a /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.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
info: stderr:
ld.lld: error: undefined symbol: l_instInhabitedError
>>> referenced by IO.c
>>>               ././.lake/build/ir/Cache/IO.c.o.export:(initialize_Cache_IO)

ld.lld: error: undefined symbol: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3114____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
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/clang' exited with code 1
Some required builds logged failures:
- cache
error: build failed

Starting a new shell didn't help.

[Yakov Pechersky]

Uninstalling the v4.17.0-rc1 and v4.18.0-rc1 toolchains and rerunning didn't help.

$ elan toolchain list
leanprover/lean4-pr-releases:pr-release-6800
leanprover/lean4:v4.12.0-rc1
leanprover/lean4:v4.13.0
leanprover/lean4:v4.13.0-rc3
leanprover/lean4:v4.14.0-rc2
leanprover/lean4:v4.15.0-rc1
leanprover/lean4:v4.16.0-rc1
leanprover/lean4:v4.16.0-rc2
leanprover/lean4:v4.17.0-rc1
leanprover/lean4:v4.18.0-rc1
$ elan toolchain uninstall leanprover/lean4:v4.17.0-rc1
info: uninstalling toolchain 'leanprover/lean4:v4.17.0-rc1'
info: toolchain 'leanprover/lean4:v4.17.0-rc1' uninstalled
$ elan toolchain uninstall leanprover/lean4:v4.18.0-rc1
info: uninstalling toolchain 'leanprover/lean4:v4.18.0-rc1'
info: toolchain 'leanprover/lean4:v4.18.0-rc1' uninstalled
$ lake exe cache get
info: downloading https://github.com/leanprover/lean4/releases/download/v4.17.0-rc1/lean-4.17.0-rc1-linux.tar.zst
279.9 MiB / 279.9 MiB (100 %)  42.3 MiB/s ETA:   0 s
info: installing /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1
✖ [12/12] Building cache
trace: .> /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/clang -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/Lean.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 --sysroot /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1 -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc/libc_nonshared.a /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/yakov/.elan/toolchains/leanprover--lean4---v4.17.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
info: stderr:
ld.lld: error: undefined symbol: l_instInhabitedError
>>> referenced by IO.c
>>>               ././.lake/build/ir/Cache/IO.c.o.export:(initialize_Cache_IO)

ld.lld: error: undefined symbol: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3114____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
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/yakov/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/clang' exited with code 1
Some required builds logged failures:
- cache
error: build failed

[Yakov Pechersky]

Deleting .lake fixed it: $ rm -rf .lake

[Sebastian Ullrich]

@Mac Malone Could we be missing a dependency edge on the Lean version here?

[Ruben Van de Velde]

I ran into this as well

[Mac Malone]

@Sebastian Ullrich Possibly, but that would be suprising. Module elaboration, C compilaiton, and executable linking should all include the Lean trace. It also is not quite clear to me what the incompability is from these error reports.

Does anyone know what changed in cache between v4.17.0-rc1 and v4.18.0-rc1 that is triggering this incompatiblity? (If not, I will take a look myself when possible, though I am currently otherwise occupied.)

[Michael Rothgang]

Ruben Van de Velde said:

I ran into this as well

Me too. A reliable workaround seems to be to run lake clean; the lake exe cache (whatever) works again.

[Jon Eugster]

I mean there's a been a few refactors to cache recently, see #21238. I don't think anything concerning Json.getObjValAs? or IO.instInhabitedError has been touched though. Maybe imports: this PR changed some imports that seem relevant. Could that be a source of the issue?

[Jon Eugster]

ok I can reproduce this consistently:

Use a random branch on v4.17 like eugster/cache_parse_args and make sure your master is up-to-date with origin/master. Then:

rm -rf .lake
git checkout eugster/cache_parse_args
lake exe cache get
cp -R .lake/ good_lake_v4_17
git checkout origin/master
lake exe cache get
cp -R .lake/ good_lake_v4_18
git checkout eugster/cache_parse_args
lake exe cache get
cp -R .lake/ bad_lake_v4_17

Now comparing the these lakefolders reveals:

• diff -rq bad_lake_v4_17 good_lake_v4_17 shows tons of .hash changes first one for example Files bad_lake_v4_17/build/bin/cache.hash and good_lake_v4_17/build/bin/cache.hash differ
• diff -rq bad_lake_v4_17 good_lake_v4_18 no difference in .hash files, only a few changes, like Files bad_lake_v4_17/build/ir/Cache/Hashing.c.o.export.trace and good_lake_v4_18/build/ir/Cache/Hashing.c.o.export.trace differ

Not sure yet what to make of it all...

[Jon Eugster]

(and probably this difference in .hash files is a red hering since I think it's lake exe cache trying to download these)

[Jon Eugster]

Maybe the more important question is why

Files bad_lake_v4_17/build/ir/Cache/IO.c and
    good_lake_v4_17/build/ir/Cache/IO.c differ

[Jon Eugster]

Ok. @Mac Malone I think the build path changed between v4.17 and v4.18 from .lake/build/lib/ to .lake/build/lib/lean/. Is this deliberate? Ofc cache would be sensible to that but here is - I think - code to demonstrate this without cache:

[Jon Eugster]

> git checkout master
> lake exe mk_all
[...]
> ls .lake/build/lib
lean
> ls .lake/build/lib/lean
Mathlib         mk_all.ilean        mk_all.ilean.hash   mk_all.olean        mk_all.olean.hash   mk_all.trace
> git checkout 5269898d6a51d047931107c8d72d934d8d5d3753   # tag for mathlib v4.17
> rm -rf .lake
> lake exe mk_all
[...]
> ls .lake/build/lib
Mathlib         mk_all.ilean        mk_all.ilean.hash   mk_all.olean        mk_all.olean.hash   mk_all.trace
> ls .lake/build/lib/lean
ls: .lake/build/lib/lean: No such file or directory

[Jon Eugster]

Although if I move the files outside that new lean folder, I get a bit of a more instructive, but equally weird error:

✖ [2/12] Building Cache.Lean
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/me/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/lean ././././Cache/Lean.lean -R ./././. -o ././.lake/build/lib/Cache/Lean.olean -i ././.lake/build/lib/Cache/Lean.ilean -c ././.lake/build/ir/Cache/Lean.c --json
error: ././././Cache/Lean.lean:7:0: object file '././.lake/packages/batteries/.lake/build/lib/Lean/Util/Paths.olean' of module Lean.Util.Paths does not exist

Why would it try to import Lean.Util.Paths from batteries :thinking: ?

[Jon Eugster]

@Mac Malone sorry for all the noise. Here is a fully reconstructable MWE without Mathlib or Cache:

lake new Debug
cd Debug
echo "leanprover/lean4:v4.18.0-rc1" > lean-toolchain
cat lean-toolchain
echo "\nimport Lean.Util.Paths\n" >> Debug.lean
lake build
echo "leanprover/lean4:v4.17.0" > lean-toolchain
cat lean-toolchain
lake build

outputs the following error

leanprover/lean4:v4.18.0-rc1
info: Debug: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
Build completed successfully.
leanprover/lean4:v4.17.0
✖ [3/8] Building Debug
trace: .> LEAN_PATH=././.lake/build/lib DYLD_LIBRARY_PATH= /Users/[user]/.elan/toolchains/leanprover--lean4---v4.17.0/bin/lean ././././Debug.lean -R ./././. -o ././.lake/build/lib/Debug.olean -i ././.lake/build/lib/Debug.ilean -c ././.lake/build/ir/Debug.c --json
error: ././././Debug.lean:3:0: object file '././.lake/build/lib/Lean/Util/Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
Some required builds logged failures:
- Debug
error: build failed

I think with that I stop debugging for now :)

[Mac Malone]

@Jon Eugster So this is a problem with downgrading from 4.18 to 4.17? I was under the impression the original problem was the inverse (i.e., upgrading from 4.17 to 4.18). Thanks for the report! From this, I know what the problem is.

[Mac Malone]

With this problem, deleting the Lake directory or running lake clean when downgrading from Lean v4.18 is the most effective solution. Lake could change the default build directory again to avoid this downgrade issue, but that is largely a workaround (and would not fix users who already have a lib/lean). Thus, it is not clear that there is a better solution.

[Kim Morrison]

Remember that some people (particularly people doing reviewing work) may be "downgrading" several times per day, as many Mathlib branches will still be on an old toolchain. We need to make things smooth even in this scenario!

[Mac Malone]

I would love to! It is unfortunate that there is no real way to patch such old versions of Mathlib/Lake/Lean to make them forward-compatible (for this or any other forward-compatibility issues).

[Johan Commelin]

On current master I get

$ lake exe cache get
✖ [12/12] Building cache
trace: .> /home/jmc/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/cc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/Lean.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 -L /home/jmc/.elan/toolchains/leanprover--lean4---v4.18.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
info: stderr:
/nix/store/bwkb907myixfzzykp21m9iczkhrq5pfy-binutils-2.43.1/bin/ld: ././.lake/build/ir/Cache/IO.c.o.export: in function `initialize_Cache_IO':
IO.c:(.text+0x363f4): undefined reference to `l_IO_instInhabitedError'
/nix/store/bwkb907myixfzzykp21m9iczkhrq5pfy-binutils-2.43.1/bin/ld: ././.lake/build/ir/Cache/Requests.c.o.export: in function `l_Cache_Requests_downloadFiles___lambda__5':
Requests.c:(.text+0x3cab): undefined reference to `l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3070____spec__1'
/nix/store/bwkb907myixfzzykp21m9iczkhrq5pfy-binutils-2.43.1/bin/ld: ././.lake/build/ir/Cache/Requests.c.o.export: in function `l_Cache_Requests_downloadFiles___lambda__7':
Requests.c:(.text+0x47bb): undefined reference to `l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3070____spec__1'
/nix/store/bwkb907myixfzzykp21m9iczkhrq5pfy-binutils-2.43.1/bin/ld: Requests.c:(.text+0x4ba7): undefined reference to `l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3070____spec__1'
/nix/store/bwkb907myixfzzykp21m9iczkhrq5pfy-binutils-2.43.1/bin/ld: Requests.c:(.text+0x4f66): undefined reference to `l_Lean_Json_getObjValAs_x3f___at___private_Lean_Message_0__Lean_fromJsonBaseMessage____x40_Lean_Message___hyg_3070____spec__1'
collect2: error: ld returned 1 exit status
error: external command '/home/jmc/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/cc' exited with code 1
Some required builds logged failures:
- cache
error: build failed

[Kevin Buzzard]

(restoring this probably not relevant comment because Johan reponded to it) Current mathlib master cc7963812d581a6f867de0121bf3e06e2a66d67e working fine for me after lake exe cache get and lake build, is this a nix issue? But now I see that you're talking about Lean not mathlib.

[Johan Commelin]

Yeah, I'm also on cc7963812d5

[Johan Commelin]

It might be a nix issue...

[Sebastian Ullrich]

Isn't that the same error as above, i.e. try lake clean?

[Johan Commelin]

Weird... I thought I had tried that. But I tried a bit too many things...

[Johan Commelin]

It seems to be working again! Merci

[Sebastian Ullrich]

To be fair, the error message is a bit different because Nix elan uses a different linker

[Kevin Buzzard]

I'm running into this in FLT right now:

$ git checkout main
$ ## now on v4.18.0-rc1
$ lake exe cache get
$ ## works fine, so let's review a PR
$ gh pr checkout 373
$ ## this PR was made on v4.17.0-rc1
$ lake exe cache get
...
ld.lld: error: undefined symbol: l_instInhabitedError
...

Easily fixed with a lake clean.

[Kim Morrison]

Just pinging @Mac Malone in case he can think of a way lake could detect this condition itself, without the user needing the guess they have to run lake clean.