got bindings building, but not right

2025-09-20 16:11:27 -07:00
commit 6fdaf64761
8 changed files with 398 additions and 0 deletions
@@ -0,0 +1 @@
+.lake/
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2025 Oliver Dressler
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
@@ -0,0 +1,38 @@
+# Lean SDL3 Bindings
+
+
+## Run
+
+### Unix (Linux, Mac)
+
+```bash
+# Install elan if this is your first time using Lean
+curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
+
+# Clone project and submodules (SDL3 etc)
+git clone --recurse-submodules https://github.com/oOo0oOo/LeanDoomed.git
+cd LeanDoomed
+
+# Build dependencies
+chmod +x ./build_sdl_and_friends.sh
+sudo ./build_sdl_and_friends.sh
+
+# Run the "game"
+lake exe LeanDoomed
+```
+
+### Windows (MSYS2 or WSL)
+
+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
+
+Next, follow the instructions for Unix above.
+
+## License & Attribution
+
+MIT
+
+Wall texture by [FacadeGaikan](https://opengameart.org/node/31075), licensed under CC0.
@@ -0,0 +1,59 @@
+namespace SDL
+
+def SDL_INIT_VIDEO : UInt32 := 0x00000020
+def SDL_WINDOW_SHOWN : UInt32 := 0x00000004
+def SDL_RENDERER_ACCELERATED : UInt32 := 0x00000002
+def SDL_QUIT : UInt32 := 0x100
+
+def SDL_SCANCODE_W : UInt32 := 26
+def SDL_SCANCODE_A : UInt32 := 4
+def SDL_SCANCODE_S : UInt32 := 22
+def SDL_SCANCODE_D : UInt32 := 7
+def SDL_SCANCODE_LEFT : UInt32 := 80
+def SDL_SCANCODE_RIGHT : UInt32 := 79
+def SDL_SCANCODE_SPACE : UInt32 := 44
+def SDL_SCANCODE_ESCAPE : UInt32 := 41
+
+@[extern "sdl_init"]
+opaque init : UInt32 → IO UInt32
+
+@[extern "sdl_quit"]
+opaque quit : IO Unit
+
+@[extern "sdl_create_window"]
+opaque createWindow : String → Int32 → Int32 → UInt32 → IO UInt32
+
+@[extern "sdl_create_renderer"]
+opaque createRenderer : Unit → IO UInt32
+
+@[extern "sdl_set_render_draw_color"]
+opaque setRenderDrawColor : UInt8 → UInt8 → UInt8 → UInt8 → IO Int32
+
+@[extern "sdl_render_clear"]
+opaque renderClear : IO Int32
+
+@[extern "sdl_render_present"]
+opaque renderPresent : IO Unit
+
+@[extern "sdl_render_fill_rect"]
+opaque renderFillRect : Int32 → Int32 → Int32 → Int32 → IO Int32
+
+@[extern "sdl_delay"]
+opaque delay : UInt32 → IO Unit
+
+@[extern "sdl_poll_event"]
+opaque pollEvent : IO UInt32
+
+@[extern "sdl_get_ticks"]
+opaque getTicks : IO UInt32
+
+@[extern "sdl_get_key_state"]
+opaque getKeyState : UInt32 → IO Bool
+
+@[extern "sdl_load_texture"]
+opaque loadTexture : String → IO UInt32
+
+@[extern "sdl_render_texture_column"]
+opaque renderTextureColumn : Int32 → Int32 → Int32 → Int32 → Int32 → Int32 → IO Int32
+
+end SDL
@@ -0,0 +1,135 @@
+#include <stdint.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;
+static SDL_Texture* g_wall_texture = NULL;
+
+lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) {
+    int32_t result = SDL_Init(flags);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_quit(lean_obj_arg w) {
+    if (g_wall_texture) {
+        SDL_DestroyTexture(g_wall_texture);
+        g_wall_texture = NULL;
+    }
+    if (g_renderer) {
+        SDL_DestroyRenderer(g_renderer);
+        g_renderer = NULL;
+    }
+    if (g_window) {
+        SDL_DestroyWindow(g_window);
+        g_window = NULL;
+    }
+    SDL_Quit();
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+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)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(lean_obj_arg w) {
+    if (g_window == NULL) {
+        SDL_Log("C: No window available for renderer creation\n");
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+    g_renderer = SDL_CreateRenderer(g_window, NULL);
+    if (g_renderer == NULL) {
+        const char* error = SDL_GetError();
+        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));
+}
+
+lean_obj_res sdl_set_render_draw_color(uint8_t r, uint8_t g, uint8_t b, uint8_t a, lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
+    int32_t result = SDL_SetRenderDrawColor(g_renderer, r, g, b, a);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_render_clear(lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box_uint32(-1));
+    int32_t result = SDL_RenderClear(g_renderer);
+    return lean_io_result_mk_ok(lean_box_uint32(result));
+}
+
+lean_obj_res sdl_render_present(lean_obj_arg w) {
+    if (g_renderer == NULL) return lean_io_result_mk_ok(lean_box(0));
+    SDL_RenderPresent(g_renderer);
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+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_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));
+}
+
+lean_obj_res sdl_delay(uint32_t ms, lean_obj_arg w) {
+    SDL_Delay(ms);
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+lean_obj_res sdl_poll_event(lean_obj_arg w) {
+    SDL_Event event;
+    int has_event = SDL_PollEvent(&event);
+    return lean_io_result_mk_ok(lean_box_uint32(has_event ? event.type : 0));
+}
+
+lean_obj_res sdl_get_ticks(lean_obj_arg w) {
+    uint32_t ticks = SDL_GetTicks();
+    return lean_io_result_mk_ok(lean_box_uint32(ticks));
+}
+
+lean_obj_res sdl_get_key_state(uint32_t scancode, lean_obj_arg w) {
+    const uint8_t* state = (const uint8_t*)SDL_GetKeyboardState(NULL);
+    uint8_t pressed = state[scancode];
+    return lean_io_result_mk_ok(lean_box(pressed));
+}
+
+// TEXTURE SUPPORT
+// Assuming 64x64 texture
+lean_obj_res sdl_load_texture(lean_obj_arg filename, lean_obj_arg w) {
+    const char* filename_str = lean_string_cstr(filename);
+    SDL_Surface* surface = IMG_Load(filename_str);
+    if (!surface) {
+        SDL_Log("C: Failed to load texture: %s\n", SDL_GetError());
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    if (g_wall_texture) SDL_DestroyTexture(g_wall_texture);
+    g_wall_texture = SDL_CreateTextureFromSurface(g_renderer, surface);
+    SDL_DestroySurface(surface);
+
+    if (!g_wall_texture) {
+        SDL_Log("C: Failed to create texture: %s\n", SDL_GetError());
+        return lean_io_result_mk_ok(lean_box(0));
+    }
+
+    return lean_io_result_mk_ok(lean_box(1));
+}
+
+lean_obj_res sdl_render_texture_column(uint32_t dst_x, uint32_t dst_y, uint32_t dst_height, uint32_t src_x, uint32_t src_y_start, uint32_t src_y_end, lean_obj_arg w) {
+    if (!g_renderer || !g_wall_texture) return lean_io_result_mk_ok(lean_box_uint32(-1));
+
+    uint32_t tex_y_start = src_y_start >= 64 ? 0 : src_y_start;
+    uint32_t tex_y_end = src_y_end > 64 ? 64 : src_y_end;
+    if (tex_y_end <= tex_y_start) tex_y_end = tex_y_start + 1;
+
+    SDL_FRect src_rect = {(float)(src_x % 64), (float)tex_y_start, 1.0f, (float)(tex_y_end - tex_y_start)};
+    SDL_FRect dst_rect = {(float)dst_x, (float)dst_y, 1.0f, (float)dst_height};
+
+    return lean_io_result_mk_ok(lean_box_uint32(SDL_RenderTexture(g_renderer, g_wall_texture, &src_rect, &dst_rect)));
+}
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "LeanDoomed",
+ "lakeDir": ".lake"}
@@ -0,0 +1,138 @@
+import Lake
+open System Lake DSL
+
+package SDL3
+
+def sdlGitRepo : String := "https://github.com/libsdl-org/SDL.git"
+def sdlRepoDir : String := "vendor/SDL"
+
+def sdlImageGitRepo : String := "https://github.com/libsdl-org/SDL_image.git"
+def sdlImageRepoDir : String := "vendor/SDL_image"
+
+-- clone from a stable branch to avoid breakages
+def sdlBranch : String := "release-3.2.x"
+
+input_file sdl.c where
+  path := "c" / "sdl.c"
+  text := true
+
+target sdl.o pkg : FilePath := do
+  let srcJob ← sdl.c.fetch
+  let oFile := pkg.buildDir / "c" / "sdl.o"
+  let leanInclude := (<- getLeanIncludeDir).toString
+  let sdlInclude := "vendor/SDL/include/"
+  let sdlImageInclude := "vendor/SDL_image/include/"
+  let compiler := if Platform.isWindows then "gcc" else "cc"
+  buildO oFile srcJob #[] #["-fPIC", s!"-I{sdlInclude}", s!"-I{sdlImageInclude}", "-D_REENTRANT", s!"-I{leanInclude}"] compiler
+
+target libleansdl pkg : FilePath := do
+-- Helper function to run command and handle errors
+-- Clone the repos if they don't exist
+  let sdlExists ← System.FilePath.pathExists sdlRepoDir
+  if !sdlExists then
+    IO.println "Cloning SDL"
+    let sdlClone ← IO.Process.output { cmd := "git", args := #["clone", "-b", sdlBranch, "--single-branch", "--depth", "1", "--recursive", sdlGitRepo, sdlRepoDir] }
+    if sdlClone.exitCode != 0 then
+      IO.println s!"Error cloning SDL: {sdlClone.stderr}"
+    else
+      IO.println "SDL cloned successfully"
+      IO.println sdlClone.stdout
+
+  let sdlImageExists ← System.FilePath.pathExists sdlImageRepoDir
+  if !sdlImageExists then
+    IO.println "Cloning SDL_image"
+    let sdlImageClone ← IO.Process.output { cmd := "git", args := #["clone", "-b", sdlBranch, "--single-branch", "--depth", "1", "--recursive", sdlImageGitRepo, sdlImageRepoDir] }
+    if sdlImageClone.exitCode != 0 then
+      IO.println s!"Error cloning SDL_image: {sdlImageClone.stderr}"
+    else
+      IO.println "SDL_image cloned successfully"
+      IO.println sdlImageClone.stdout
+
+-- Build the repos with cmake
+-- SDL itself needs to be built before SDL_image, as the latter depends on the former
+-- We also need to make sure we are using a system provided C compiler, as the one that comes with Lean is missing important headers
+  IO.println "Building SDL"
+-- Create build directory if it doesn't exist
+  let sdlBuildDirExists ← System.FilePath.pathExists (sdlRepoDir ++ "/build")
+  if !sdlBuildDirExists then
+    let compiler := if Platform.isWindows then "gcc" else "cc"
+    let configureSdlBuild ← IO.Process.output { cmd := "cmake", args := #["-S", sdlRepoDir, "-B", sdlRepoDir ++ "/build", "-DBUILD_SHARED_LIBS=ON", "-DCMAKE_BUILD_TYPE=Release", s!"-DCMAKE_C_COMPILER={compiler}"] }
+    if configureSdlBuild.exitCode != 0 then
+      IO.println s!"Error configuring SDL: {configureSdlBuild.stderr}"
+    else
+      IO.println "SDL configured successfully"
+      IO.println configureSdlBuild.stdout
+  else
+    IO.println "SDL build directory already exists, skipping configuration step"
+-- now actually build SDL once we've configured it
+  let buildSdl ← IO.Process.output { cmd := "cmake", args :=  #["--build", sdlRepoDir ++ "/build", "--config", "Release",] }
+  if buildSdl.exitCode != 0 then
+    IO.println s!"Error building SDL: {buildSdl.exitCode}"
+    IO.println buildSdl.stderr
+  else
+    IO.println "SDL built successfully"
+    IO.println buildSdl.stdout
+-- Build SDL_Image
+  IO.println "Building SDL_image"
+-- Create SDL_Image build directory if it doesn't exist
+  let sdlImageBuildDirExists ← System.FilePath.pathExists (sdlImageRepoDir ++ "/build")
+  if !sdlImageBuildDirExists then
+    let currentDir ← IO.currentDir
+    let sdlConfigPath := currentDir / sdlRepoDir / "build"
+    let compiler := if Platform.isWindows then "gcc" else "cc"
+    let configureSdlImageBuild ← IO.Process.output { cmd := "cmake", args :=  #["-S", sdlImageRepoDir, "-B", sdlImageRepoDir ++ "/build", s!"-DSDL3_DIR={sdlConfigPath}", "-DBUILD_SHARED_LIBS=ON", "-DCMAKE_BUILD_TYPE=Release", s!"-DCMAKE_C_COMPILER={compiler}"] }
+    if configureSdlImageBuild.exitCode != 0 then
+      IO.println s!"Error configuring SDL_image: {configureSdlImageBuild.stderr}"
+    else
+      IO.println "SDL_image configured successfully"
+      IO.println configureSdlImageBuild.stdout
+  else
+    IO.println "SDL_image build directory already exists, skipping configuration step"
+-- now actually build SDL_image once we've configured it
+  let buildSdlImage ← IO.Process.output { cmd := "cmake", args := #["--build", sdlImageRepoDir ++ "/build", "--config", "Release"] }
+  if buildSdlImage.exitCode != 0 then
+    IO.println s!"Error building SDL_image: {buildSdlImage.stderr}"
+  else
+    IO.println "SDL_image built successfully"
+    IO.println buildSdlImage.stdout
+
+  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/"
+  let dstDir := ".lake/build/bin/"
+  let sdlBinariesDir : FilePath := "vendor/SDL/build/"
+  for entry in (← sdlBinariesDir.readDir) do
+    if entry.path.extension != none then
+      copyFile entry.path (dstDir / entry.path.fileName.get!)
+  let sdlImageBinariesDir : FilePath := "vendor/SDL_image/build/"
+  for entry in (← sdlImageBinariesDir.readDir) do
+    if entry.path.extension != none then
+      copyFile entry.path (dstDir / entry.path.fileName.get!)
+  if Platform.isWindows then
+    -- binaries for Lean/Lake itself for the executable to run standalone
+    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!)
+  else
+  -- binaries for Lean/Lake itself, like libgmp are on a different place on Linux
+    let lakeBinariesDir := (← IO.appPath).parent.get!.parent.get! / "lib"
+    println! "Copying Lake binaries from {lakeBinariesDir}"
+
+    for entry in (← lakeBinariesDir.readDir) do
+      if entry.path.extension != none then
+       copyFile entry.path (".lake/build/bin/" / entry.path.fileName.get!)
+
+  buildStaticLib (pkg.staticLibDir / name) #[sdlO]
+
+@[default_target]
+lean_lib SDL where
+  moreLinkObjs := #[libleansdl]
+  -- 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=$ORIGIN", "-Wl,-rpath=$ORIGIN"]
@@ -0,0 +1 @@
+leanprover/lean4:v4.23.0