From c2b9175fe5fbde9e442d1122e8d1d651b6dda9d2 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 8 Dec 2023 18:14:35 +0100
Subject: [PATCH] use the gameserver of each game individually

---
 server/bubblewrap.sh |  6 ++++--
 server/index.mjs     | 15 ++++++++++++---
 server/lakefile.lean | 20 ++++++++++++++++++++
 3 files changed, 36 insertions(+), 5 deletions(-)

diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh
index 6f6cd20..53ed95f 100755
--- a/server/bubblewrap.sh
+++ b/server/bubblewrap.sh
@@ -2,7 +2,9 @@
 
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
-
+# $1 : the game directory
+# $2 : the lean4game folder
+# $3 : the gameserver executable
 
 (exec bwrap\
   --bind $2 /lean4game \
@@ -25,5 +27,5 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
   --unshare-cgroup \
   --die-with-parent \
   --chdir "/lean4game/server/.lake/build/bin/" \
-  ./gameserver --server /game
+  $3 --server /game
 )
diff --git a/server/index.mjs b/server/index.mjs
index 743af10..4b78bb8 100644
--- a/server/index.mjs
+++ b/server/index.mjs
@@ -95,11 +95,20 @@ function startServerProcess(owner, repo) {
   let serverProcess
   if (isDevelopment) {
     let args = ["--server", game_dir]
-    serverProcess = cp.spawn("./gameserver", args,  // TODO: find gameserver inside the games
-        { cwd: path.join(__dirname, "./.lake/build/bin/") })
+    let executable = path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver")
+    if (fs.existsSync(executable)) {
+      // Try to use the game's own copy of `gameserver`.
+      serverProcess = cp.spawn(executable, args, { cwd: game_dir })
+    } else {
+      // If the game is built with `-Klean4game.local` there is no copy in the lake packages.
+      serverProcess = cp.spawn("./gameserver", args,
+        { cwd: path.join(__dirname, ".lake", "build", "bin") })
+    }
   } else {
     serverProcess =  cp.spawn("./bubblewrap.sh",
-      [game_dir, path.join(__dirname, '..')],
+      [ game_dir,
+        path.join(__dirname, '..'),
+        path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver")],
       { cwd: __dirname })
   }
   serverProcess.on('error', error =>
diff --git a/server/lakefile.lean b/server/lakefile.lean
index 851c78d..1adad98 100644
--- a/server/lakefile.lean
+++ b/server/lakefile.lean
@@ -15,3 +15,23 @@ lean_exe gameserver {
   root := `Main
   supportInterpreter := true
 }
+
+/--
+When a package depending on GameServer updates its dependencies,
+build the `gameserver` executable.
+-/
+post_update pkg do
+  let rootPkg ← getRootPackage
+  if rootPkg.name = pkg.name then
+    return -- do not run in GameServer itself
+
+  /-
+  TODO: Could we use the Lake API instead of spawning a new process?
+  -/
+  let toolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
+  let exitCode ← IO.Process.spawn {
+    cmd := "elan"
+    args := #["run", toolchain.trim, "lake", "build", "gameserver"]
+  } >>= (·.wait)
+  if exitCode ≠ 0 then
+    logError s!"{pkg.name}: failed to build gameserver"