Docker Images on ARM

Stream: lean4

[Andrés Goens]

Has anyone built a docker container with Lean4 yet? I'm trying to do that and I'm getting a linker error:

Linking test
error: > /home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-01/bin/leanc -o ./build/bin/test ./build/ir/Main.o ./build/ir/Test.o
error: stderr:
ld.lld: error: undefined symbol: __stack_chk_guard
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-01/lib/libgmp.a
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-01/lib/libgmp.a
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-01/lib/libgmp.a
>>> referenced 125 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-01/bin/leanc` exited with code 1

This happens every time I try to compile something (even a newly lake inited project). Does anyone have a clue what might be happening?

[Andrés Goens]

for reference, this is on Linux on ARM:

user@984b050c5996:~/test$ uname -a
Linux 984b050c5996 5.15.49-linuxkit #1 SMP PREEMPT Tue Sep 13 07:51:32 UTC 2022 aarch64 aarch64 aarch64 GNU/Linux

[Alexander Bentkamp]

This works well for me: https://github.com/leanprover-community/lean4web/blob/main/server/lean.Dockerfile

[Yaël Dillies]

@Eric Wieser, you sorted one out for mathlib4, right?

[Andrés Goens]

yeah it seems to be ARM specific, on x86 it works for me as well

[Andrés Goens]

(edited the title)

[Eric Wieser]

Yaël Dillies said:

Eric Wieser, you sorted one out for mathlib4, right?

Yes, it's what the gitpod setup for mathlib 4 uses

[Matthew Ballard]

Has anyone got past this on ARM? I'm guessing I have to pass a flag to clang to disable stack protection. Can this be done with lake build or do I need to do something else?