use the gameserver of each game individually

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
 )

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 =>

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"