elan toolchains broken on macos M1

Stream: lean4

[Adrien Champion]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I think that's the MacOS aarch64 build here

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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]

lean4#1778

[Adrien Champion]

I'm not sure how to test this for you

[Adrien Champion]

Is there an elan command to install from a repo?

[Julian Berman]

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]

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]

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

[Sebastian Ullrich]

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

[Adrien Champion]

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: