Help Troubleshooting Lean in VisualStudioCode

Stream: new members

[Steven Flynn]

Hello, I am having problems getting Lean working in Visual Studio Code. It worked fine a couple weeks ago. I am using MacOS Monterey 12.6.3.

When I open up an existing project with Lean exercises that I pulled from a git repository the Lean InfoView gave me the error message
"Imports are out of date and must be rebuilt; use the "Restart File" command in your editor."
When I "restart file" in my editor Lean runs indefinitely until my computer crashes.

I updated with

elon self update

And the same problem repeated itself.

Then I uninstalled and reinstalled with

elan toolchain install leanprover/lean4:v4.21.0

I made sure that my defaut was set to the most recent stable version

elan default leanprover/lean4:v4.21.0

Then I opened my Lean project and I still had the same error massage in the Lean InfoView. When I used the "Restart File" command, Lean got stuck in an infinite loop again.

Then I tried creating a new project ( tried both standalone and mathlib). I received an compile error that ended with

Some required builds logged failures:

- Cache.Lean:c.o

- Batteries.Data.Array.Match:c.o

- Batteries.Data.String.Basic:c.o

- Batteries.Data.String.Matcher:c.o

- Cache.IO:c.o

- Cache.Hashing:c.o

- Cache.Requests:c.o

- Cache.Main:c.o

error: build failed

=> Operation failed. Exit code: 1.

After more attempts at uninstalling and reinstalling and many reboots, I have been unable to fix these issues. Any guidance would be appreciated! Also please let me know if any part of this question can be made more clear. Thank you!

[Nicolas Escobar]

I have the same issue, I'd also appreciate some guidance

[Henrik Böving]

Could you show us more of your output? We would need to see why those C files actually fail to compile to figure out what's wrong.

[Steven Flynn]

In Visual Studio Code, I selected New Project -> Create Standalone Project. I called my new project folder Lean2025 and chose the location of my project folds to be Users/stevenflynn. Here is the output:

/Users/stevenflynn/Lean2025> curl --version
curl 7.79.1 (x86_64-apple-darwin21.0) libcurl/7.79.1 (SecureTransport) LibreSSL/3.3.6 zlib/1.2.11 nghttp2/1.45.1
Release-Date: 2021-09-22
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtsp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS GSS-API HSTS HTTP2 HTTPS-proxy IPv6 Kerberos Largefile libz MultiSSL NTLM NTLM_WB SPNEGO SSL UnixSockets

/Users/stevenflynn/Lean2025> git --version
git version 2.50.1

/Users/stevenflynn/Lean2025> elan --version
elan 4.1.2 (58e8d545e 2025-05-26)

/Users/stevenflynn/Lean2025> lean +leanprover/lean4:stable --version
Lean (version 4.21.0, x86_64-apple-darwin22.6.0, commit 6741444a63ee, Release)
/Users/stevenflynn/Lean2025> lake +leanprover/lean4:stable --version
Lake version 5.0.0-6741444 (Lean version 4.21.0)
/Users/stevenflynn/Lean2025> lake +leanprover/lean4:stable init Lean2025
/Users/stevenflynn/Lean2025> lake +leanprover/lean4:stable update
info: Lean2025: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
/Users/stevenflynn/Lean2025> lake +leanprover/lean4:stable build
✔ [2/8] Built Lean2025.Basic
✔ [3/8] Built Lean2025
✔ [4/8] Built Main
✖ [5/8] Building Lean2025.Basic:c.o
trace: .> /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang -c -o /Users/stevenflynn/Lean2025/.lake/build/ir/Lean2025/Basic.c.o.export /Users/stevenflynn/Lean2025/.lake/build/ir/Lean2025/Basic.c -I /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0 -nostdinc -isystem /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[75411]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang' exited with code 134
✖ [6/8] Building Lean2025:c.o
trace: .> /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang -c -o /Users/stevenflynn/Lean2025/.lake/build/ir/Lean2025.c.o.export /Users/stevenflynn/Lean2025/.lake/build/ir/Lean2025.c -I /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0 -nostdinc -isystem /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[75413]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang' exited with code 134
✖ [7/8] Building Main:c.o
trace: .> /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang -c -o /Users/stevenflynn/Lean2025/.lake/build/ir/Main.c.o.export /Users/stevenflynn/Lean2025/.lake/build/ir/Main.c -I /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0 -nostdinc -isystem /Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[75415]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/stevenflynn/.elan/toolchains/leanprover--lean4---v4.21.0/bin/clang' exited with code 134
Some required builds logged failures:
- Lean2025.Basic:c.o
- Lean2025:c.o
- Main:c.o
error: build failed
=> Operation failed. Exit code: 1.

[Sebastian Ullrich]

This appears to be some specific OS version incompatibility. Please note that as a general policy, we cannot support obsolete operating system versions!