latest

Author: kiranandcode

bindings/sdl2-shim.c

@@ -1,8 +1,8 @@
 #include <lean/lean.h>
 
-#include <SDL2/SDL.h>
-#include <SDL2/SDL_image.h>
-#include <SDL2/SDL_timer.h>
+#include <SDL.h>
+#include <SDL_image.h>
+#include <SDL_timer.h>
 
 /**
  * Unwrap an Option of an external object as data for some
@@ -692,4 +692,4 @@ lean_obj_res lean_sdl_event_to_mouse_wheel_event_data(lean_obj_arg s) {
   )))));
 
   return tuple;
-}
+}

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "SDL",

lakefile.lean

@@ -1,9 +1,10 @@
+import Lean
 import Lake
 open Lake DSL
 
 package «SDL» {
   moreLinkArgs := #["-L.lake/build/lib", "-lsdl2-shim", "-lSDL2", "-lSDL2_image"]
-  extraDepTargets := #["sdl2-shim"]
+  extraDepTargets := #[Lean.Name.mkStr1 "sdl2-shim"]
 }
 
 lean_lib «SDL» {
@@ -15,15 +16,17 @@ def ffiSrc := "sdl2-shim.c"
 def ffiO   := "sdl2-shim.o"
 def ffiLib := "sdl2-shim"
 
-target ffi.o pkg : FilePath := do
+target ffi.o pkg : System.FilePath := do
   let oFile := pkg.buildDir / ffiO
-  let srcJob ← inputFile <| pkg.dir / cDir / ffiSrc
+  let srcJob ← inputFile (text:=.true) <| pkg.dir / cDir / ffiSrc
+  let cflags <- captureProc { cmd := "sdl2-config", args := #["--cflags"]}
+  let cflags := cflags.splitOn " "
   buildFileAfterDep oFile srcJob fun srcFile => do
     let flags := #["-I", (← getLeanIncludeDir).toString,
       "-I", (<- IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC"]
-    compileO ffiSrc oFile srcFile flags
+    compileO oFile srcFile (cflags.toArray ++ flags)
 
-target «sdl2-shim» pkg : FilePath := do
+target «sdl2-shim» pkg : System.FilePath := do
   let name := nameToStaticLib ffiLib
   let ffiO ← fetch <| pkg.target ``ffi.o
   buildStaticLib (pkg.buildDir / "lib" / name) #[ffiO]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.26.0