diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot
index c38d1e8..740b2aa 100644
--- a/.i18n/en/Game.pot
+++ b/.i18n/en/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.21.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: 2025-08-06\n"
+"POT-Creation-Date: 2025-08-09\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
diff --git a/Game/Metadata.lean b/Game/Metadata.lean
index 24a2ecf..bb82d3c 100644
--- a/Game/Metadata.lean
+++ b/Game/Metadata.lean
@@ -1,4 +1,4 @@
-import GameServer.Commands
+import GameServer
 
 import Game.MyNat.Definition
 
diff --git a/lake-manifest.json b/lake-manifest.json
index f0f8499..e775b4d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": "server",
    "scope": "hhu-adam",
-   "rev": "8a65448ddfd23b6878aa6213b50e8f91f4e34509",
+   "rev": "274cc77ee8acc0fb3e1a78d969d4efd7a1029270",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.21.0",
diff --git a/lakefile.lean b/lakefile.lean
index c1d48d4..1e4a29b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,10 @@ open Lake DSL
 -- Using this assumes that each dependency has a tag of the form `v4.X.0`.
 def leanVersion : String := s!"v{Lean.versionString}"
 
+/--
+Use the GameServer from a `lean4game` folder lying next to the game on your local computer.
+Activated with `lake update -Klean4game.local`.
+-/
 def LocalGameServer : Dependency := {
   name := `GameServer
   scope := "hhu-adam"
@@ -12,6 +16,10 @@ def LocalGameServer : Dependency := {
   opts := ∅
 }
 
+/--
+Use the GameServer version from github.
+Deactivate local version with `lake update -R`.
+-/
 def RemoteGameServer : Dependency := {
   name := `GameServer
   scope := "hhu-adam"
@@ -20,7 +28,9 @@ def RemoteGameServer : Dependency := {
   opts := ∅
 }
 
-/- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/
+/-
+Choose GameServer dependency depending on whether `-Klean4game.local` has been passed to `lake`.
+-/
 open Lean in
 #eval (do
   let gameServerName := if get_config? lean4game.local |>.isSome then
@@ -28,37 +38,50 @@ open Lean in
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
   : Elab.Command.CommandElabM Unit)
 
-/-! # USER SECTION
+/-!
+# USER DEPENDENCIES
 
-Below are all the dependencies the game needs. Add or remove packages here as you need them.
+Add any further dependencies of your game below.
 
 Note: If your package (like `mathlib` or `Std`) has tags of the form `v4.X.0` then
-you can use `require mathlib from git "[URL]" @ leanVersion`
+you can use
+
+```
+require "leanprover-community" / mathlib @ git leanVersion
+```
  -/
 
+require "leanprover-community" / mathlib @ git leanVersion
 
+/-!
+# PACKAGE CONFIGURATION
 
-require "leanprover-community" / mathlib @ s!"git#{leanVersion}"
+Here you can set options used in your game. The player will use the same options as you'll
+have set here.
 
+NOTE: The `leanOptions` and `moreServerOptions` influence how the player preceives the game.
+For example, it is important to have `linter.all` set to `false` to prevent any linter
+warnings from showing up during playing.
 
-
-/-! # END USER SECTION -/
-
--- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
--- off when calling `lake build`. Ideally there would be a better way using `logInfo` and
--- an option like `lean4game.verbose`.
+NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
+off when calling `lake build`. Ideally there would be a better way using `logInfo` and
+an option like `lean4game.verbose`.
+-/
 package Game where
+  /- Used in all cases. -/
+  leanOptions := #[
+    /- linter warnings might block the player. (IMPORTANT) -/
+    ⟨`linter.all, false⟩,
+    /- make all assumptions always accessible. -/
+    ⟨`tactic.hygienic, false⟩]
+  /- Used when calling `lake build`. -/
   moreLeanArgs := #[
-    "-Dtactic.hygienic=false",
-    "-Dlinter.unusedVariables.funArgs=false",
-    "-Dweak.linter.unusedTactic=false",
+    -- TODO: replace with `lean4game.verbose`
     "-Dtrace.debug=false"]
+  /- Used when opening a file in VSCode or when playing the game. -/
   moreServerOptions := #[
-    ⟨`tactic.hygienic, false⟩,
-    ⟨`linter.unusedVariables.funArgs, true⟩,
-    ⟨`weak.linter.unusedTactic, false⟩,
+    -- TODO: replace with `lean4game.verbose`
     ⟨`trace.debug, true⟩]
-  weakLeanArgs := #[]
 
 @[default_target]
 lean_lib Game