Videogames developed using lean

Stream: general

[Linus]

Hello! I'm new to Zulip so apologies if this is the wrong way to do things. I wanted to ask whether there are any projects that use Lean 4 as a general purpose programming language, for example to develop a video game.

I have found not much about this topic online. There appear to exist raylib bindings for lean:
https://github.com/KislyjKisel/Raylib.lean

And there is also this
https://github.com/dwrensha/lean4-maze
but it hardly constitutes an interactive application.

Is there any project that better illustrates these capabilities of lean? I'm not looking exclusively for games, just for about anything that's interactive or graphical in some way or another.

[Linus]

https://github.com/kmill/lean4-raytracer
This project also is in the direction of what I'm looking for. And it has some funny code.
图片.png

[metakuntyyy]

Well there are some react widgets that you can use to display stuff in the infoview. I think lean is the wrong tool for games/game engines. However I think it would be hilarious if someone actually develops GDExtension bindings for Godot. Or maybe I can eat dirt and it's already developed.

[metakuntyyy]

You could even prove properties about the game objects.

[Anthony Wang]

There's https://github.com/ValorZard/lean-sdl3 by @Srayan Jana who used it to write a Flappy Bird demo.

[Linus]

Oh that looks awesome!

[Alex Nguyen]

There's also Functorio https://github.com/konne88/functorio

[Darij Grinberg]

now that's the answer to supply chain disruptions

[Ruben Van de Velde]

Oh dear, that's what I needed, another distraction to take over my free time

[Srayan Jana]

@Linus :wave: hello! im glad someone besides me is interesting in Lean game development LOL
The main issue right now with lean (and correct me if this changed at all while I've been busy with other things), is that compiling Lean with the C FFI is a bit annoying right now. You basically need to have clang installed on your computer, and there's some weird quirks that you have to deal with.

[Srayan Jana]

@metakuntyyy lowkey i have thought about writing a GDExtension for Lean....

[Srayan Jana]

To be clear, I had no issue with writing the game code in lean itself (it was actually surprisingly really nice), the main problem was just FFI build issues

[TongKe Xue]

One thing I'd like to see is a Zelda style JRPG where you go around

• instead of collecting weapons, you collect tactics / lemmas
• bosses/enemies are theorems, and you fight them by using tactics/lemmas
• and its timed, so the boss/enemy doesn't fight back, but if you don't defeat them within 120 seconds, you lose

and the goal is to build up rapid reflexes for applying lemmas/tactics :-)

[Srayan Jana]

Hey if your interested, you can try out my SDL bindings lol: https://github.com/ValorZard/lean-sdl3
Though, lemme know if there are any build issues, I can do my best to tackle them.
It's been a minute since I've done Lean stuff though, I've been focusing on other things