Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
1 task done
zwarich opened this issue Dec 3, 2024 · 1 comment · Fixed by #6297
Closed
1 task done

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

zwarich opened this issue Dec 3, 2024 · 1 comment · Fixed by #6297
Labels
bug Something isn't working

Comments

@zwarich
Copy link
Contributor

zwarich commented Dec 3, 2024

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 d9d54c1
macOS Sonoma 14.7.1

@zwarich zwarich added the bug Something isn't working label Dec 3, 2024
@zwarich
Copy link
Contributor Author

zwarich commented Dec 3, 2024

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant