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

Use LEAN_CC=clang lake for builds on linux. #11

Closed
wants to merge 2 commits into from

Conversation

paulcadman
Copy link
Owner

The LEAN_CC variable was introduced recently to use override the bundled clang (leanc) from the lean toolchain.

leanprover/lean4#4477 (comment)

We must use LEAN_CC on linux because the example executable will fail to link if raylib is built with a glibc that's incompatible with the version that's bundled with leanc. This currently happens with the arch distro.

Thanks to @keeganperry7 for figuring this out.

In addition to installing clang we needed to install:

Arch

libc++

Debian / Ubuntu

libc++-dev, libgmp-dev, libc++abi-dev

paulcadman and others added 2 commits August 18, 2024 12:17
The LEAN_CC variable was introduced recently to use override the bundled
clang (leanc) from the lean toolchain.

leanprover/lean4#4477 (comment)

We must use LEAN_CC on linux because the example executable will fail to
link if raylib is built with a glibc that's incompatible with the version
that's bundled with leanc. This currently happens with the arch distro.

Thanks to @keeganperry7 for figuring this out.

Co-authored-by: keeganperry7 <keegan.perry.kp@gmail.com>
@paulcadman
Copy link
Owner Author

paulcadman commented Oct 27, 2024

just forwards environment variables to shell commands, so you can run:

LEAN_CC=clang just build

to set the LEAN_CC environment variable for the lake build.

I'd prefer to do it this way instead of setting LEAN_CC for all linux builds because the 'standard' (and fully tested / supported) lake invocation works for some (e.g ubuntu / debian) distributions.

What remains is to document that the LEAN_CC workaround may help if you see glibc linker errors in the README.

@paulcadman paulcadman closed this Oct 27, 2024
@paulcadman paulcadman deleted the use-LEAN_CC-in-linux-builds branch October 27, 2024 12:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants