Making SDL3 bindings for Lean 4

Stream: general

[Srayan Jana]

https://github.com/ValorZard/sdl3-lean-test
Experimenting with making SDL3 bindings for Lean here.
However this is linux only for now until i can figure out a way to build this on windows. And, I'm also not sure how to process. SDL gives you a set of callbacks that it wants you to set, and I'm not really sure how to set a c callback with a Lean function?

[Srayan Jana]

Explanation on how SDL3 callbacks work: https://wiki.libsdl.org/SDL3/README-main-functions

[Srayan Jana]

Running into a weird error when trying to run lean exe

sraya@Penelope:~/sdl3-test$ lake exe sdl3-test
/home/sraya/sdl3-test/.lake/build/bin/sdl3-test: error while loading shared libraries: libSDL3.so.0: cannot open shared object file: No such file or directory

[Srayan Jana]

It can’t find libSDL3 even though it exists (I’m using guix for packages)

sraya@Penelope:~/sdl3-test$ sudo find / -name libSDL3.so.0 /gnu/store/k07f8wq9zrgngqn73vp0rhmbsyl6nx5i-profile/lib/libSDL3.so.0 /gnu/store/851kyaim7vd5p69hnwisg357rsb5wshd-profile/lib/libSDL3.so.0 /gnu/store/zrgafc6kc0n3gl6s0zssx5111qvxk09w-sdl3-3.2.10/lib/libSDL3.so.0 /gnu/store/khwamrygp99pkyrwkb6f42g5qxnb82aa-profile/lib/libSDL3.so.0 /gnu/store/lyajh49gks1hn3w8j4idv5ggr5pbry2b-sdl3-3.2.10/lib/libSDL3.so.0 /gnu/store/azv7f4kz2p833rmfs5m4d1q70407rnbf-profile/lib/libSDL3.so.0 /gnu/store/v85cayxw2snplwdcbqmcsnpl94glgn17-profile/lib/libSDL3.so.0

[Oliver Dressler]

I have also been playing around with the FFI and SDL2 bindings. This is just an experiment, maybe it helps:
https://github.com/oOo0oOo/LeanDoomed

Also ran into some similar build issues, w linking etc. Currently the build works but uses very specific paths to my system... Let me know if you figure out a nicer build than this.

[Srayan Jana]

@Oliver Dressler what would probably be nicer if you just statically link sdl3 with lean. See: https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW/issues/3

Lowkey, do you wanna team up? it would be nice to have two people on the same project.

[Oliver Dressler]

Yes, this looks similar to the issues I encountered. Was considering a vendored approach but ultimately I just wanted to implement some raycasting in Lean. I saw you were working on a PR to improve the build, I will merge if it runs on my system.

I am happy to work a bit on some more generic SDL bindings. However, I am too busy to take on proper development and maintenance of the library. If you get started I am happy to contribute some PRs..

[Srayan Jana]

Yeah my plan is to get it working without any hardcoded paths and stuff, and then once everything is working, we could probably extract out a library from this repo

[Srayan Jana]

if anyone is curious what i've been up to, i finally got standalone windows exectuables building for LeanDoomed
@Oliver Dressler https://github.com/ValorZard/LeanDoomed/tree/main

[Oliver Dressler]

Great news! I'll test it on my machine and merge it tomorrow.

[Srayan Jana]

@Oliver Dressler Note that the windows build only works on Windows itself, you can't cross compile.
However, I made it so that all of the binaries get copied to the bin folder, so you can zip it and share it on itch.io if you'd like.

I still need some help figuring out how to do the same thing on Linux, though after talking with @Sebastian Ullrich seems like I would need to

1. Figure out the rpath stuff on Linux
2. Copy over all the SDL binaries from the vendor folder into /bin
3. Copy over all of the lean binaries from wherever its stored on linux into /bin
   And presto, we got a distributable cross platform game in Lean!

I have no idea how to abstract out the bindings into a reusable library though :sweat_smile:

[Srayan Jana]

Cross Compiling itself seems like something the Lean team isnt interested in, so you'd probably need to use Github Actions or something to generate binaries

[Srayan Jana]

Also make sure you read the readme, I updated it with new build instructions

[Srayan Jana]

Also to be clear it works on Linux too, you just cant redistribute it to another computer yet cuz of the rpath stuff

[Oliver Dressler]

Ok, the possibility of deploying to itch.io is nice. I think proper cross-compilation is ambitious for this example project. The current state where you can build and run on Unix and Windows is already great!

I have tested on Unix and it works like a charm. Merged your PR :tada:

Will take some time today and try adding texture support, since you have included SDL_image in the dependencies. Hopefully we can keep the framerate up :fingers_crossed:

[Srayan Jana]

Let’s go! Thanks for merging! I have put …. Wayyy too much time into making this work. Do you have any ideas on how to set the rpath stuff correctly @Oliver Dressler ? I’d love to be able to zip up the /bin folder for Linux and share it around. We could even probably use github actions to publish releases

[Srayan Jana]

Oh also, there was a minor mistake in the cloning instructions, since it uses my git repo instead of yours. I will change that in a PR real quick

[Srayan Jana]

I GOT THE BINARIES WORKING STANDALONE
ALL I NEEDED TO DO WAS COPY ALL THE BINARIES FOR LEAN AND SDL AND NOW IT JUST WORKS
LETS GOOO
https://github.com/oOo0oOo/LeanDoomed/pull/5

[Srayan Jana]

Also here's my README fix PR https://github.com/oOo0oOo/LeanDoomed/pull/4

[Bulhwi Cha]

I get the following error when trying to run LeanDoomed:

chabulhwi@desktop ~/l/LeanDoomed (main)> lake build
✖ [8/9] Building LeanDoomed/sdl.o
trace: .> cc -c -o /home/chabulhwi/lean-projects/LeanDoomed/.lake/build/c/sdl.o /home/chabulhwi/lean-projects/LeanDoomed/c/sdl.c -fPIC -Ivendor/SDL/include/ -Ivendor/SDL_image/include/ -D_REENTRANT -I/home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.22.0/include
info: stderr:
/home/chabulhwi/lean-projects/LeanDoomed/c/sdl.c: In function ‘sdl_get_key_state’:
/home/chabulhwi/lean-projects/LeanDoomed/c/sdl.c:97:28: error: initialization of ‘const uint8_t *’ {aka ‘const unsigned char *’} from incompatible pointer type ‘const _Bool *’ [-Wincompatible-pointer-types]
   97 |     const uint8_t* state = SDL_GetKeyboardState(NULL);
      |                            ^~~~~~~~~~~~~~~~~~~~
error: external command 'cc' exited with code 1
ℹ [10/11] Ran LeanDoomed/libleansdl
info: stdout/stderr:
Copying Lake binaries from /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.22.0/lib
Some required builds logged failures:
- LeanDoomed/sdl.o
error: build failed

[Srayan Jana]

@Bulhwi Cha are you on linux or windows?

[Bulhwi Cha]

I'm on Slackware Linux.

[Srayan Jana]

If you are on linux: make sure you have build-essential or whatever llvm compiler is on your distro installed
if you are on windows: check the link in the readme about MSYS2

[Srayan Jana]

like, if you type clang in your terminal, something should pop up

[Bulhwi Cha]

chabulhwi@desktop ~/l/LeanDoomed (main) [1]> clang --version
clang version 21.1.1
Target: x86_64-unknown-linux-gnu
Thread model: posix
InstalledDir: /usr/bin

[Srayan Jana]

Ah, i see the issue
@Bulhwi Cha

sraya@Penelope:~/LeanDoomed$ lake exe LeanDoomed
ℹ [8/9] Replayed LeanDoomed/sdl.o
info: stderr:
/home/sraya/LeanDoomed/c/sdl.c: In function ‘sdl_get_key_state’:
/home/sraya/LeanDoomed/c/sdl.c:98:28: warning: initialization of ‘const uint8_t *’ {aka ‘const unsigned char *’} from incompatible pointer type ‘const _Bool *’ [-Wincompatible-pointer-types]
   98 |     const uint8_t* state = SDL_GetKeyboardState(NULL);
      |                            ^~~~~~~~~~~~~~~~~~~~
ℹ [10/11] Replayed LeanDoomed/libleansdl
info: stdout/stderr:
Copying Lake binaries from /home/sraya/.elan/toolchains/leanprover--lean4---v4.22.0/lib
Use WASD to move, A/D to turn, ESC to quit
^C
sraya@Penelope:~/LeanDoomed$

[Srayan Jana]

That's a warning on my computer, but an error on yours

[Oliver Dressler]

Yes, this was a warning for me as well. I have removed it by doing an explicit cast. Hopefully it works now?

[Srayan Jana]

Ah! i got ninjaed, yes it should work @Bulhwi Cha does it work for you?

[Srayan Jana]

I wonder how one can extract out a library out of this...
The big problem i can think of is currently this requires running a bash script. It SHOULD be possible to convert the batch script into a section of the lakefile, but then I wonder how the git sub modules would work.
If you were to get the sdl3 bindings by using https://lean-lang.org/doc/reference/4.19.0/Build-Tools-and-Distribution/Lake/#Lake___Dependency-git does that handle git sub modules as well?
Many questions....

[Bulhwi Cha]

Srayan Jana said:

Ah! i got ninjaed, yes it should work Bulhwi Cha does it work for you?

It works! 2025-09-12_20-58-17_resized.webm

[Srayan Jana]

@Oliver Dressler Sent a new PR, MASSIVELY simplified how the build process works.
Now you just have the one lakefile that does everything for you, no sketchy bash script required!
AND no git submodules
https://github.com/oOo0oOo/LeanDoomed/pull/7

[Srayan Jana]

Thinking that next steps will be:

• splitting out the sdl bindings into a seperate project
• make a simple Pong or Flappy Bird clone to show off how you can make a simple game in Lean
• maybe write a tutorial on how to do it?

[Srayan Jana]

@Oliver Dressler split out the sdl bindings into their own repository:
https://github.com/ValorZard/lean-sdl3/tree/master
Test project/Fork where I got it working: https://github.com/ValorZard/lean-sdl-test/tree/master
MASSIVE thanks to @Mac Malone for walking me through this.
I need to go for a walk and not stare at the computer anymore lol

[Srayan Jana]

If im not totally mentally exhausted I'll submit a PR, but hopefully its pretty obvious how to use them and replace what is currently there with this

[Oliver Dressler]

Sounds great! I think I would like to keep the LeanDoomed repo as a self-contained example case.
But we can obviously create a new repo based on it and also use it as an example for how to use this library.

In general it would be nice, if the library covered some more SDL functions, e.g. mouse interaction.

I am also happy to provide another simple example game for the library; the more the better. Let me know what your plans are, some variety of examples would be great. 2D, 3D, UI-heavy, ...

[Srayan Jana]

@Oliver Dressler #announce > SDL3 Bindings Alpha Release! made an annoucement releasing it to the public and future plans.
I REALLY want to do a sample project and write a tutorial on how to make your own game with it.
I can also turn the lean-sdl-test repo into its own standalone thing, and probably add your license back lol. It was originally just a private repo meant for testing out the bindings, but I'm down to make it more official

[Wrenna Robson]

Wow, this is exciting.

[Oliver Dressler]

Srayan Jana said:

I can also turn the lean-sdl-test repo into its own standalone thing, and probably add your license back lol. It was originally just a private repo meant for testing out the bindings, but I'm down to make it more official

You don't have to worry about the license. LeanDoomed is MIT-licensed, which means you can use it very freely (commercial, without attribution, change license etc). I saw that both lean-sdl3 and lean-sdl-test licenses are copied and still include my name. That's fine with me, since I wrote some of the code, but you can also change it to yours.

Only thing that's important to me is to include attribution for the creator of the wall texture, even though it is not strictly required (CC0). I saw it is in lean-sdl-test but not in lean-sdl3, which currently includes the texture in assets/. Although I would consider removing the assets/ altogether from the bindings if possible. Assets should be provided by the users of the library.

Regarding examples: I have a game concept, that I couldn't implement in lean4game, as it deviates too much from its structure. It's quite UI-heavy, so it definietly requires the ttf support you are working on.

What I miss is mouse support. Can I provide a PR?

[Srayan Jana]

@Oliver Dressler yeah I added a license in assets in lean-sdl3 for stuff like text and walls
https://github.com/ValorZard/lean-sdl3/blob/master/assets/LICENSE.md
The assets are strictly for the test app, which I could probably remove at some point. Still, I wanted some sort of minimal example to show off all the features, which requires some assets to do so.
Feel free to submit as many PRs as you want! I'm kinda flying by the seat of my pants here.
I'm trying to refactor the SDL bindings as much as I can to make them as flexible as possible

[Srayan Jana]

Also, I added SDL_Mixer support so now all four main SDL libraries are now in lean-SDL3! I don't anticipate adding any more libraries, since this is more than enough to start making games lol

[Srayan Jana]

You can run the test app by doing lake exe test-app

[Srayan Jana]

If you could, I'd really appreciate a PR at some point that updates "lean-sdl-test" to the latest version of the SDL3 bindings. I did a bunch of refactoring that breaks a bunch of code, since it was still assuming you were doing the raycasting stuff. I figure it would be better for the bindings to expose the low level C stuff, and you just do all the high level stuff in Lean

[Srayan Jana]

Also, quoting this from DMs,
Currently, we have a single mutable variable g_texture that stores the texture once created.

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_texture) SDL_DestroyTexture(g_texture);
    g_texture = SDL_CreateTextureFromSurface(g_renderer, surface);
    SDL_DestroySurface(surface);

    if (!g_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));
}

I'd rather for that to be stored in Lean itself

For the texture, you would want to register a texture class with register_external_class (that runs SDL_DestroyTexture in the finalizer) and and then wrap the texture via alloc_external using that class.

Mac Malone said:

An opaqur type would be either:

opaque SDL.Texture : Type

or, if you want it to provably nonempty (which you probably do):

namespace SDL
private opaque Texture.nonemptyType : NonemptyType.)0{
def Texture : Type := Texture.nonemptyType.type
instance Texture.instNonempty : Nonempty Texture := Texture.nonemptyType.property
end

This would probably be a solution to all of the global mutable variables floating around

[Srayan Jana]

We would need to use
lean_register_external_class and lean_alloc_external
https://github.com/leanprover/lean4/blob/90db9ef006467ae5998f8707e420a392a88a05b8/src/include/lean/lean.h#L303
https://github.com/leanprover/lean4/blob/90db9ef006467ae5998f8707e420a392a88a05b8/src/runtime/object.cpp#L2636
https://github.com/leanprover/lean4/blob/90db9ef006467ae5998f8707e420a392a88a05b8/src/include/lean/lean.h#L1228

[Oliver Dressler]

Srayan Jana said:

This would probably be a solution to all of the global mutable variables floating around

Yes, this major refactor is absolutely required for the library. The current asset handling was only good enough for LeanDoomed but we definitely want to support multiple textures/fonts/etc with proper memory management.
I'll do a PR the next few days.

[Srayan Jana]

https://github.com/ValorZard/lean-sdl3/pull/6
Okay this seems easier than I thought, just really tedious

[Srayan Jana]

@Oliver Dressler did the PR, it was suprsingly easy to return SDL Objects as Lean Objects

[Srayan Jana]

The one thing tripping me up is that you can't pass any signed integers, so we basically have to cast from int64 to uint64 and then back to Int64 in lean, which feels .. gross

[Kim Morrison]

Could you open an issue for this? Signed integers are a relatively late addition to Lean.

[Srayan Jana]

@Kim Morrison https://github.com/leanprover/lean4/issues/10561
here you go!

[Srayan Jana]

https://github.com/ValorZard/lean-sdl-test
Turned this into a (sorta) flappy bird clone
Let me know what your guys high score is! It's pretty hard :sweat_smile:

[Srayan Jana]

https://valorzard.itch.io/lean-sdl-test
Uploaded the windows version on itch in case anyone doesn't want to compile it themselves

[Srayan Jana]

Adding proper graphics and audio to the game.
The jumping noise is pretty annoying though, lol

[Srayan Jana]

Okay, so I should probably talk about where my mind is at currently.
For now, I'm probably not going to add any more features to the SDL bindings
However, I will continue to maintain it and try to fix any new build issues that pop up.
This is because I'm not really sure if people really want to use it :sweat_smile:
Recently, I went to UC Berkley to take part in the Lean for PDEs conference thing, and after talking to the people there, I came to the conclusion that the stuff im working on, while fun, just isn't very useful for the Lean community right now.
There were some interesting ideas I got, like maybe using SDL to model temperature PDEs or whatever, but ultimately none of them were super compelling to me.
There's a couple of other projects I want to pursue, so I'll go do that instead for now.
However, this NOT to say I'm abandoning this or anything. If anyone needs help or if they want to add a new feature or whatever, feel free to ping me on here or file an issue on Github and I'll try to take care of it straight away!

[Anthony Wang]

Thanks for creating these SDL bindings! I have a few Lean project ideas that involve using SDL but I've been too busy recently to work on them. I'm also interested in creating SQLite bindings for Lean but have no idea where to start, so your project might be useful as reference.

I think here on the Lean Zulip and at conferences, most people are interested in math and proofs rather than software development, so thus they might not be as interested in SDL bindings. However, there are also Lean users outside of those circles and a small but increasing number of people trying to use Lean for writing other kinds of programs, for which your bindings could be useful for.

[Srayan Jana]

@Anthony Wang thank you so much!
Yeah I went back and tried to learn Haskell, and I won’t lie, using Lean feels so much better haha.
Again, I’d love to work on more stuff for lean, but maybe it’s best to wait a bit before doing so,
HAVING SAID THAT:
I would be super down to work on SQlite bindings for Lean. I learned a lot from the sdl bindings

[Srayan Jana]

If you’d like to collaborate on such a project, I’ll be all ears

[Anthony Wang]

Sure! My idea for the project is that in most programming languages, SQL queries are just strings, but in Lean we can do better and make it type safe by embedding the SQLite syntax and semantics in Lean. There's already a similar project for PostgreSQL but it didn't get very far.

[Eric Taucher]

Please consider starting a new thread for the SQLite bindings discussion. I have a strong interest in SQLite integration with Lean 4, and I think a dedicated topic would help future readers interested in this specific aspect locate the conversation more easily.

---

Some of my ideas/needs include

• Proofs with the code.
• Hoare pre/post conditions.
• Use of views instead of free form text for queries.
• Having more than one SQLite module that would require proofs versus a binding that does not require proofs.

[Eric Taucher]

Thanks Anthony for creating the SQLite binding topic.

#general > SQLite bindings for Lean