Merge pull request #3 from ValorZard/main

changes to base repo to make it portable

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "SDL"]
+	path = vendor/SDL
+	url = https://github.com/libsdl-org/SDL.git
+[submodule "SDL_image"]
+	path = vendor/SDL_image
+	url = https://github.com/libsdl-org/SDL_image.git

Engine.lean

@@ -166,20 +166,22 @@ partial def gameLoop (engineState : IO.Ref EngineState) : IO Unit := do
     gameLoop engineState
 
 partial def run : IO Unit := do
-  unless (← SDL.init SDL.SDL_INIT_VIDEO) == 0 do
+  unless (← SDL.init SDL.SDL_INIT_VIDEO) == 1 do
     IO.println "Failed to initialize SDL"
     return
 
-  unless (← SDL.createWindow "LeanDoomed" 100 100 SCREEN_WIDTH SCREEN_HEIGHT SDL.SDL_WINDOW_SHOWN) != 0 do
+  unless (← SDL.createWindow "LeanDoomed" SCREEN_WIDTH SCREEN_HEIGHT SDL.SDL_WINDOW_SHOWN) != 0 do
     IO.println "Failed to create window"
     SDL.quit
     return
 
-  unless (← SDL.createRenderer 4294967295 SDL.SDL_RENDERER_ACCELERATED) != 0 do
+
+  unless (← SDL.createRenderer ()) != 0 do
     IO.println "Failed to create renderer"
     SDL.quit
     return
 
+
   let initialState : EngineState := {
     deltaTime := 0.0, lastTime := 0, running := true,
     camera := { x := 1.5, y := 1.5, angle := 0.0 },

README.md

@@ -1,16 +1,37 @@
-# Lean SDL2 Bindings Example
+# Lean SDL3 Bindings Example
 
-Playing around with SDL2 bindings in Lean4 to learn about the FFI.
+Playing around with SDL3 bindings in Lean4 to learn about the FFI.
 
 Simple real-time Doom-style raycasting engine in Lean4:
 
 ![Screenshot](screenshots/screenshot1.png)
 
+## Cloning
+
+When you clone, MAKE SURE YOU RUN ``git submodule update --init --recursive`` IN THE ROOT OF THIS REPOSITORY JUST TO BE SAFE
+
 ## Run
 
-This is just an experiment and the build is currently specific to my system (Ubuntu 24.04.2).
+This is just an experiment
 
-**You need to install dependencies and adjust paths in lakefile.lean!**
+First, make sure you've set up Lean properly on your computer.
+
+If you are on Windows, use MSYS2 or WSL 
+
+IMPORTANT: FOR MSYS2, MAKE SURE YOU ARE USING THE "CLANG" SHELL TO RUN EVERYTHING
+
+(For more information on MSYS2, see: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md)
+
+Follow the "legacy" instructions from here (They should work on Linux, WSL, and MSYS2): https://leanprover-community.github.io/install/linux.html
+
+Second, make sure you run the build script first to build all the dependencies to get this to work
+
+```bash
+chmod +x ./build_sdl_and_friends.sh
+sudo ./build_sdl_and_friends.sh
+```
+
+Then you can run the game proper
 
 ```bash
 lake exe LeanDoomed

SDL.lean

@@ -21,10 +21,10 @@ opaque init : UInt32 → IO UInt32
 opaque quit : IO Unit
 
 @[extern "sdl_create_window"]
-opaque createWindow : String → Int32 → Int32 → Int32 → Int32 → UInt32 → IO UInt32
+opaque createWindow : String → Int32 → Int32 → UInt32 → IO UInt32
 
 @[extern "sdl_create_renderer"]
-opaque createRenderer : UInt32 → UInt32 → IO UInt32
+opaque createRenderer : Unit → IO UInt32
 
 @[extern "sdl_set_render_draw_color"]
 opaque setRenderDrawColor : UInt8 → UInt8 → UInt8 → UInt8 → IO Int32

build_sdl_and_friends.sh

@@ -0,0 +1,6 @@
+cd vendor/SDL
+cmake -S . -B build
+cmake --build build
+cd ../SDL_image
+cmake -S . -B build -DSDL3_DIR=../SDL/build
+cmake --build build

c/sdl.c

@@ -1,15 +1,15 @@
 #include <stdint.h>
-#include <SDL2/SDL.h>
-#include <SDL2/SDL_image.h>
+#include <SDL3/SDL.h>
+#include <SDL3_image/SDL_image.h>
 #include <lean/lean.h>
 
 static SDL_Window* g_window = NULL;
 static SDL_Renderer* g_renderer = NULL;
 
 uint32_t sdl_get_version(void) {
-    SDL_version compiled;
-    SDL_VERSION(&compiled);
-    return compiled.major * 100 + compiled.minor * 10 + compiled.patch;
+    // from https://wiki.libsdl.org/SDL3/SDL_GetVersion
+    const int linked = SDL_GetVersion();  /* reported by linked SDL library */
+    return SDL_VERSIONNUM_MAJOR(linked) * 100 + SDL_VERSIONNUM_MINOR(linked) * 10 + SDL_VERSIONNUM_MICRO(linked);
 }
 
 lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
@@ -30,25 +30,24 @@ lean_obj_res sdl_quit(lean_obj_arg w) {
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-lean_obj_res sdl_create_window(lean_obj_arg title, uint32_t x, uint32_t y, uint32_t w, uint32_t h, uint32_t flags, lean_obj_arg world) {
+lean_obj_res sdl_create_window(lean_obj_arg title, uint32_t w, uint32_t h, uint32_t flags, lean_obj_arg world) {
     const char* title_str = lean_string_cstr(title);
-    g_window = SDL_CreateWindow(title_str, (int)x, (int)y, (int)w, (int)h, flags);
+    g_window = SDL_CreateWindow(title_str, (int)w, (int)h, flags);
     if (g_window == NULL) {
         return lean_io_result_mk_ok(lean_box(0));
     }
     return lean_io_result_mk_ok(lean_box(1));
 }
 
-lean_obj_res sdl_create_renderer(uint32_t index_unsigned, uint32_t flags, lean_obj_arg w) {
+lean_obj_res sdl_create_renderer(lean_obj_arg w) {
     if (g_window == NULL) {
-        printf("C: No window available for renderer creation\n");
+        SDL_Log("C: No window available for renderer creation\n");
         return lean_io_result_mk_ok(lean_box(0));
     }
-    int32_t index = (int32_t)index_unsigned;
-    g_renderer = SDL_CreateRenderer(g_window, index, flags);
+    g_renderer = SDL_CreateRenderer(g_window, NULL);
     if (g_renderer == NULL) {
         const char* error = SDL_GetError();
-        printf("C: SDL_CreateRenderer failed: %s\n", error);
+        SDL_Log("C: SDL_CreateRenderer failed: %s\n", error);
         return lean_io_result_mk_ok(lean_box(0));
     }
     return lean_io_result_mk_ok(lean_box(1));
@@ -74,7 +73,7 @@ lean_obj_res sdl_render_present(lean_obj_arg w) {
 
 lean_obj_res sdl_render_fill_rect(uint32_t x, uint32_t y, uint32_t w, uint32_t h, lean_obj_arg world) {
     if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
-    SDL_Rect rect = {(int)x, (int)y, (int)w, (int)h};
+    SDL_FRect rect = {(float)x, (float)y, (float)w, (float)h};
     int32_t result = SDL_RenderFillRect(g_renderer, &rect);
     return lean_io_result_mk_ok(lean_box_uint32(result));
 }

lakefile.lean

@@ -10,21 +10,39 @@ input_file sdl.c where
 target sdl.o pkg : FilePath := do
   let srcJob ← sdl.c.fetch
   let oFile := pkg.buildDir / "c" / "sdl.o"
-  let leanInclude := "/home/ooo/.elan/toolchains/leanprover--lean4---v4.22.0/include"
-  buildO oFile srcJob #[] #["-fPIC", "-I/usr/include/SDL2", "-D_REENTRANT", s!"-I{leanInclude}"] "cc"
+  let leanInclude := (<- getLeanIncludeDir).toString
+  let sdlInclude := "vendor/SDL/include/"
+  let sdlImageInclude := "vendor/SDL_image/include/"
+  buildO oFile srcJob #[] #["-fPIC", s!"-I{sdlInclude}", s!"-I{sdlImageInclude}", "-D_REENTRANT", s!"-I{leanInclude}"] "cc"
 
 target libleansdl pkg : FilePath := do
   let sdlO ← sdl.o.fetch
   let name := nameToStaticLib "leansdl"
+  -- manually copy the DLLs we need to .lake/build/bin/ for the game to work
+  IO.FS.createDirAll ".lake/build/bin/"
+  if Platform.isWindows then
+    copyFile "vendor/SDL/build/SDL3.dll" ".lake/build/bin/SDL3.DLL"
+    copyFile "vendor/SDL_image/build/SDL3_image.dll" ".lake/build/bin/SDL3_image.DLL"
+    let lakeBinariesDir := (← IO.appPath).parent.get!
+    println! "Copying Lake DLLs from {lakeBinariesDir}"
+
+    for entry in (← lakeBinariesDir.readDir) do
+      if entry.path.extension == some "dll" then
+       copyFile entry.path (".lake/build/bin/" / entry.path.fileName.get!)
+
   buildStaticLib (pkg.staticLibDir / name) #[sdlO]
 
 lean_lib SDL where
   moreLinkObjs := #[libleansdl]
-  moreLinkArgs := #["-lSDL2", "-lSDL2_image"]
+  moreLinkArgs := #["-lSDL3", "-lSDL3_image"]
 
 lean_lib Engine
 
 @[default_target]
 lean_exe LeanDoomed where
   root := `Main
-  moreLinkArgs := #["/usr/lib/x86_64-linux-gnu/libSDL2.so", "/usr/lib/x86_64-linux-gnu/libSDL2_image.so"]
+  -- we have to add the rpath to tell the compiler where all of the libraries are
+  moreLinkArgs := if Platform.isWindows then
+    #["vendor/SDL/build/SDL3.dll", "vendor/SDL_image/build/SDL3_image.dll"]
+  else
+    #["vendor/SDL/build/libSDL3.so", "vendor/SDL_image/build/libSDL3_image.so", "-Wl,--allow-shlib-undefined", "-Wl,-rpath=vendor/SDL/build/", "-Wl,-rpath=vendor/SDL_image/build/"]