diff --git a/server/GameServer.lean b/server/GameServer.lean
new file mode 100644
index 0000000..919f07a
--- /dev/null
+++ b/server/GameServer.lean
@@ -0,0 +1,2 @@
+import GameServer.Commands
+import GameServer.Server
\ No newline at end of file
diff --git a/server/NNG/GameServer/Commands.lean b/server/GameServer/Commands.lean
similarity index 99%
rename from server/NNG/GameServer/Commands.lean
rename to server/GameServer/Commands.lean
index cc0b9bb..67ac1d1 100644
--- a/server/NNG/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -1,7 +1,7 @@
 import Lean
 
-import NNG.GameServer.Utils
-import NNG.GameServer.EnvExtensions
+import GameServer.Utils
+import GameServer.EnvExtensions
 
 open Lean Meta
 
diff --git a/server/NNG/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
similarity index 97%
rename from server/NNG/GameServer/EnvExtensions.lean
rename to server/GameServer/EnvExtensions.lean
index 062565f..7bddb97 100644
--- a/server/NNG/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -1,5 +1,5 @@
-import NNG.GameServer.HashMapExtension
-import NNG.GameServer.SingleValPersistentEnvExtension
+import GameServer.HashMapExtension
+import GameServer.SingleValPersistentEnvExtension
 
 /-! # Environment extensions
 
diff --git a/server/NNG/GameServer/HashMapExtension.lean b/server/GameServer/HashMapExtension.lean
similarity index 100%
rename from server/NNG/GameServer/HashMapExtension.lean
rename to server/GameServer/HashMapExtension.lean
diff --git a/server/NNG/GameServer/Server.lean b/server/GameServer/Server.lean
similarity index 98%
rename from server/NNG/GameServer/Server.lean
rename to server/GameServer/Server.lean
index c0fe6ca..46ded93 100644
--- a/server/NNG/GameServer/Server.lean
+++ b/server/GameServer/Server.lean
@@ -6,8 +6,8 @@ It is based on lean-gym by Daniel Selsam.
 -/
 import Lean.Data.Json.Basic
 
-import NNG.GameServer.Utils
-import NNG.GameServer.EnvExtensions
+import GameServer.Utils
+import GameServer.EnvExtensions
 
 open Lean Meta Elab Tactic Std
 
@@ -223,7 +223,7 @@ where
 open System Lean Std in
 partial def runGame (GameName : Name) (paths : List FilePath): IO Unit := do
   searchPathRef.set paths
-  let env ← importModules [{ module := `Init : Import }, { module := GameName ++ GameName : Import }] {} 0    
+  let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0    
   let termElabM : TermElabM Unit := do
     let levels := levelsExt.getState env
     let game := {← gameExt.get with nb_levels := levels.size }
diff --git a/server/NNG/GameServer/SingleValPersistentEnvExtension.lean b/server/GameServer/SingleValPersistentEnvExtension.lean
similarity index 100%
rename from server/NNG/GameServer/SingleValPersistentEnvExtension.lean
rename to server/GameServer/SingleValPersistentEnvExtension.lean
diff --git a/server/NNG/GameServer/Utils.lean b/server/GameServer/Utils.lean
similarity index 100%
rename from server/NNG/GameServer/Utils.lean
rename to server/GameServer/Utils.lean
diff --git a/server/Main.lean b/server/Main.lean
index 6ee0bbb..e477189 100644
--- a/server/Main.lean
+++ b/server/Main.lean
@@ -1,13 +1,16 @@
-import NNG.GameServer.Server
-import NNG.NNG
-
-def System.FilePath.parent! (fp : System.FilePath) : System.FilePath :=
-  match fp.parent with
-  | some path => path
-  | none => panic! "Couldn't find parent folder"
-
-unsafe def main : IO Unit := do
-  let build_folder := (← IO.appPath).parent!.parent!
-  let paths : List System.FilePath := [build_folder/"lib",
-                                      (← Lean.findSysroot) / "lib" / "lean"]
-  Server.runGame `NNG paths
+import GameServer.Server
+
+unsafe def main (args : List String) : IO Unit := do
+
+  if args.length != 2 then
+    throw (IO.userError "Expected two arguments: The name of the game module and the path to the game project.")
+
+  let out ← IO.Process.output { cwd := args[1]!, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+
+  if out.exitCode != 0 then
+    IO.eprintln out.stderr
+  else
+    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+    let currentDir ← IO.currentDir
+    let paths := paths.map fun p => currentDir / (args[1]! : System.FilePath) / p
+    Server.runGame (Lean.Name.mkSimple args[0]!) paths
diff --git a/server/NNG/NNG.lean b/server/NNG/NNG.lean
deleted file mode 100644
index 7a374e7..0000000
--- a/server/NNG/NNG.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import NNG.Metadata
-import NNG.Levels.Level1
-import NNG.Levels.Level2
-import NNG.Levels.Level3
-import NNG.Levels.Level4
-import NNG.Levels.Level5
-
diff --git a/server/lakefile.lean b/server/lakefile.lean
index 5c0b06c..6ae07e2 100644
--- a/server/lakefile.lean
+++ b/server/lakefile.lean
@@ -1,20 +1,12 @@
 import Lake
 open Lake DSL
 
-package nng {
-  -- add package configuration options here
-}
-
-lean_lib NNG {
-  -- add library configuration options here
-}
+package GameServer
 
-lean_lib NNG.levels {
-  -- add library configuration options here
-}
+lean_lib GameServer
 
 @[defaultTarget]
-lean_exe nng {
+lean_exe gameserver {
   root := `Main
   supportInterpreter := true
 }
diff --git a/testgame/.gitignore b/testgame/.gitignore
new file mode 100644
index 0000000..c795b05
--- /dev/null
+++ b/testgame/.gitignore
@@ -0,0 +1 @@
+build
\ No newline at end of file
diff --git a/testgame/TestGame.lean b/testgame/TestGame.lean
new file mode 100644
index 0000000..b5b0d24
--- /dev/null
+++ b/testgame/TestGame.lean
@@ -0,0 +1,7 @@
+import TestGame.Metadata
+import TestGame.Levels.Level1
+import TestGame.Levels.Level2
+import TestGame.Levels.Level3
+import TestGame.Levels.Level4
+import TestGame.Levels.Level5
+
diff --git a/server/NNG/LemmaDocs.lean b/testgame/TestGame/LemmaDocs.lean
similarity index 83%
rename from server/NNG/LemmaDocs.lean
rename to testgame/TestGame/LemmaDocs.lean
index 12e5a8f..e49db37 100644
--- a/server/NNG/LemmaDocs.lean
+++ b/testgame/TestGame/LemmaDocs.lean
@@ -1,5 +1,5 @@
-import NNG.GameServer.Commands
-import NNG.MyNat
+import GameServer.Commands
+import TestGame.MyNat
 
 LemmaDoc zero_add as zero_add in "Addition"
 "This lemma says `∀ a : ℕ, 0 + a = a`."
diff --git a/server/NNG/Levels/Level1.lean b/testgame/TestGame/Levels/Level1.lean
similarity index 97%
rename from server/NNG/Levels/Level1.lean
rename to testgame/TestGame/Levels/Level1.lean
index c8cd1a4..1f94405 100644
--- a/server/NNG/Levels/Level1.lean
+++ b/testgame/TestGame/Levels/Level1.lean
@@ -1,4 +1,4 @@
-import NNG.Metadata
+import TestGame.Metadata
 
 Level 1
 
diff --git a/server/NNG/Levels/Level2.lean b/testgame/TestGame/Levels/Level2.lean
similarity index 96%
rename from server/NNG/Levels/Level2.lean
rename to testgame/TestGame/Levels/Level2.lean
index b73b4b2..4b1cdaf 100644
--- a/server/NNG/Levels/Level2.lean
+++ b/testgame/TestGame/Levels/Level2.lean
@@ -1,4 +1,4 @@
-import NNG.Metadata
+import TestGame.Metadata
 
 Level 2
 
diff --git a/server/NNG/Levels/Level3.lean b/testgame/TestGame/Levels/Level3.lean
similarity index 98%
rename from server/NNG/Levels/Level3.lean
rename to testgame/TestGame/Levels/Level3.lean
index 759d2f9..ec6d69c 100644
--- a/server/NNG/Levels/Level3.lean
+++ b/testgame/TestGame/Levels/Level3.lean
@@ -1,4 +1,4 @@
-import NNG.Metadata
+import TestGame.Metadata
 
 Level 3
 
diff --git a/server/NNG/Levels/Level4.lean b/testgame/TestGame/Levels/Level4.lean
similarity index 97%
rename from server/NNG/Levels/Level4.lean
rename to testgame/TestGame/Levels/Level4.lean
index 6f0cd82..6fdefc0 100644
--- a/server/NNG/Levels/Level4.lean
+++ b/testgame/TestGame/Levels/Level4.lean
@@ -1,4 +1,4 @@
-import NNG.Metadata
+import TestGame.Metadata
 
 Level 4
 
diff --git a/server/NNG/Levels/Level5.lean b/testgame/TestGame/Levels/Level5.lean
similarity index 98%
rename from server/NNG/Levels/Level5.lean
rename to testgame/TestGame/Levels/Level5.lean
index eb259cb..2298ab9 100644
--- a/server/NNG/Levels/Level5.lean
+++ b/testgame/TestGame/Levels/Level5.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.Tactics
+import TestGame.Metadata
+import TestGame.Tactics
 
 Level 5
 
diff --git a/server/NNG/Metadata.lean b/testgame/TestGame/Metadata.lean
similarity index 85%
rename from server/NNG/Metadata.lean
rename to testgame/TestGame/Metadata.lean
index de35d7e..eb71ac5 100644
--- a/server/NNG/Metadata.lean
+++ b/testgame/TestGame/Metadata.lean
@@ -1,9 +1,9 @@
-import NNG.GameServer.Commands
-import NNG.MyNat
-import NNG.TacticDocs
-import NNG.LemmaDocs
+import GameServer.Commands
+import TestGame.MyNat
+import TestGame.TacticDocs
+import TestGame.LemmaDocs
 
-Game "NNG"
+Game "TestGame"
 
 Title "The Natural Number Game"
 
diff --git a/server/NNG/MyNat.lean b/testgame/TestGame/MyNat.lean
similarity index 100%
rename from server/NNG/MyNat.lean
rename to testgame/TestGame/MyNat.lean
diff --git a/server/NNG/TacticDocs.lean b/testgame/TestGame/TacticDocs.lean
similarity index 96%
rename from server/NNG/TacticDocs.lean
rename to testgame/TestGame/TacticDocs.lean
index 9b70a9f..989e92f 100644
--- a/server/NNG/TacticDocs.lean
+++ b/testgame/TestGame/TacticDocs.lean
@@ -1,6 +1,6 @@
-import NNG.GameServer.Commands
+import GameServer.Commands
 
-import NNG.Tactics
+import TestGame.Tactics
 
 TacticDoc rfl
 "
diff --git a/server/NNG/Tactics.lean b/testgame/TestGame/Tactics.lean
similarity index 80%
rename from server/NNG/Tactics.lean
rename to testgame/TestGame/Tactics.lean
index 964ba3f..945aad9 100644
--- a/server/NNG/Tactics.lean
+++ b/testgame/TestGame/Tactics.lean
@@ -1,5 +1,5 @@
 import Lean
-import NNG.MyNat
+import TestGame.MyNat
 
 open Lean Elab Tactic
 
diff --git a/testgame/lakefile.lean b/testgame/lakefile.lean
new file mode 100644
index 0000000..4fd6349
--- /dev/null
+++ b/testgame/lakefile.lean
@@ -0,0 +1,9 @@
+import Lake
+open Lake DSL
+
+require GameServer from ".."/"server"
+
+package TestGame
+
+@[defaultTarget]
+lean_lib TestGame
diff --git a/testgame/lean-toolchain b/testgame/lean-toolchain
new file mode 100644
index 0000000..95b70f5
--- /dev/null
+++ b/testgame/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2022-09-23