Merge branch 'main' of https://github.com/hhu-adam/Robo into main

.devcontainer/devcontainer.json

@@ -13,7 +13,9 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update -R && lake build"
+    // 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)"
   },
   "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {

Game.lean

@@ -18,7 +18,7 @@ import Game.Levels.Function
 --import Game.Levels.LinearAlgebra
 
 
-Title "Game over oder QED?"
+Title "Formaloversum"
 Introduction
 "
 # Game Over oder QED?
@@ -75,6 +75,17 @@ Kontakt: [Jon Eugster](https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprech
 Conclusion
 "Fertig!"
 
+
+/-! Information to be displayed on the servers landing page. -/
+Languages "German"
+CaptionShort "Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
+CaptionLong "Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
+
+(Das Spiel befindet sich noch in der Entstehungsphase.)"
+-- Prerequisites "" -- add this if your game depends on other games
+CoverImage "images/cover.png"
+
 Dependency Inequality → SetTheory
 
+/-! Build the game. Show's warnings if it found a problem with your game. -/
 MakeGame

Game/Levels/Implication.lean

@@ -14,6 +14,8 @@ import Game.Levels.Implication.L12_Summary
 World "Implication"
 Title "Implis"
 
+Image "images/planet_logos.jpg"
+
 Introduction
 "
 Zurück im Raumschiff macht ihr euch auf den Weg zu einem benachbarten Planeten, der ebenfalls

Game/Levels/Proposition.lean

@@ -16,6 +16,8 @@ import Game.Levels.Proposition.L13_Summary
 World "Proposition"
 Title "Logo"
 
+Image "images/planet_logos.jpg"
+
 Introduction "
 Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
 bist du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.

images/LICENSE.md

@@ -0,0 +1 @@
+All images in this game are under copyright and may not be reused or redistributed beyond this game's context.

lake-manifest.json

@@ -4,19 +4,19 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
+   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0-rc2",
+   "inputRev": "v4.3.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
    "subDir": "server",
-   "rev": "622e9d389768e8abb5b3103a65d07165587a27ad",
+   "rev": "d5697d052e5154b909f379073a591ebf66eb3e22",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0-rc2",
+   "inputRev": "v4.3.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "83d4f222771f491b351d70b070406481f5d2b2ba",
+   "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0-rc2",
+   "inputRev": "v4.3.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Game",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.3.0