diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index eacaca8..0026df4 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 @@ -52,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 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: | 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 41c579b..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) { @@ -66,7 +54,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 +98,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/justfile b/justfile index 068369d..8a01c63 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 { "clang" } + 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: 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