lake exe cache get from mathlib4

Stream: new members

[Bolton Bailey]

When I run lake exe cache get from mathlib4 itself, is it supposed to get the cache, or is there a different command for that?

[Bolton Bailey]

When I try this, I get the error

boltonbailey@starlight mathlib4 % lake exe cache get
info: [8/8] Linking cache
error: > /Users/boltonbailey/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/bin/leanc -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o
error: stderr:
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: error: ./build/ir/Cache/Main.o: unhandled file type
ld64.lld: error: ./build/ir/Cache/IO.o: unhandled file type
ld64.lld: error: ./build/ir/Cache/Hashing.o: unhandled file type
ld64.lld: error: ./build/ir/Cache/Requests.o: unhandled file type
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.3.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.3.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.3.0, which is newer than target minimum of 13.0.0
ld64.lld: error: undefined symbol: _main
>>> referenced by the entry point
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/boltonbailey/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/bin/leanc` exited with code 1
boltonbailey@starlight mathlib4 %

[Bolton Bailey]

For example, I see in .devcontainer/devcontainer.json the line "onCreateCommand": "lake exe cache get!",. Does the exclamation point matter?

[Ruben Van de Velde]

The ! forces a download in case you have a corrupted cache

[Bolton Bailey]

Surely that shouldn't be necessary for a container?

[Ruben Van de Velde]

Maybe it's slightly more efficient if you know it's the first download?

[Ruben Van de Velde]

Anyway, it seems that you're failing to build the code that is supposed to download the cache

[Bolton Bailey]

TBH, maybe I should just try to use this containerization I found

[Kevin Buzzard]

Just to confirm that lake exe cache get works fine for mathlib (for me).

[Bolton Bailey]

Perhaps it's some kind of issue with xcode, which will be fixed if I update it? I can try updating it later.