lean phone apps

Stream: general

[Kevin Buzzard]

If I find myself without a computer I'm sometimes forced to play phone games and right now I'm very slowly working through about 1000 sokoban levels. Ones like this

3e1f72c3-19c4-438e-a2b1-19d5944efbe1.png

annoy me a bit because part of the puzzle here is the endgame, ie how to begin the dual game where you pull the crosses under the boxes, and I can't play the dual game on my phone app. But I've seen sokoban in lean. What would it take to make a simple phone app where I could write simple algorithms for manipulating sokoban levels in lean and applying them at the touch of a button?

[Kevin Buzzard]

Would one be able to use Tatham's framework somehow? Sorry for being so clueless. What I'm after is "write algorithm on my laptop, compile to an android app and now I've got a button which applies my algorithm to a position on my phone".. Or even just a basic sokoban app

[Matthew Ballard]

Has anyone generated Java from Lean?

[Kevin Buzzard]

or C?
https://www.chiark.greenend.org.uk/~sgtatham/puzzles/devel/

[Eric Wieser]

Lean compiles to C already!

[Eric Wieser]

So one answer is "fork tatham's puzzles, and add some code to interact with lean", which will save you from dealing with the android bits

[Bernardo Borges]

You could try to integrate with react native, since lean game already integrates with react in the web