Zulip Chat Archive

Stream: lean4

Topic: elan toolchains broken on macos M1


Adrien Champion (Oct 25 2022 at 21:09):

I run macos (M1) and it seems elan toolchains are broken starting at nightly 2022-10-15.

Building code causes linking errors (below), the problem being that leanc thinks it's building for x86:

❯ elan default leanprover/lean4:nightly-2022-10-15
info: using existing install for 'leanprover/lean4:nightly-2022-10-15'
info: default toolchain set to 'leanprover/lean4:nightly-2022-10-15'

  leanprover/lean4:nightly-2022-10-15 unchanged - Lean (version 4.0.0-nightly-2022-10-15, commit 1eda0fd7349d, Release)

❯ leanc --version
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-apple-darwin21.6.0
Thread model: posix
InstalledDir: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-15/bin

Unlike the previous version (there's no 2022-10-14 as far as my elan can tell):

❯ elan default leanprover/lean4:nightly-2022-10-13
info: using existing install for 'leanprover/lean4:nightly-2022-10-13'
info: default toolchain set to 'leanprover/lean4:nightly-2022-10-13'

  leanprover/lean4:nightly-2022-10-13 unchanged - Lean (version 4.0.0-nightly-2022-10-13, commit 870de844dcc7, Release)

❯ leanc --version
clang version 14.0.0 (https://github.com/llvm/llvm-project 329fda39c507e8740978d10458451dcdb21563be)
Target: arm64-apple-darwin21.6.0
Thread model: posix
InstalledDir: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-13/bin

Linking errors on fresh install:

❯ ls -a
./  ../

❯ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# custom install with no toolchain

❯ elan install leanprover/lean4:nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-10-25
info: downloading component 'lean'
Total: 173.5 MiB Speed:  12.6 MiB/s
info: installing component 'lean'

  leanprover/lean4:nightly installed - Lean (version 4.0.0-nightly-2022-10-25, commit e55badef051a, Release)

❯ elan toolchain list
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2022-10-25

❯ leanc --version
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-apple-darwin21.6.0
Thread model: posix
InstalledDir: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly/bin

❯ lake init Test

❯ lake build
Building Test
Compiling Test
Building Main
Compiling Main
Linking test
error: > /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/bin/leanc -o ./build/bin/test ./build/ir/Main.o ./build/ir/Test.o
error: stderr:
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libInit.a(Init.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libInit.a(IO.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libleanrt.a(object.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libleanrt.a(init_module.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libleanrt.a(io.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/lib/lean/libleanrt.a(alloc.cpp.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 12.6.0, which is newer than target minimum of 12.0.0
ld64.lld: error: undefined symbol: _l_IO_println___at_Lean_instEval___spec__1
>>> referenced by ./build/ir/Main.o:(symbol __lean_main+0x10)
>>> referenced by ./build/ir/Main.o:(symbol _main+0x5b)

ld64.lld: error: undefined symbol: _lean_dec_ref_cold
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x150)
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x13b)
>>> referenced by ./build/ir/Main.o:(symbol _main+0xc4)
>>> referenced 2 more times

ld64.lld: error: undefined symbol: _lean_mark_persistent
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x126)
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x104)
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0xe4)
>>> referenced 3 more times

ld64.lld: error: undefined symbol: _lean_string_append
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x117)
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0xd5)

ld64.lld: error: undefined symbol: _lean_mk_string_from_bytes
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0xf5)
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0xb0)
>>> referenced by ./build/ir/Test.o:(symbol _initialize_Test+0x49)

ld64.lld: error: undefined symbol: _initialize_Init
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x50)
>>> referenced by ./build/ir/Test.o:(symbol _initialize_Test+0x1e)

ld64.lld: error: undefined symbol: _lean_alloc_small
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x1a)
>>> referenced by ./build/ir/Test.o:(symbol _initialize_Test+0x7a)

ld64.lld: error: undefined symbol: _lean_io_result_show_error
>>> referenced by ./build/ir/Main.o:(symbol _main+0x86)

ld64.lld: error: undefined symbol: _lean_finalize_task_manager
>>> referenced by ./build/ir/Main.o:(symbol _main+0x65)

ld64.lld: error: undefined symbol: _lean_init_task_manager
>>> referenced by ./build/ir/Main.o:(symbol _main+0x4a)

ld64.lld: error: undefined symbol: _lean_io_mark_end_initialization
>>> referenced by ./build/ir/Main.o:(symbol _main+0x2f)

ld64.lld: error: undefined symbol: _lean_set_panic_messages
>>> referenced by ./build/ir/Main.o:(symbol _main+0x28)
>>> referenced by ./build/ir/Main.o:(symbol _main+0x11)

ld64.lld: error: undefined symbol: _lean_initialize_runtime_module
>>> referenced by ./build/ir/Main.o:(symbol _main+0xa)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-25/bin/leanc` exited with code 1

❯ elan default leanprover/lean4:nightly-2022-10-15
info: using existing install for 'leanprover/lean4:nightly-2022-10-15'
info: default toolchain set to 'leanprover/lean4:nightly-2022-10-15'

  leanprover/lean4:nightly-2022-10-15 unchanged - Lean (version 4.0.0-nightly-2022-10-15, commit 1eda0fd7349d, Release)

❯ leanc --version
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-apple-darwin21.6.0
Thread model: posix
InstalledDir: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-15/bin

❯ elan default leanprover/lean4:nightly-2022-10-13
info: using existing install for 'leanprover/lean4:nightly-2022-10-13'
info: default toolchain set to 'leanprover/lean4:nightly-2022-10-13'

  leanprover/lean4:nightly-2022-10-13 unchanged - Lean (version 4.0.0-nightly-2022-10-13, commit 870de844dcc7, Release)

❯ leanc --version
clang version 14.0.0 (https://github.com/llvm/llvm-project 329fda39c507e8740978d10458451dcdb21563be)
Target: arm64-apple-darwin21.6.0
Thread model: posix
InstalledDir: /Users/adrien/.elan/toolchains/leanprover--lean4---nightly-2022-10-13/bin

Mario Carneiro (Oct 25 2022 at 21:27):

Looking at the diff, it seems like there were some relevant CI changes, likely related either the LLVM bump (cc: @Siddharth Bhat) or some cleanup activities (cc: @Sebastian Ullrich)

Julian Berman (Oct 25 2022 at 21:33):

Ones built external to elan work fine in case that's helpful to confirm for diagnosis.

Mario Carneiro (Oct 25 2022 at 21:36):

Does it work if you directly download the nightly that was uploaded by CI?

Mario Carneiro (Oct 25 2022 at 21:37):

I think that's the MacOS aarch64 build here

Sebastian Ullrich (Oct 25 2022 at 21:41):

It looks like I uploaded the wrong arch for LLVM. Unfortunately I can't fix it until next week.

Sebastian Ullrich (Oct 25 2022 at 21:43):

The easiest fix would be to revert the LLVM url for that platform to 14. It's not like we actually depend on 15 right now.

Adrien Champion (Oct 25 2022 at 21:43):

Alright, no worries I have no problem just building lean locally

Mario Carneiro (Oct 25 2022 at 21:45):

We should probably put that hotfix in before the next nightly. I think I see what to change but I have basically no way to test it

Mario Carneiro (Oct 25 2022 at 21:52):

lean4#1778

Adrien Champion (Oct 25 2022 at 22:14):

I'm not sure how to test this for you

Adrien Champion (Oct 25 2022 at 22:14):

Is there an elan command to install from a repo?

Julian Berman (Oct 25 2022 at 22:23):

Given that the archive Mario linked didn't work when directly downloaded (sorry, forgot to confirm "no") probably it's reasonable to test just by downloading that directly and re-checking

Mario Carneiro (Oct 25 2022 at 22:25):

you will have to wait until it is merged and the nightly is run though, since it's a change to the nightly CI script

Mario Carneiro (Oct 25 2022 at 22:25):

unless there is a way to trigger a test version of the nightly build?

Sebastian Ullrich (Oct 25 2022 at 22:39):

There is no separate nightly setup, it's all the same build instructions apart from the version number

Adrien Champion (Oct 26 2022 at 13:01):

Mario Carneiro said:

We should probably put that hotfix in before the next nightly. I think I see what to change but I have basically no way to test it

I confirm that nightly is now fixed :clap:


Last updated: Dec 20 2023 at 11:08 UTC