From 9634e2c12f1ee67844e2971b796a269e8bfa106e Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Thu, 30 Nov 2023 10:13:54 +0100
Subject: [PATCH] complete devcontainer setup

---
 .devcontainer/devcontainer.json           |  2 +-
 Game/Levels/DemoWorld/L01_HelloWorld.lean |  4 ++--
 lake-manifest.json                        | 22 +++++++++++-----------
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index ab268b5..f4fca6f 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -13,7 +13,7 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
+    "lake_build": "(cd ~/game && lake update -R && lake build)"
   },
   "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {
diff --git a/Game/Levels/DemoWorld/L01_HelloWorld.lean b/Game/Levels/DemoWorld/L01_HelloWorld.lean
index 0cc7356..08cd074 100644
--- a/Game/Levels/DemoWorld/L01_HelloWorld.lean
+++ b/Game/Levels/DemoWorld/L01_HelloWorld.lean
@@ -13,10 +13,10 @@ Statement (h : x = 2) (g: y = 4) : x + x = y := by
   Hint "You can either start using `h` or `g`."
   Branch
     rw [g]
-    Hint "You should use {h} now."
+    Hint "You should use `{h}` now."
     rw [h]
   rw [h]
-  Hint "You should use {g} now."
+  Hint "You should use `{g}` now."
   rw [g]
 
 Conclusion "This last message appears if the level is solved."
diff --git a/lake-manifest.json b/lake-manifest.json
index 1401dbe..bf2d287 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,24 +1,24 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/lean4game.git",
-   "type": "git",
-   "subDir": "server",
-   "rev": "241ef4b67a5c95e33a4101769bb34ae45a66b82c",
-   "name": "GameServer",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0-rc2",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
    "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.3.0-rc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean4game.git",
+   "type": "git",
+   "subDir": "server",
+   "rev": "07b6525c5807436ed58ba4a3b399e694434f69d5",
+   "name": "GameServer",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0-rc2",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,