libgmp linking error

Stream: lean4

[Anne Baanen]

When running lake exe cache get on Debian Bullseye 5.10.0.22 (2023-04-22), @Freek Wiedijk gets the following error:

ld.lld: error: undefined symbol: __stack_chk_guard
referenced by [many functions] in archive ~/.elan/toolchains/[leanprover_lean4-etc]/lib/libgmp.a

We tried adding -lssp_nonshared and -fstack-protector to the extraLinkArgs in the Lakefile, with no success.

Doesn't Lean get built for Debian anyway?

[Sebastian Ullrich]

Is this x86 or ARM?

[Anne Baanen]

This is Debian x86_64 in Parallels, on an ARM Mac.

[Matthew Ballard]

Related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Docker.20Images.20on.20ARM :eyes:

[Sebastian Ullrich]

Hmm, hopefully the architecture of the host should not be relevant here. We should probably run the linker cmdline with -v -y __stack_chk_guard on a working and non-working system but I don't have access to a standard (non-NixOS) Linux system right now

[Mario Carneiro]

I have a standard linux setup to test with if you need. I get the following, when linking hello world:

@[default_target]
lean_exe test where
  root := `Test
  moreLinkArgs := #["-v", "-y", "__stack_chk_guard"]

$ lake build
[2/2] Linking test
error: > /home/mario/Documents/lean/lean4/build/release/stage1/bin/leanc -o ./build/bin/test ./build/ir/Test.o -v -y __stack_chk_guard
error: stderr:
cc -I /home/mario/Documents/lean/lean4/build/release/stage1/include -fstack-clash-protection -fPIC -fvisibility=hidden -o ./build/bin/test ./build/ir/Test.o -v -y __stack_chk_guard -L /home/mario/Documents/lean/lean4/build/release/stage1/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lstdc++ /usr/lib/x86_64-linux-gnu/libgmp.so -lm -ldl -pthread -Wno-unused-command-line-argument
Using built-in specs.
COLLECT_GCC=cc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/11/lto-wrapper
OFFLOAD_TARGET_NAMES=nvptx-none:amdgcn-amdhsa
OFFLOAD_TARGET_DEFAULT=1
cc: error: unrecognized command-line option ‘-y’
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu 11.3.0-1ubuntu1~22.04.1' --with-bugurl=file:///usr/share/doc/gcc-11/README.Bugs --enable-languages=c,ada,c++,go,brig,d,fortran,objc,obj-c++,m2 --prefix=/usr --with-gcc-major-version-only --program-suffix=-11 --program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --libdir=/usr/lib --enable-nls --enable-bootstrap --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new --enable-gnu-unique-object --disable-vtable-verify --enable-plugin --enable-default-pie --with-system-zlib --enable-libphobos-checking=release --with-target-system-zlib=auto --enable-objc-gc=auto --enable-multiarch --disable-werror --enable-cet --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic --enable-offload-targets=nvptx-none=/build/gcc-11-aYxV0E/gcc-11-11.3.0/debian/tmp-nvptx/usr,amdgcn-amdhsa=/build/gcc-11-aYxV0E/gcc-11-11.3.0/debian/tmp-gcn/usr --without-cuda-driver --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu --with-build-config=bootstrap-lto-lean --enable-link-serialization=2
Thread model: posix
Supported LTO compression algorithms: zlib zstd
gcc version 11.3.0 (Ubuntu 11.3.0-1ubuntu1~22.04.1)
error: external command `/home/mario/Documents/lean/lean4/build/release/stage1/bin/leanc

[Sebastian Ullrich]

Could you test with an official release? Yours doesn't use lld

[Mario Carneiro]

$ lake +leanprover/lean4:nightly-2023-07-01 build
[0/2] Building Test
[2/2] Linking test
error: > /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/bin/leanc -o ./build/bin/test ./build/ir/Test.o -v -y __stack_chk_guard
error: stderr:
/home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/bin/clang -I /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/include -fstack-clash-protection -fPIC -fvisibility=hidden -nostdinc -isystem /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/include/clang -o ./build/bin/test ./build/ir/Test.o -v -y __stack_chk_guard -L /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib -L /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -Wl,--as-needed -lgmp -Wl,--no-as-needed -lm -ldl -pthread -Wno-unused-command-line-argument
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-unknown-linux-gnu
Thread model: posix
InstalledDir: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/bin
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/11
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/12
Found candidate GCC installation: /usr/lib/gcc/x86_64-linux-gnu/9
Selected GCC installation: /usr/lib/gcc/x86_64-linux-gnu/12
Candidate multilib: .;@m64
Selected multilib: .;@m64
clang: error: no such file or directory: '__stack_chk_guard'
error: external command `/home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/bin/leanc` exited with code 1

[Floris van Doorn]

On @Freek Wiedijk's laptop we also get

clang: error: no such file or directory: '__stack_chk_guard'

[Sebastian Ullrich]

I don't even see any reference to __stack_chk_guard on x64 Linux outside of LLVM (which could be from its ARM backend)

$  nm /home/vscode/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a  | grep __stack_chk_guard
nm: mp_clz_tab.o: no symbols
nm: repl-vsnprintf.o: no symbols
$ grep -R __stack_chk_guard  /home/vscode/.elan/toolchains/leanprover--lean4---nightly-2023-06-20
grep: /home/vscode/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libLLVM-15.so: binary file matches
grep: /home/vscode/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libLLVM-15.0.1.so: binary file matches
grep: /home/vscode/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libLLVM.so: binary file matches

[Sebastian Ullrich]

Could you try this one?

leanc -o ./build/bin/cache ./build/ir/Util/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -Wl,-y,__stack_chk_guard -Wl,--verbose

[Mario Carneiro]

That works for me on a "normal" linux x86 system:

lakefile:

...
lean_exe test where
  root := `Test
  moreLinkArgs := #["-Wl,-y,__stack_chk_guard", "-Wl,--verbose"]

output:

$ lake +leanprover/lean4:nightly-2023-07-01 build
[0/2] Building Test
stdout:
./././Test.lean:3:0: warning: using 'exit' to interrupt Lean
[1/2] Compiling Test
[2/2] Linking test
stderr:
ld.lld: /lib/x86_64-linux-gnu/Scrt1.o
ld.lld: /lib/x86_64-linux-gnu/crti.o
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/clang_rt.crtbegin.o
ld.lld: ./build/ir/Test.o
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libc_nonshared.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/libgmp.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/libunwind.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/lean/libleancpp.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/lean/libLean.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/lean/libInit.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/lean/libleanrt.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/libc++.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/libc++abi.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/libgmp.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libm.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libdl.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/libclang_rt.builtins.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libc.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/libclang_rt.builtins.a
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/clang/15.0.1/lib/x86_64-unknown-linux-gnu/clang_rt.crtend.o
ld.lld: /lib/x86_64-linux-gnu/crtn.o
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libdl.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/librt.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so
ld.lld: /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-07-01/lib/glibc/libpthread.so

[Freek Wiedijk]

[4/4] Linking hello
error: > /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/leanc -o ./build/bin/hello ./build/ir/Main.o ./build/ir/Hello.o -Wl,-y,__stack_chk_guard -Wl,--verbose
error: stdout:
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt43-set_str.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(sqr.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(sqr_basecase.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(nussbaumer_mul.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(mul_fft.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(mul_n.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt82-mul.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(toom42_mul.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(toom53_mul.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt89-set_str.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt31-mul.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(tdiv_q.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(div_q.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(mu_div_q.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(invertappr.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(dcpi1_div_qr.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(dcpi1_divappr_q.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(dcpi1_div_q.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(tdiv_r.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt99-tdiv_qr.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(n_pow_ui.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(and.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(ior.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(xor.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(gcd.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt97-gcd.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(hgcd.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(hgcd_reduce.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(hgcd_appr.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(hgcd_matrix.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(hgcd_step.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(mod_1.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt20-get_str.o): reference to __stack_chk_guard
/home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a(lt88-get_str.o): reference to __stack_chk_guard
error: stderr:
ld.lld: /lib/aarch64-linux-gnu/Scrt1.o
ld.lld: /lib/aarch64-linux-gnu/crti.o
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/clang/15.0.1/lib/aarch64-unknown-linux-gnu/clang_rt.crtbegin.o
ld.lld: ./build/ir/Main.o
ld.lld: ./build/ir/Hello.o
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libc_nonshared.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libunwind.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/lean/libleancpp.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/lean/libLean.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/lean/libInit.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/lean/libleanrt.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libc++.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libc++abi.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libm.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libdl.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/clang/15.0.1/lib/aarch64-unknown-linux-gnu/libclang_rt.builtins.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libc.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/clang/15.0.1/lib/aarch64-unknown-linux-gnu/libclang_rt.builtins.a
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/clang/15.0.1/lib/aarch64-unknown-linux-gnu/clang_rt.crtend.o
ld.lld: /lib/aarch64-linux-gnu/crtn.o
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libdl.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/librt.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/glibc/libpthread.so
ld.lld: error: undefined symbol: __stack_chk_guard
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/lib/libgmp.a
>>> referenced by lt43-set_str.o:(__gmpz_set_str) in archive /home/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/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/freek/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/leanc` exited with code 1

[Sebastian Ullrich]

Ok, so this one is ARM

[Sebastian Ullrich]

I would suspect that compiling Lean binaries on ARM Linux has never worked in the first place especially since the only user I know of, @Gabriel Ebner, was probably not affected because of differences in using elan sourced from Nixpkgs

[Julian Berman]

The point is "via elan specifically" right? -- I've definitely compiled Lean 4 on ARM Linux before (my Android phone -- though I haven't been able recently to figure out how to fix an error which is different from the one being discussed here, it has to do with fPIC, and I fixed it before but can't remember what I did).

[Sebastian Ullrich]

The point is "official release", as above

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/2319

[Matthew Ballard]

I think I live without all my RPi bignum computation :lol:

[Gabriel Ebner]

Sebastian Ullrich said:

I would suspect that compiling Lean binaries on ARM Linux has never worked in the first place especially since the only user I know of, Gabriel Ebner, was probably not affected because of differences in using elan sourced from Nixpkgs

To be completely honest, I only worked on the ARM port because I was planning to get a Linux ARM laptop "designed in California" but that never happened. In particular, I'm not sure if I've ever even tried to compile a native binary with the ARM build. At that time, mathlib didn't require any native binaries.

[Sebastian Ullrich]

Not that it should really be required for cache either :)

[Mario Carneiro]

Actually, it would be great if there was a way to run lake scripts using the interpreter... @Mac ?

[Mac Malone]

Mario Carneiro That is what scripts / lake run is for. If you want to run a Lean file, you can use the usual Lean mechanisms in a script to do so (e.g., runFrontend). I do plan to add some helpers to do so easier soon.

[Mario Carneiro]

@Mac lake run cache get doesn't work though

[Mac Malone]

@Mario Carneiro That is because cache is an executable not a script? If you want to run cache from the interpreter, you need to interpret the main module from a script (e.g., with runFrontend).

[Mario Carneiro]

I feel like this should just work out of the box

[Mario Carneiro]

that is, you can just run any lake_exe from the interpreter with an appropriate invocation

[Mac Malone]

@Mario Carneiro It is worth noting that this is not possible with all kinds of lean_exe targets. For example, if the executable needs to be linked to certain system libraries.

[Mac Malone]

However, I do think this this a feasible feature request (maybe via lake exe -I cache get?)