Sokoban

Stream: general

[Miroslav Olšák]

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]

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

[Miroslav Olšák]

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]

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]

So I added the html visualisation. Enjoy!