running games locally documentation

2023-06-06 10:59:58 +02:00
parent 73ca0f4d95
commit 839910a408
2 changed files with 63 additions and 23 deletions
@@ -154,3 +154,64 @@ Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level f
 can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.

 There will be features added to get automatic information from mathlib!
+
+# Running Games Locally
+
+Install `nvm`:
+```
+curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
+```
+then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
+
+Now install node:
+```
+nvm install node
+```
+
+Clone the game (e.g. `NNG4` here):
+```
+git clone git@github.com:hhu-adam/NNG4.git
+```
+
+Download dependencies and build the game:
+```
+cd NNG4
+lake update
+lake build
+```
+
+Clone the game repository into a directory next to the game:
+```
+cd ..
+git clone git@github.com:leanprover-community/lean4game.git
+```
+The folders `NNG4` and `lean4game` must be in the same directory!
+
+In `lean4game`, install dependencies:
+```
+cd lean4game
+npm install
+```
+
+If you are developing a game other than `Robo` or `NNG4`, adapt the
+code at the beginning of `lean4game/server/index.mjs`:
+```
+const games = {
+    "g/hhu-adam/robo": {
+        dir: "../../../../Robo",
+        queueLength: 5
+    },
+    "g/hhu-adam/nng4": {
+        dir: "../../../../NNG4",
+        queueLength: 5
+    }
+}
+```
+
+Run the game:
+```
+npm start
+```
+
+This takes a little time. Eventually, the server is available on http://localhost:3000/
+and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
@@ -5,11 +5,8 @@ This is a prototype for a Lean 4 game platform. The project is based on ideas fr
 of Kevin Buzzard and Mohammad Pedramfar.
 The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

-Building this requires a [npm](https://www.npmjs.com/) toolchain. After cloning the repository you should run
-`npm install` to pull in all dependencies. For development and experimentation, you can run `npm start` that will perform a non-optimized build and then run a local webserver on port 3000.
-
 ### Progress & Contributing
-Currently the interface is still undergoing bigger changes, contributions are of course welcome, but it might be better to wait with them for a bit until proper support for external games is implemented andthe existing games are separated from this repository. (ca. Sept. 2023)
+Currently the interface is still undergoing bigger changes, contributions are of course welcome, but it might be better to wait with them for a bit until proper support for external games is implemented and the existing games are separated from this repository. (ca. Sept. 2023)


 ### Documentation
@@ -17,7 +14,7 @@ Currently the interface is still undergoing bigger changes, contributions are of
 For game developers, there is a work-in-progress Documentation: [Create a Game](DOCUMENTATION.md).
 Best to talk with us directly.

-For the game engine itself, the documentations is missing currently.
+For the game engine itself, documentation is missing currently.

 ## NPM Scripts

@@ -34,21 +31,3 @@ On the server side, the command will set up a docker image containing the Lean s

 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container
 secured by [gVisor](https://gvisor.dev/).
-
-
-## Detailed installation notes
-
-### Node.js
-
-Developed using `node v19.3.0 (npm v9.2.0)`.
-
-Install `nvm`
-```
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-```
-then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
-
-Now install node:
-```
-nvm install node
-```