From a740c2c1b3e2ec85ad65396728346f03b6eabf6c Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 18:16:52 +0100 Subject: [PATCH 1/6] Update to lean v4.20.1 --- c/raylib_bindings.c | 4 ++-- lake-manifest.json | 4 ++-- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c index 41c579b..96e47d2 100644 --- a/c/raylib_bindings.c +++ b/c/raylib_bindings.c @@ -66,7 +66,7 @@ static lean_external_class *raylib_texture2d_class = NULL; // collected static void raylib_texture2d_finalizer(void *texture2d) { UnloadTexture(*(Texture2D *)texture2d); - lean_free_small(texture2d); + lean_free_small_object((lean_object*)texture2d); } static void raylib_texture2d_foreach(void *mod, b_lean_obj_arg fn) {} @@ -110,7 +110,7 @@ static lean_external_class *raylib_image_class = NULL; // The finalizer is run by the lean runtime when an Image is garbage collected static void raylib_image_finalizer(void *image) { UnloadImage(*(Image *)image); - lean_free_small(image); + lean_free_small_object((lean_object*)image); } static void raylib_image_foreach(void *mod, b_lean_obj_arg fn) {} diff --git a/lake-manifest.json b/lake-manifest.json index 65d86fd..0ae14c7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.20.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "raylean", diff --git a/lakefile.lean b/lakefile.lean index 7dca30b..6987fda 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,7 @@ def optionUseBundle : Bool := get_config? bundle == some "on" def optionDisableResvg : Bool := get_config? resvg == some "disable" -require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.14.0" +require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.20.0" require «lens-demo» from git "https://github.com/funexists/lens-demo.git" @ "c0121c73d85ae3539add5b69b3345123ac4606e1" @@ -51,4 +51,4 @@ target raylib_bindings.o pkg : FilePath := do extern_lib libleanffi pkg := do let ffiO ← raylib_bindings.o.fetch let name := nameToStaticLib "rayliblean" - buildStaticLib (pkg.nativeLibDir / name) #[ffiO] + buildStaticLib (pkg.staticLibDir / name) #[ffiO] diff --git a/lean-toolchain b/lean-toolchain index 401bc14..78adacd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 \ No newline at end of file +leanprover/lean4:v4.20.1 From 7369ce49bf9d1f712aead68b8778e3391cdf73a5 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 18:53:28 +0100 Subject: [PATCH 2/6] Use system toolchain to build lean native objects 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. --- README.md | 14 ++++++++++++++ c/raylib_bindings.c | 16 ++-------------- justfile | 24 +++++++++++++++++++----- 3 files changed, 35 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index bf50089..dfc4913 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,8 @@ Raylean has several dependencies: * [Just](https://github.com/casey/just), as a replacement for Make. * XCode for macOS SDK frameworks like OpenGL. * [Rust](https://www.rust-lang.org/) for building resvg, which provides SVG support. +* [libgmp](https://gmplib.org), required to link lean executables +* [libuv](https://libuv.org), requried to link lean executables You need to install all four to build Raylean. Below follows instructions for each. @@ -53,6 +55,18 @@ curl https://sh.rustup.rs -sSf | sh Or use the [official documentation](https://www.rust-lang.org/tools/install) to setup Rust. + +#### [libgmp](https://gmplib.org) and [libuv](https://libuv.org) + +These are requried to link lean executables. + +Install using [Homebrew](https://brew.sh) with: + +``` sh +brew install gmp +brew install libuv +``` + ### Build and Run To build the raylib static library and the demo executable, run the following command in the project: diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c index 96e47d2..96edeb1 100644 --- a/c/raylib_bindings.c +++ b/c/raylib_bindings.c @@ -2,23 +2,11 @@ #include #include #include +#include +#include #define IO_UNIT (lean_io_result_mk_ok(lean_box(0))) -// leanc doesn't provide stdlib.h -void *memcpy(void *, const void *, size_t); -void *malloc(size_t); -void *calloc(size_t, size_t); - -// leanc doesn't provide string.h -int strcmp(const char *s1, const char *s2) { - while (*s1 && (*s1 == *s2)) { - s1++; - s2++; - } - return *(const unsigned char *)s1 - *(const unsigned char *)s2; -} - #ifdef RAYLEAN_NO_BUNDLE void bundle_free_resource(void *data) { diff --git a/justfile b/justfile index 068369d..9264fa1 100644 --- a/justfile +++ b/justfile @@ -10,6 +10,9 @@ disableResvg := '' # just disableBundle=yes build disableBundle := '' +# set to the C compiler used to build native libraries (e.g raylib CC, and lake LEAN_CC) +native_compiler := if os() == "macos" { "/usr/bin/clang" } else { "gcc" } + lake_bundle_config_opt := if disableBundle == "" { "-K bundle=on" } else { "" } lake_resvg_config_opt := if disableResvg == "" { "" } else { "-K resvg=disable" } @@ -37,14 +40,25 @@ raylib_config_flags := "" # Raylib CUSTOM_CFLAGS make parameter raylib_custom_cflags := raylib_config_flags + " " + raylib_os_custom_cflags -# Raylib CC make paramter -raylib_cc_parameter := if os() == "macos" { "/usr/bin/clang" } else { "gcc" } - # Raylib extra Makefile variables # # e.g add "USE_WAYLAND_DISPLAY=TRUE" to build Raylib with Wayland support. raylib_extra_make_variables := "" +# The path to the GMP library root +# +# On macOS use `brew install gmp` to install it +gmp_prefix := if os() == "macos" { shell("brew --prefix gmp") } else { "" } + +# The path to libuv root +# +# On macOS use `brew install libuv` to install it +libuv_prefix := if os() == "macos" { shell("brew --prefix libuv") } else { "" } + +# The value of LIBRARY_PATH used when running `just build`. This is passed to +# the C compiler when lake builds native objects. +library_path := if gmp_prefix == "" { "" } else if libuv_prefix == "" { "" } else {gmp_prefix + "/lib:" + libuv_prefix + "/lib"} + static_lib_path := join(justfile_directory(), "lib") raylib_src_path := join(justfile_directory(), "raylib-5.0", "src") resource_dir := join(justfile_directory(), "resources") @@ -86,7 +100,7 @@ build_raylib: if [ ! -f "{{static_lib_path}}/libraylib.a" ]; then mkdir -p {{static_lib_path}} make -C {{raylib_src_path}} \ - CC={{raylib_cc_parameter}} \ + CC={{native_compiler}} \ PLATFORM=PLATFORM_DESKTOP \ RAYLIB_LIBTYPE=STATIC \ RAYLIB_RELEASE_PATH={{static_lib_path}} \ @@ -96,7 +110,7 @@ build_raylib: # build both the raylib library and the Lake project build: build_resvg build_raylib bundler - lake -R {{lake_config_opts}} build + LIBRARY_PATH={{library_path}} LEAN_CC={{native_compiler}} lake -R {{lake_config_opts}} build # clean only the Lake project clean: From 2b4e8d9a1a063d36fb4376321094d9132b0b2ed4 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 19:07:57 +0100 Subject: [PATCH 3/6] Install gmp, libuv in the github build --- .github/workflows/build.yaml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index eacaca8..a044420 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -28,6 +28,11 @@ jobs: - name: query clang run: clang --version + - name: install libgmp, libuv + run: | + brew install gmp + brew install libuv + - uses: actions/checkout@v4 - name: build project From ae405ab39d7a8b2d4b925314cb8a0bf28c26b97a Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 19:14:32 +0100 Subject: [PATCH 4/6] Add libuv1 and libc++ to ubuntu build deps --- .github/workflows/build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index a044420..c78128d 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -57,7 +57,7 @@ jobs: run: rustup toolchain install stable --profile minimal - name: Install raylib deps - run: sudo apt-get install -y --no-install-recommends libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev + run: sudo apt-get install -y --no-install-recommends libc++abi-dev libc++-dev libuv1-dev libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev - name: install elan run: | From 69e918953250f9fe308d4be3115101ce7285e8f2 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 19:25:52 +0100 Subject: [PATCH 5/6] Use clang on linux --- justfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/justfile b/justfile index 9264fa1..8a01c63 100644 --- a/justfile +++ b/justfile @@ -11,7 +11,7 @@ disableResvg := '' disableBundle := '' # set to the C compiler used to build native libraries (e.g raylib CC, and lake LEAN_CC) -native_compiler := if os() == "macos" { "/usr/bin/clang" } else { "gcc" } +native_compiler := if os() == "macos" { "/usr/bin/clang" } else { "clang" } lake_bundle_config_opt := if disableBundle == "" { "-K bundle=on" } else { "" } From b05db76e5b437dfb3f8e9e5664c39a0d92a7f20c Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Sat, 28 Jun 2025 19:29:01 +0100 Subject: [PATCH 6/6] Remove libc++abi-dev libc++-dev linux dependencies in CI --- .github/workflows/build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index c78128d..0026df4 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -57,7 +57,7 @@ jobs: run: rustup toolchain install stable --profile minimal - name: Install raylib deps - run: sudo apt-get install -y --no-install-recommends libc++abi-dev libc++-dev libuv1-dev libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev + run: sudo apt-get install -y --no-install-recommends libuv1-dev libglfw3 libglfw3-dev libx11-dev libxcursor-dev libxrandr-dev libxinerama-dev libxi-dev libxext-dev libxfixes-dev libwayland-dev libxkbcommon-dev - name: install elan run: |