How to play natural number game locally, not on browser?

Stream: new members

[Claire Wang]

Hey am new to lean - I've been playing natural number game but lost progress when I cleared my cookies. I just want to play it on my terminal - this would also get me used to having my own dev environment for writing lean. I cloned the repo here https://github.com/ImperialCollegeLondon/natural_number_game/tree/master but there's a lot of other files for the website. Was wondering if anyone has played without the browser on their machine, and what files were needed and not needed. thanks!

[Kevin Buzzard]

That looks like the Lean 3 version of the game. But whether you use Lean 3 or Lean 4 https://github.com/leanprover-community/NNG4, one issue will be that all of the levels are fully solved in the source code.

[Claire Wang]

would it be of much trouble to have a version of nng that one can clone and play from cli, without solutions in the level code but a separate file of solutions that can be used to test solutions? i also don't mind helping out if it seems worthwhile to do

[Kevin Buzzard]

I think the only issue with playing in VS Code is simply that all the solutions are there already, and you'll have to move between words manually by opening files. But if you write some code which just strips out all the proofs in NNG4/Game/Levels/*/*.lean(there is a unique proof in each of those files) then there's no reason you can't just fill in the solutions again, although you will lose all the hints.

[Julian Berman]

It would be nice to have something in GameMaker that autogenerated such a thing. I assume it must have enough of the metadata to do so given it's doing it to generate the web page

[Julian Berman]

(But I haven't looked -- I do remember wanting the same thing though when trying to play one of the other games)

[Dan Velleman]

There are instructions here for running a game locally:
https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md
I have been doing this on a mac (using the VSCode Dev Containers approach).

[Dan Velleman]

Well, maybe that's not what you're looking for--you'd still be playing the game in a browser, but without using the internet.