leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.77k stars 429 forks source link

Invocations of C++ compiler by Lake tests don't pass `-isysroot` on macOS #6296

Closed zwarich closed 8 hours ago

zwarich commented 21 hours ago

Prerequisites

Description

When C++ files are built as part of Lake tests, they do not pass -isysroot to Clang, which causes Clang to be unable to find system libraries.

Steps to Reproduce

  1. Configure Lean's build with cmake --preset release.
  2. Build Lean with make -C build/release -j<N>.
  3. Run tests with make -C build/release test -j<N>.

Expected behavior:

Invocations of the C++ compiler by Lake succeed.

Actual behavior:

The C++ compiler emits errors indicative of an unspecified sysroot, e.g.

2307: trace: .> MACOSX_DEPLOYMENT_TARGET=99.0 /Library/Developer/CommandLineTools/usr/bin/cc -o ././.lake/build/bin/hello ././.lake/build/ir/Main.c.o.export ././.lake/build/ir/Hello.c.o.export -L /Users/zwarich/lean4/build/release/stage1/lib/lean -lleancpp -lInit -lStd -lLean -lleanrt -lc++ -lLake  /opt/homebrew/lib/libgmp.dylib /opt/homebrew/lib/libuv.dylib
2307: info: stderr:
2307: ld: library 'c++' not found

Versions

lean4 d9d54c1f9 macOS Sonoma 14.7.1

zwarich commented 21 hours ago

This appears to be caused by the test Makefiles setting LEAN_CC but not passing the additional flags that leanc would add. Commenting out the line setting LEAN_CC fixes the problem, but I don't know if that's acceptable for all targets. It does look like this change to set LEAN_CC was a few weeks prior to the creation of leanc, so maybe it's no longer necessary?