Update to Lean v4.20.1 and build using system toolchain#53
Merged
paulcadman merged 6 commits intofunexists:mainfrom Jun 28, 2025
Merged
Update to Lean v4.20.1 and build using system toolchain#53paulcadman merged 6 commits intofunexists:mainfrom
paulcadman merged 6 commits intofunexists:mainfrom
Conversation
Previously we used the bundled lean clang toolchain to build native objects (e.g raylib_bindings.o, libleanffi.a, raylean executable). This causes problems because we link with raylib.a which is build by the system toolchain. There can be linking errors caused by the lean toolchain and the system toolchain linking against different libraries, e.g glibc. This changes uses the LEAN_CC feature of lake to build lean native objects using the system toolchain. So both the lean and the raylib native objects are built using the same toolchain. The system toolchain needs to be able to find the system libgmp and libuv to link the lean executable. These are now passed using the LIBRARY_PATH variable in `lake build`. On macOS these can be installed using: ``` brew install gmp brew install libuv ``` The Just file constructs the LIBRARY_PATH using `brew --prefix`. On linux the system toolchain may already be able to find libgmp and libuv (when they're installed using a distro package manager for example). If not then the user must set the `library_path` variable when running the justfile.
paulcadman
force-pushed
the
lean-update-v4.20
branch
3 times, most recently
from
634b222 to
302e59a
Compare
paulcadman
force-pushed
the
lean-update-v4.20
branch
from
302e59a to
ae405ab
Compare
|
|
||
| #### [libgmp](https://gmplib.org) and [libuv](https://libuv.org) | ||
|
|
||
| These are requried to link lean executables. |
Collaborator
There was a problem hiding this comment.
requried -> required
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR:
You must now install
gmpandlibuvto build the raylean executable. On macOS you can run:Details
Previously we used the bundled lean clang toolchain to build native
objects (e.g raylib_bindings.o, libleanffi.a, raylean executable).
This causes problems because we link with raylib.a which is build by the
system toolchain. There can be linking errors caused by the lean
toolchain and the system toolchain linking against different libraries,
e.g glibc.
This changes uses the LEAN_CC feature of lake to build lean native
objects using the system toolchain. So both the lean and the raylib
native objects are built using the same toolchain.
The system toolchain needs to be able to find the system libgmp and
libuv to link the lean executable.
These are now passed using the LIBRARY_PATH variable in
lake build. On macOS the justfile constructs the LIBRARY_PATH usingbrew --prefix.On linux the system toolchain may already be able to find libgmp and
libuv (when they're installed using a distro package manager for
example). If not then the user must set the
library_pathvariable whenrunning the justfile.