Installation issues with clang on old Macbook air

Stream: lean4

[Floris van Doorn]

A student has trouble getting Lean to work on an old Macbook air.
Downloading the Mathlib cache within the VSCode extension fails with the error "this is not a project depending on Mathlib" (it is), and in the command line it gives the output below. I also added the setup information output.

MacBook-Air-5:LeanCourse javier.duran$ lake exe cache get
✖ [9/19] Building Batteries.Data.Array.Match:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2614]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [10/19] Building Batteries.Data.String.Basic:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2615]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [11/19] Building Batteries.Data.String.Matcher:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Matcher.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Matcher.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2618]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [12/19] Building Cache.Lean:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2616]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [13/19] Building Cache.IO:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/IO.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/IO.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2617]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [16/19] Building Cache.Main:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Main.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Main.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2621]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [17/19] Building Cache.Hashing:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2619]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
✖ [18/19] Building Cache.Requests:c.o
trace: .> /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang -c -o /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Requests.c.o.export /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/.lake/packages/mathlib/.lake/build/ir/Cache/Requests.c -I /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0 -nostdinc -isystem /Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[2620]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/javier.duran/.elan/toolchains/leanprover--lean4---v4.24.0/bin/clang' exited with code 134
Some required targets logged failures:
- Batteries.Data.Array.Match:c.o
- Batteries.Data.String.Basic:c.o
- Batteries.Data.String.Matcher:c.o
- Cache.Lean:c.o
- Cache.IO:c.o
- Cache.Main:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o
error: build failed
(base) MacBook-Air-5:LeanCourse javier.duran$

[Floris van Doorn]

**Operating system**: Darwin (release: 21.6.0)
**CPU architecture**: x64
**CPU model**: 4 x Intel(R) Core(TM) i5-5250U CPU @ 1.60GHz
**Available RAM**: 8.59 GB

**VS Code version**: Reasonably up-to-date (version: 1.100.2)
**Lean 4 extension version**: 0.0.216
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.1.2)
**Lean**: Reasonably up-to-date (version: 4.24.0)
**Project**: Valid Lean project (path: /Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse)
**Active Lean version**: leanprover/lean4:v4.24.0 (set by `file:///Users/javier.duran/Documents/MatheBonn/PhD/LeanCourse/lean-toolchain`)
**Installed Lean versions**: leanprover/lean4:v4.21.0, leanprover/lean4:v4.24.0

[Sebastian Ullrich]

This is macOS Monterey? Unfortunately it is infeasible for us to support OS versions not even supported by the OS manufacturer anymore

[Sebastian Ullrich]

(https://lean-lang.org/doc/reference/latest/platforms/Tier-1/#The-Lean-Language-Reference--Supported-Platforms--Tier-1)

[Floris van Doorn]

Yes, that seems to be the case, thanks for checking!
Does it make sense to add a message "this OS is not officially supported, so errors may occur" to the "Show Setup Information" popup?

[Sebastian Ullrich]

We were discussing that just now but it's not completely trivial as the information depends on the Lean version

[Marc Huisinga]

We can add a warning in the extension for the current minimum required OS versions of the last Lean 4 release.