Update to Lean v4.20.1 and build using system toolchain

.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: |

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:

c/raylib_bindings.c

@@ -2,23 +2,11 @@
 #include <raylib.h>
 #include <resvg.h>
 #include <stdint.h>
+#include <string.h>
+#include <stdlib.h>
 
 #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) {}

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:

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",

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]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.20.1