bump gameserver and make dev-container more robust

hhu-adam · Feb 29, 2024 · 75d719d · 75d719d
1 parent dfaaf56
commit 75d719d
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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",