failed to run lean game server on windows 11

Stream: general

[Subin Kim]

Good Afternoon,

My name is Subin Kim, and I am a university student from South Korea.

I recently became interested in Lean and have just started learning it. I encountered an issue while trying to clone and run the Lean4game server from this link: https://github.com/leanprover-community/lean4game, and I am seeking advice on how to resolve it.

Issue description:

1. I attempted to run the Lean4game server on a Windows 11 OS environment.
2. All dependencies related to npm and Node.js were installed successfully.
3. The result of the npm -v command was 9.8.1, and the result of the node -v command was 20.6.1.
4. After installing all necessary dependencies via npm install, I ran the npm start command.
5. However, after the server starts, both npm run start_client and npm run start_server automatically exit with code 1.
6. I also tried accessing http://192.168.219.104:3000/ in my Chrome browser, which was the IP address provided by the server logs:

Here is the relevant log output:

rla00@LAPTOP-M9P88K6J MINGW64 ~/2024-OSSCA-Lean/activity/lean4game (main)
$ npm start

> lean4-game@0.1.0 start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client"

[server]
[server] > lean4-game@0.1.0 start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client] > lean4-game@0.1.0 start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server] info: downloading component 'lean'
[client]
[client] VITE v4.5.3 ready in 9351 ms
[client]
[client] ➜ Local: http://localhost:3000/
[client] ➜ Network: http://192.168.219.104:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[server] ^C^CTerminate batch job (Y/N)? Terminate batch job (Y/N)? npm run start_client exited with code 1
[server] npm run start_server exited with code 1

I would appreciate any advice on how to resolve this issue.

Thank you.

[Bulhwi Cha]

By the way, she's one of my mentees in this year's Open-Source Software Contribution Academy.

[Bulhwi Cha]

We're trying to translate the Natural Number Game into Korean, but so far, only I've been able to run the Lean web game server locally without any errors.

I'm the only Linux user on my team.

[Jon Eugster]

Im sorry, I wont really have time to debug windows issue over the next two weeks.

But if you just want to work on NNG, does it work if you open the NNG repo in VScode and then "open in devcontainer"? (This needs docker istalled but is supposed to be the easy way to get everything running)

What I'm confused about is that the only thing I see in the provided log is that the user manually killed everything with pressing Ctrl-C twice. Am I missing something?

Moreover, just to dummy-check the most trivial issues, you dou have built your game with lake build, haven't you?

[Jon Eugster]

Conretely, these are the instructions Im thinking of: running game in devcontainer

[Bulhwi Cha]

Jon Eugster said:

What I'm confused about is that the only thing I see in the provided log is that the user manually killed everything with pressing Ctrl-C twice. Am I missing something?

I think you're right. I'll try running the server on Windows 11, which is also installed on my computer.

[Subin Kim]

@Jon Eugster I pressed ctrl+c(shortcut key) to copy this link(http://192.168.219.104:3000/) on my Windows operating system, and this seems to have been a failure to run the server. I copied it in a different way and confirmed that the server runs normally!! It was an inexperienced question, but thank you for clear suggesting the solution!

[Bulhwi Cha]

This may be useful: https://superuser.com/q/1639562.

[Bulhwi Cha]

It's about how to customize shortcut keys on Git Bash.

[Jon Eugster]

Indeed, in terminal/shell its usually Ctrl+Shift+C to copy, I myself killed so many processes by accident, too.

Glad it works:blush: Let me know if there are further issues