Replicating Lean Game Server Locally

Stream: general

[Richard L Ford]

I would like to replicate the Lean Game Server locally. I tried with just the server and one game, but ran into build problems, I thinking probably due to version skew. It would be helpful if the Lean Game Server would list the urls and version tags of the server and all of the supplied games to make it easier to reproduce. It would also be helpful if directions were supplied on how to do this.

[Kevin Buzzard]

I've had no problems with running everything locally, following the instructions here https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md (and I did this a lot when I was developing NNG). However I note that currently lean4game is not passing CI https://github.com/leanprover-community/lean4game/actions/runs/20576820292/job/59095589334 -- perhaps this is your issue?

[PAUL BERNARD]

The issue comes from the use of gitpkg.vercel.app in the dependencies, which has been shut down for some reason recently. From what I've seen, there has been some efforts to fix this issue: https://github.com/leanprover-community/lean4game/pull/431
I also have tried on my side with no success since I'm not really familiar with the node-npm ecosystem

[Jon Eugster]

Indeed, Alex has a half-finished fix and I've allocated as much time as necessary from 6.-12. January to fix the installation issues.
I'm sorry it's not installable currently without tricky workarounds or with cache.

As for the URL of games, there isn't a button right now, but you can open a game's overview page and replace adam.math.hhu.de/#/g/ with github.com/ and you should be on the source repo of the game (i.e. the last two parts of the url are deliberately gitbhub-user/github-repo)

[Richard L Ford]

I see. Thanks for the information. So getting the URLs is easy. If the hashes of the live versions were available, then one could deploy locally even if the master version is broken. I did look back in the test history for lean4game and see the last version that passed CI, so I'll try that version and see if I have success.

[Alexander Bentkamp]

I don't think you will find an old version that works because the setup broke when an external server that we relied on stopped working.

[Richard L Ford]

OK. Good to know. I'll wait for the fix while also studying the source code to understand how the game server works.

[Richard L Ford]

But if that is the case, why does the live version at hhu.de still work?

[Alexander Bentkamp]

It's only npm install that is a problem. Once the problematic dependencies are cached, even npm install works.

[Richard L Ford]

OK. Thanks.

[Richard L Ford]

I looked a little at vercel. It looks like it was useful at managing node dependencies. Is the plan now to change things to avoid vercel?

[Richard Kelley]

@Richard L Ford I forked the server and got it running without the Vercel dependency. You can see what I did here: https://github.com/RichardKelley/lean4game/tree/remove-vercel. It's not much code, so I suspect that this will get resolved rather soon.

[Richard L Ford]

@Richard Kelley, Thanks. I'll take a look.

[Jon Eugster]

I've now merged @Alexander Bentkamp's fix including @Richard Kelley's adjustments. Big thank you to both of you!

I hope this means the projects should be installable again. Let me know if you have further issues with it!

[Richard L Ford]

It now works for me. Thanks!