From dac15d84b5500c5005f0a4fe40039c4e001b89b0 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 23 Mar 2023 15:54:47 +0100
Subject: [PATCH] add build mechanism for nng

---
 UPDATE_LEAN.sh           |  4 ++++
 package.json             |  2 +-
 server/build.sh          | 12 +++++++++++-
 server/index.mjs         |  3 ++-
 server/server.Dockerfile |  4 ++--
 5 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh
index 3ea0fe4..899dbbc 100755
--- a/UPDATE_LEAN.sh
+++ b/UPDATE_LEAN.sh
@@ -10,6 +10,10 @@ lake update
 
 cp lake-packages/mathlib/lean-toolchain lean-toolchain
 cp lake-packages/mathlib/lean-toolchain ../leanserver/lean-toolchain
+cp lake-packages/mathlib/lean-toolchain ../nng/lean-toolchain
 
 cd ../leanserver
 lake update
+
+cd ../nng
+lake update
diff --git a/package.json b/package.json
index a230586..ebe5cdc 100644
--- a/package.json
+++ b/package.json
@@ -56,7 +56,7 @@
   },
   "scripts": {
     "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
-    "start_server": "cd server && (cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build)  && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
+    "start_server": "cd server && (cd leanserver && lake build) && (cd testgame && lake exe cache get && lake build)  && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"",
     "start_client": "NODE_ENV=development webpack-dev-server --hot",
     "build": "npm run build_server && npm run build_client",
     "build_server": "server/build.sh",
diff --git a/server/build.sh b/server/build.sh
index bc3f11a..3b85690 100755
--- a/server/build.sh
+++ b/server/build.sh
@@ -6,6 +6,16 @@ cd $(dirname $0)
 # Build elan image if not already present
 docker build --pull --rm -f elan.Dockerfile -t elan:latest .
 
+# Build testgame
 (cd testgame && lake exe cache get && lake build)
 docker rmi testgame:latest || true
-docker build --rm -f server.Dockerfile -t testgame:latest .
+docker build \
+  --build-arg GAME_DIR=testgame \
+  --rm -f server.Dockerfile -t testgame:latest .
+
+# Build NNG
+(cd nng && lake build)
+docker rmi nng:latest || true
+docker build \
+  --build-arg GAME_DIR=nng \
+  --rm -f server.Dockerfile -t nng:latest .
diff --git a/server/index.mjs b/server/index.mjs
index 4e80f8a..756987c 100644
--- a/server/index.mjs
+++ b/server/index.mjs
@@ -45,7 +45,8 @@ function startServerProcess(gameId) {
             ["--server", gameId, games[gameId].module, games[gameId].name],
             { cwd: "./leanserver/build/bin/" })
         : cp.spawn("docker",
-            ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`],
+            ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`,
+              "./gameserver", "--server", gameId, games[gameId].module, games[gameId].name],
             { cwd: "." })
     serverProcess.on('error', error =>
         console.error(`Launching Lean Server failed: ${error}`)
diff --git a/server/server.Dockerfile b/server/server.Dockerfile
index a054176..304b16b 100644
--- a/server/server.Dockerfile
+++ b/server/server.Dockerfile
@@ -1,10 +1,11 @@
+ARG GAME_DIR
 FROM elan:latest
 
 WORKDIR /
 
 # Copy lean files
 COPY leanserver ./leanserver
-COPY testgame ./testgame
+COPY $GAME_DIR ./$GAME_DIR
 # TODO: make `testgame` a build argument
 
 WORKDIR /leanserver
@@ -12,4 +13,3 @@ RUN rm -f ./build/bin/gameserver
 RUN lake build
 
 WORKDIR /leanserver/build/bin/
-CMD ["./gameserver", "--server", "testgame", "TestGame", "TestGame"]