Failure to build with glibc 2.26 on Amazon Cloud Desktop

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

(asked customer to test repro on nightly)

Description

AWS lean user @seanmcl reports inability to build any lean target on Amazon-internal cloud desktop (which has glibc 2.26) due to glibc version incompatibility.

Context

We assert in the reference manual that "x86-64 Linux with glibc 2.26+" is a Tier 1 supported platform. Lean's own execution appears to work fine, up to generation of C code, but errors arise when trying to compile the generated C with the clang shipped with lean. If we mean only to promise that Lean itself works on glibc 2.26, then maybe we should close this issue as "working as intended" and update the docs to reflect that the user may need to bring their own C compiler if they're on such an old glibc.

Steps to Reproduce

1. Create a new lean project, e.g. with lake new ProjectName
2. lake build ProjectName

Expected behavior:

Successful compilation.

Actual behavior:

/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libclang-cpp.so.19.1)
/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.27' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libLLVM.so.19.1)
/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libLLVM.so.19.1)

In fact, one can reproduce this error without invoking lake as well, by directly invoking the lean-distributed clang:

$ /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang --version
/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libclang-cpp.so.19.1)
/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.27' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libLLVM.so.19.1)
/local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/clang: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /local/home/seanmcl/.elan/toolchains/leanprover--lean4---v4.26.0/bin/../lib/libLLVM.so.19.1)

We saw repro on lean v4.18.0 as well, (with the minor variation that error messages about only GLIBC_2.27 and not GLIBC_2.29 appeared) which was to my knowledge the first version of lean that claimed to work with 2.26, as a result of #7037.

It would be desirable to find a repro on, e.g. some docker image that's on glibc 2.26 so that we don't have to go through customer for repro.

Versions

$ cat /etc/os-release
NAME="Amazon Linux"
VERSION="2"
ID="amzn"
ID_LIKE="centos rhel fedora"
VERSION_ID="2"
PRETTY_NAME="Amazon Linux 2"
ANSI_COLOR="0;33"
CPE_NAME="cpe:2.3:o:amazon:amazon_linux:2:-:internal"
HOME_URL="https://amazonlinux.com/"
VARIANT="internal"

Start by reproducing the failure with the distributed clang, first via clang --version and then with lake build ProjectName, on a glibc 2.26 environment such as Amazon Linux 2. Compare the behavior with the Tier 1 platform claim and the history around #7037. Done means determining whether the Lean toolchain supports this platform or documenting the limitation clearly.