Lean SDL3 Bindings Example

Playing around with SDL3 bindings in Lean4 to learn about the FFI.

Simple real-time Doom-style raycasting engine in Lean4:

Run

This is just an experiment

First, make sure you've set up Lean properly on your computer. If you are on Windows, use MSYS2 or WSL IMPORTANT: FOR MSYS2, MAKE SURE YOU ARE USING THE "CLANG" SHELL TO RUN EVERYTHING Follow the "legacy" instructions from here (They should work on Linux, WSL, and MSYS2): https://leanprover-community.github.io/install/linux.html

Second, make sure you run the build script first to build all the dependencies to get this to work

chmod +x ./build_sdl_and_friends.sh
sudo ./build_sdl_and_friends.sh

Then you can run the game proper

lake exe LeanDoomed

License

MIT