From 75d719d2aacb2ef606d416c5369ef3d3456a59b2 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 29 Feb 2024 17:06:34 +0100
Subject: [PATCH] bump gameserver and make dev-container more robust

---
 .devcontainer/devcontainer.json           | 8 +++-----
 .i18n/Game.pot                            | 4 ++--
 Game/Levels/DemoWorld/L01_HelloWorld.lean | 2 +-
 lake-manifest.json                        | 2 +-
 4 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 62b8651..b048595 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -12,12 +12,10 @@
   // I don't know why I need this, but I did...
   "overrideCommand": true,
   "onCreateCommand": {
-    "npm_install": "(cd ~/lean4game && npm install)",
-    // BUG: Apparently `&& lake exe cache get` was needed here because the update hook was broken.
-    // should been fixed in https://github.com/leanprover-community/mathlib4/pull/8755
-    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
+    "npm_install": "(cd ~/lean4game && npm install) || echo \"ERROR: `cd ~/lean4game && npm install` failed\", try running it manually in your dev-container!",
+    "lake_build": "(cd ~/game && lake update -R && lake build) || echo \"ERROR: `cd ~/game && lake update -R && lake exe cache get && lake build` failed!, try running it manually in your dev-container!\""
   },
-  "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
+  "postStartCommand": "(cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start) || echo \"ERROR: Did not start game server! See if you have warnings above, then try to start it manually using `cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start`!\"",
   "customizations": {
     "vscode": {
       "settings": {
diff --git a/.i18n/Game.pot b/.i18n/Game.pot
index ded3bff..83e931b 100644
--- a/.i18n/Game.pot
+++ b/.i18n/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Thu Feb 29 12:11:54 2024\n"
+"POT-Creation-Date: Thu Feb 29 16:58:28 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -19,7 +19,7 @@ msgid "This text is shown as first message when the level is played.\n"
 msgstr ""
 
 #: Game.Levels.DemoWorld.L01_HelloWorld
-msgid "You can either start using `h` or `g`."
+msgid "You can either start using `«{h}»` or `«{g}»`."
 msgstr ""
 
 #: Game.Levels.DemoWorld.L01_HelloWorld
diff --git a/Game/Levels/DemoWorld/L01_HelloWorld.lean b/Game/Levels/DemoWorld/L01_HelloWorld.lean
index 08cd074..7046e90 100644
--- a/Game/Levels/DemoWorld/L01_HelloWorld.lean
+++ b/Game/Levels/DemoWorld/L01_HelloWorld.lean
@@ -10,7 +10,7 @@ You can insert hints in the proof below. They will appear in this side panel
 depending on the proof a user provides."
 
 Statement (h : x = 2) (g: y = 4) : x + x = y := by
-  Hint "You can either start using `h` or `g`."
+  Hint "You can either start using `{h}` or `{g}`."
   Branch
     rw [g]
     Hint "You should use `{h}` now."
diff --git a/lake-manifest.json b/lake-manifest.json
index 2faf3e0..1f99806 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
    "subDir": "server",
-   "rev": "dd60093dfc508e6cf593b46a6c92b7cbb0f3392f",
+   "rev": "68f84a3426684914f834342854bf4963ba2d8d57",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.6.0",