Zulip Chat Archive

Stream: lean4

Topic: SDL2 library SDL.lean

Anders Christiansen Sørby (Feb 22 2023 at 08:20):

My SDL.lean library now has a lakefile integration and can be loaded from Lake. Bear in mind that you currently need to have libSDL2.so and libSDL2_image.so in your linker path. In the repo nix can take care of that for you.
https://github.com/Anderssorby/SDL.lean
It supports image rendering, animations, and drawing.

Bulhwi Cha (Feb 22 2023 at 10:01):

I'm considering learning to use SDL2 for game development, so I'm glad we have SDL2 bindings for Lean! Thanks for your hard work.

Bulhwi Cha (Jul 17 2023 at 08:45):

@Anders Christiansen Sørby I don't understand these error messages. Can anyone help me?

Error message

Anders Christiansen Sørby (Jul 17 2023 at 09:00):

@Bulhwi Cha Seems like a linker issue. Your need to configure your enviroment.
You could use nix to do this: nix develop

Bulhwi Cha (Jul 17 2023 at 09:02):

I'll install Nix and see if that works.

Sebastian Ullrich (Jul 17 2023 at 10:30):

Your SDL links against a newer version of glibc than Lean does. You should be able to use LEAN_CC=gcc to make Lean use your system glibc.

Bulhwi Cha (Jul 17 2023 at 11:20):

@Anders Christiansen Sørby Nix doesn't work on my Slackware Linux 15.0 desktop. I'll create a new topic and ask how to configure Nix. It works when I run the commands as superuser privileges.

@Sebastian Ullrich Thanks, that worked! But I don't see any image after I run lake exe Tests bitmap This error occurred because I ran the command on my fork of the upstream repository. Looks cool, by the way!

bitmap.png
bitmap-upstream.png

Bulhwi Cha (Jul 17 2023 at 12:01):

When I run lake exe Tests animation or lake exe Tests event, a blank window pops up and disappears instantly.

Bulhwi Cha (Jul 17 2023 at 13:10):

Only running sudo nix run .#test -- bitmap doesn't give me an error message.

chabulhwi@desktop:~/lean-projects/SDL_upstream$ nix run .#test -- animation
error:
       … while fetching the input 'git+file:///home/chabulhwi/lean-projects/SDL_upstream'

       error: cannot connect to socket at '/nix/var/nix/daemon-socket/socket': Connection refused
chabulhwi@desktop:~/lean-projects/SDL_upstream$ sudo nix run .#test -- animation
Password:
Illegal instruction
chabulhwi@desktop:~/lean-projects/SDL_upstream$ sudo nix run .#test -- event
Illegal instruction

Anders Christiansen Sørby (Jul 17 2023 at 13:14):

Did you run git lfs checkout? The README might be outdated

Bulhwi Cha (Jul 17 2023 at 13:15):

Yes, I did.

Anders Christiansen Sørby (Jul 17 2023 at 13:16):

I recommend using lake mostly btw. It is more maintained, but you can use nix to get the right packages and env

Bulhwi Cha (Jul 17 2023 at 13:17):

Bulhwi Cha said:

When I run lake exe Tests animation or lake exe Tests event, a blank window pops up and disappears instantly.

I still can't see the animation even when I use Lake.

Anders Christiansen Sørby (Jul 17 2023 at 13:19):

Maybe it's broken. I haven't tested it in a while. Take a look at the source to see if things makes sense now. I don't have a computer at hand.

Bulhwi Cha (Jul 17 2023 at 13:21):

In order to do so, I'll learn C Programming and functional programming in Lean! Thanks anyway.

Bulhwi Cha (Jul 18 2023 at 11:52):

Someone already created a PR that fixes the issue: https://github.com/Anderssorby/SDL.lean/pull/3#issue-1620484825.

Antanas Kalkauskas (Jul 18 2023 at 19:02):

Hey @Bulhwi Cha , I have responded to your comment on my PR https://github.com/Anderssorby/SDL.lean/pull/3

Can you check if this works when you try building my PR branch without using nix?

lake clean
lake exe Tests NAME_OF_TEST

I am not experienced in nix or lean build system, but I think there might be some issue with build setup, the executables might not always be properly rebuilt and you would need to clean up them.

Bulhwi Cha (Jul 19 2023 at 00:10):

@Antanas Kalkauskas It worked! Perhaps this issue is fixed in the latest Lean 4 nightly release.

Bulhwi Cha (Jul 19 2023 at 11:24):

event.gif

Last updated: Dec 20 2023 at 11:08 UTC