Greg Shuflin
1830995cc5
The opaque Pixels type wrapped a void* pointing into an SDL_Surface's pixel buffer, but nothing tied the Pixels lifetime to the surface. If the GC collected the surface first, the Pixels pointer would dangle, causing use-after-free. Replace with two safe alternatives: - updateTexture now takes a ByteArray (Lean-owned, GC-managed buffer) plus pitch, matching how Haskell's sdl2 uses ByteString and Rust's rust-sdl2 uses &[u8]. This is faithful to SDL_UpdateTexture's general void* interface but requires copying pixels into a ByteArray first. - updateTextureFromSurface is a new zero-copy convenience that takes an SDLSurface directly. The C side extracts both pixels and pitch from the surface internally. Because the surface is borrowed (@&) for the call's duration, the GC cannot collect it mid-use. This is not strictly faithful to SDL_UpdateTexture's C API, but is the common case and avoids an unnecessary memcpy. Also removes: Pixels type, Pixels.nonemptyType, sdl_pixels_external_class, sdl_Surface_get_pixels, and the pixels_external_class registration in sdl_init. WebcamApp.lean is updated to use updateTextureFromSurface. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Lean SDL3 Bindings
This is my (Greg Shuflin's) fork of Srayan Jana's Lean SDL3 bindings. I've added a few additional SDL3 bindings, particularly ones necessary to make the webcam work. Note that this is an incomplete, work-in-progress project.
Sample Projects
In this repo, run just run to build and run the original sdl3 demo, which
displays some basic graphics and plays an mp3. Run just webcam to build and
run the webcam demo, which accesses a webcam (if one exists) and mirrors its
video on the screen.
If you want to see an example project that uses these bindings, check this out:
https://github.com/ValorZard/lean-sdl-test
How to use:
If you want to use SDL3 bindings in your own Lean4 project, add this library as
a dependency in your lakefile.lean (Not .toml)
In your default target in your project, make sure you do something like this
@[default_target]
lean_exe «lean-sdl-test» where
root := `Main
-- this is necessary because on Linux, binaries don't automatically get picked up by the executable unless you set the rpath
-- also, moreLinkArgs doesn't get inherited by the parent project
moreLinkArgs := if !System.Platform.isWindows then #["-Wl,--allow-shlib-undefined", "-Wl,-rpath=$ORIGIN"] else #[]
Acknowledgements
MASSIVE thanks to Oliver Dressler (@oOo0oOo) and Mac Malone (@tydeu) for all the help they gave!
License & Attribution
MIT