Zulip Chat Archive

Stream: general

Topic: natural numbers game

Michael Melesse (Sep 29 2021 at 23:26):

Is the natural numbers game site down? https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

Mario Carneiro (Sep 29 2021 at 23:28):

the address in my history is https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ . Maybe imperial switched their hosting around and broke something?

Mario Carneiro (Sep 29 2021 at 23:29):

@Kevin Buzzard

Kevin Buzzard (Sep 30 2021 at 06:48):

Yeah looks like I have no personal website right now

Marc Masdeu (Sep 30 2021 at 07:14):

If you check out https://github.com/mmasdeu/topologygame you will see how I managed to hack github actions to deploy a NNG-like game automatically on gh-pages. I have an option to deploy a test version so that the players don't get upset at each tiny update. I think that this setup is worth advertising, you can edit the game (and play it!) from any device...

Ruben Van de Velde (Sep 30 2021 at 07:38):

It seems like https://mmasdeu.github.io/topologygame/?world=2&level=2 is failing to import level1

Marc Masdeu (Sep 30 2021 at 10:33):

Ruben Van de Velde said:

It seems like https://mmasdeu.github.io/topologygame/?world=2&level=2 is failing to import level1

Fixed it, thanks! In the process, I made it to always take the latest Lean browser extension. So everything is a bit more automated. It would be nice to have a "level submission" form, but I don't have the skills to do it.

Michael Melesse (Sep 30 2021 at 13:07):

Thank you. Hopefully it can be up soon. Just wanted to say this was a genius idea. I feel like I have finally found my way in into mathematics.

Kevin Buzzard (Sep 30 2021 at 13:29):

@Marc Masdeu that's very cool :-) In fact the entire ma.ic.ac.uk domain seems down right now, although this is very rare in my experience. You know Patrick wrote a bunch of tactics in French? It's easy to write new tactics which just mimic old tactics in a different language, so you could make a Catalan version!

Marc Masdeu (Sep 30 2021 at 14:30):

@Kevin Buzzard I think that what students find hard when first seeing Lean is not the fact that it's in English, precisely!

Apurva Nakade (Sep 30 2021 at 17:25):

@Marc Masdeu This is really cool! I don't quite understand github actions so I dunno what's going on in the background here. Do I just fork the repo and hack away or do I need to install the Lean-game-maker locally first?

Marc Masdeu (Sep 30 2021 at 19:20):

You can just fork it (actually I made the repo a template, so you it'll be essentially a brand new repo) and hack tot your pleasure. No need to install game-maker (or Lean, for that matter)! You will probably have to push some button in your repo page to enable gh pages, and every time you want to recompile you need to run the action manually.
Let me know how it works for you, please.