diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..56c6607
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,6 @@
+[submodule "SDL"]
+	path = SDL
+	url = https://github.com/libsdl-org/SDL.git
+[submodule "SDL_image"]
+	path = SDL_image
+	url = https://github.com/libsdl-org/SDL_image.git
diff --git a/Engine.lean b/Engine.lean
index 3560d45..14aab5c 100644
--- a/Engine.lean
+++ b/Engine.lean
@@ -166,21 +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 },
diff --git a/SDL b/SDL
new file mode 160000
index 0000000..dc7a3a1
--- /dev/null
+++ b/SDL
@@ -0,0 +1 @@
+Subproject commit dc7a3a1219384a010efd90229fa48d0e203f8977
diff --git a/SDL.lean b/SDL.lean
index 6586c22..b3009cb 100644
--- a/SDL.lean
+++ b/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
diff --git a/SDL_image b/SDL_image
new file mode 160000
index 0000000..21167aa
--- /dev/null
+++ b/SDL_image
@@ -0,0 +1 @@
+Subproject commit 21167aaec8de5d0e98ca631c84c92307183ee998
diff --git a/c/sdl.c b/c/sdl.c
index 3c84573..2951577 100644
--- a/c/sdl.c
+++ b/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));
 }
diff --git a/lakefile.lean b/lakefile.lean
index f2162df..e3accb4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,8 +10,10 @@ 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/sraya/.elan/toolchains/leanprover--lean4---v4.22.0/include"
-  buildO oFile srcJob #[] #["-fPIC", "-I/usr/local/include/SDL2", "-D_REENTRANT", s!"-I{leanInclude}"] "cc"
+  let leanInclude := (<- getLeanIncludeDir).toString
+  let sdlInclude := "SDL/include/"
+  let sdlImageInclude := "SDL_image/include/"
+  buildO oFile srcJob #[] #["-fPIC", s!"-I{sdlInclude}", s!"-I{sdlImageInclude}", "-D_REENTRANT", s!"-I{leanInclude}", s!"-I{sdlInclude}", s!"-I{sdlImageInclude}"] "cc"
 
 target libleansdl pkg : FilePath := do
   let sdlO ← sdl.o.fetch
@@ -20,11 +22,11 @@ target libleansdl pkg : FilePath := do
 
 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/local/lib/libSDL2.so", "/usr/local/lib/libSDL2_image.so", "-Wl,--allow-shlib-undefined", "-Wl,-rpath=/usr/local/lib/"]
+  moreLinkArgs := #["SDL/build/libSDL3.so", "SDL_image/build/libSDL3_image.so", "-Wl,--allow-shlib-undefined", "-Wl,-rpath=SDL/build/", "-Wl,-rpath=SDL_image/build/"]