Lean4 Natural Number Game server down?

Stream: general

[David Loeffler]

I'm getting an HTTP "address unreachable" error from https://adam.math.hhu.de/#/g/hhu-adam/NNG4. Are other people seeing this too, or is there something fishy with my own network connection?

(I was hoping to use this for a class that starts in 55 minutes, so if the server's really down, then I'm in trouble...)

[Ruben Van de Velde]

Down here, and https://downforeveryoneorjustme.com/adam.math.hhu.de also agrees

[David Loeffler]

I'm currently frantically trying to get a local docker container working and failing. Looks like that's my class for today gone down the pan, then.

[Johan Commelin]

Would it be worth considering to play the Lean 3 version instead? I know it's not ideal....

[Henrik Böving]

I just scrambled a little to run it on my server but after building the container there it gives me Watchdog error: Cannot read LSP request: Stream was closed when trying to run it. If someone can tell me how to fix that I can give you nng4.hboeving.dev

[Alexander Bentkamp]

I'm sorry, this is my fault. Working on it...

[Alexander Bentkamp]

It's back online.

[Alexander Bentkamp]

@David Loeffler Sorry for spoiling your class

[David Loeffler]

Alexander Bentkamp said:

David Loeffler Sorry for spoiling your class

No problem, thanks for getting it back up + running again!

[Henrik Böving]

Alexander Bentkamp said:

I'm sorry, this is my fault. Working on it...

do you have a guess as to why it was failing locally for me?

[David Loeffler]

FWIW, I didn't manage to get anywhere running it locally with docker; running docker container fails with the message

failed to create task for container: failed to create shim task: OCI runtime create failed: runc create failed: unable to start container process: exec: \"3000:3000\": executable file not found in $PATH: unknown

It seems that the port number (3000) is getting misinterpreted as a separate command.

[Patrick Massot]

We clearly need at least a second server if people start teaching using it.

[Alexander Bentkamp]

You can run the game on codespaces by the way: https://github.com/hhu-adam/NNG4#codespaces

[Alexander Bentkamp]

@Henrik Böving A docker container is no longer necessary. We use bubblewrap for isolation now.

[Alexander Bentkamp]

(deleted)

[Alexander Bentkamp]

Oh, well, I see what went wrong. We are in the process of using bubblewrap instead of docker, and things got out of sync.

[Alexander Bentkamp]

The version of lean4game that works with docker would be commit 52b42544ac8bcdbf4655e9c3a99567d924bd0caf

[Alexander Bentkamp]

We need to rework this to make it easier to install again.

[Kevin Buzzard]

I have got NNG running locally on my laptop with npm start. I've never ever got devcontainers/docker working. The last time I tried, the system started downloading a second copy of all of mathlib, owned by root, in my repo's lake-packages directory, and also scattered other root-owned files around the place; the only fix I found was to delete the entire directory as root and then reclone everything

In contrast I've had no problems with npm running locally on Ubuntu 22.04 and I intend to use NNG on my laptop in class in October

[Alexander Bentkamp]

Yes, I assume you are using this setup: https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#without-dev-containers

[Alexander Bentkamp]

That should still work.

[Alexander Bentkamp]

I think @Henrik Böving tried to do a production setup.

[Henrik Böving]

Indeed I tried to run the container directly on my server with docker build + docker run but got this weird LSP error

[Kevin Buzzard]

Alexander Bentkamp said:

Yes, I assume you are using this setup: https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#without-dev-containers

Yes, and it has been absolutely wonderful for game development. I can make changes locally in the Lean files, run lake build and then click reload on my browser and see them instantly. It is so much better than NNG3 development, which was super-painful!

Random NNG4 update: I have tutorial -> addition -> multiplication -> power worlds in a state I'm happy with, and am currently working on advanced addition world.

[Alexander Bentkamp]

Henrik Böving said:

Indeed I tried to run the container directly on my server with docker build + docker run but got this weird LSP error

Ah, I see, the Dockerfiles are not intended to be used like that.