From 6fdaf64761a40fc1f282fe563426e7eddfb31600 Mon Sep 17 00:00:00 2001 From: Srayan Jana Date: Sat, 20 Sep 2025 16:11:27 -0700 Subject: [PATCH] got bindings building, but not right --- .gitignore | 1 + LICENSE | 21 +++++++ README.md | 38 +++++++++++++ SDL.lean | 59 +++++++++++++++++++ c/sdl.c | 135 ++++++++++++++++++++++++++++++++++++++++++++ lake-manifest.json | 5 ++ lakefile.lean | 138 +++++++++++++++++++++++++++++++++++++++++++++ lean-toolchain | 1 + 8 files changed, 398 insertions(+) create mode 100644 .gitignore create mode 100644 LICENSE create mode 100644 README.md create mode 100644 SDL.lean create mode 100644 c/sdl.c create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1cc6956 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.lake/ \ No newline at end of file diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..cf35317 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 index 0000000..6b74e76 --- /dev/null +++ b/README.md @@ -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. \ No newline at end of file diff --git a/SDL.lean b/SDL.lean new file mode 100644 index 0000000..4aaabd1 --- /dev/null +++ b/SDL.lean @@ -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 diff --git a/c/sdl.c b/c/sdl.c new file mode 100644 index 0000000..e899ebd --- /dev/null +++ b/c/sdl.c @@ -0,0 +1,135 @@ +#include +#include +#include +#include + +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))); +} \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..2f53fda --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "LeanDoomed", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..15f3168 --- /dev/null +++ b/lakefile.lean @@ -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"] diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..14a4424 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0 \ No newline at end of file