Zulip Chat Archive

Stream: general

Topic: Sokoban


Miroslav Olšák (Apr 19 2021 at 15:08):

Hello, I just wanted to say that my Sokoban implementation in Lean is finaly sort of working: https://github.com/mirefek/sokoban.lean, I can prove that a level is solvable by providing a solution, or prove that certain configurations of boxes / missing boxes make the level unsolvable (form a deadlock). On the other hand I cannot say it would be very "playable" in Lean, that's why I also have the other Python version :smile:

Oliver Nash (Apr 19 2021 at 15:13):

This looks awesome. How difficult would it be to hook this up to a widget ?

Miroslav Olšák (Apr 19 2021 at 15:16):

It shouldn't be too difficult, I am just using mainly emacs which doesn't support them (as far as I know). But maybe, I will add this widget fanciness at some point :-) (also there is not deadlock visualisation so far).

Oliver Nash (Apr 19 2021 at 15:21):

Emacs is wonderful of course but IMHO the tactic state widget makes it worth the switch VS Code. Anyway, very nice work.

Miroslav Olšák (Apr 20 2021 at 10:54):

So I added the html visualisation. Enjoy!


Last updated: Dec 20 2023 at 11:08 UTC