incrementally publishing a Lean game

Stream: Lean for teaching

[Emily Riehl]

I could use advice on a related topic. I'd like to incrementally publish the Lean game I'm working on over the course of the semester, so my students can work on a few levels while I'm building the next ones. Everything is still under development and I'll be editing constantly so the game is not at all ready for public hosting on the Lean game server as described here.

What other options are available? How difficult would it be to change the URL. (For calibration, my personal website is on github and I maintain it myself, but don't understand any of the details of how it is built.)

Another thought I've had is to follow the instructions to publish on the Lean game server but just not advertising the link anywhere (eg so it would be at the indicated URL but not listed on the main page). Is this an abuse of the Lean game server or would this work as a compromise?

[Alexander Bentkamp]

That's not an abuse of the game server. Thats how it is intended to be used.

[Alex Kontorovich]

Emily, I'm trying to do the same thing! :) We can commiserate in our suffering... Here's my prototype, set up thanks to Jon: https://adam.math.hhu.de/#/g/AlexKontorovich/RealAnalysisGame Happy to compare notes at some point...

[Alex Kontorovich]

(I guess I'm not as shy about airing my dirty laundry, it's out there for all to see...)

[Kevin Buzzard]

There are at least two games written by me+students as part of summer projects on the server and which I've never publically advertised.

[Emily Riehl]

Thanks for the advice. It's now on the web:

https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs

To make the public version I've done something which is perhaps a bit stupid which is clone two different versions of the Lean Game Server, one public and one private. The idea is I can work ahead of the class in the private version building future levels, which I periodically copy over to the public repository. So far I've just copied across the current drafts of the first two levels and kept the other five hidden (among other things, I'm still debating about the ordering).

This is a bit annoying for implementing late stage edits (eg the typo I just caught in the intro text) but if there's a way to keep part of a git repository private while making the rest public, I've never figured this out...

[Alex Kontorovich]

In case it helps: I eventually managed to figure out (with help) how to run the game locally, just from my laptop. So there's now a public version online, and also a private version on my computer. Whenever I want to move what I'm doing locally to the web, I PR to my branch, and set off the "import trigger" to the game server...

[Alex Kontorovich]

PS: the local version is also really great because once I'm done editing the code, I run lake build in the terminal (3 secs), and refresh my browser (1 sec), and I see the outcome, as opposed to PRing to the branch, waiting ~5 mins for everything to compile, and then waiting another 5-10 mins for the trigger...

[Alexander Bentkamp]

@Emily Riehl You could use two git branches, one main branch and one work-in-progress branch. When you find typos in the main branch, you can fix them there. When you want to get the new levels from the work-in-progress branch into the main branch you can use 'git merge', which allows you to keep both the typo fixes and the new levels.