From 8246ae6eac0f8a88f962ccd645aa3cfaa8e8c177 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 26 Apr 2023 01:31:35 +0200 Subject: [PATCH] change folder structure --- UPDATE_LEAN.sh | 4 ++-- package.json | 2 +- server/.gitignore | 3 +++ server/{leanserver => }/.vscode/settings.json | 0 server/{leanserver => }/GameServer/AbstractCtx.lean | 0 server/{leanserver => }/GameServer/Commands.lean | 0 server/{leanserver => }/GameServer/EnvExtensions.lean | 0 server/{leanserver => }/GameServer/FileWorker.lean | 0 server/{leanserver => }/GameServer/Game.lean | 0 server/{leanserver => }/GameServer/Graph.lean | 0 .../{leanserver => }/GameServer/InteractiveGoal.lean | 0 server/{leanserver => }/GameServer/RpcHandlers.lean | 2 +- server/{leanserver => }/GameServer/Watchdog.lean | 2 +- server/{leanserver => }/Main.lean | 0 server/index.mjs | 2 +- server/{leanserver => }/lake-manifest.json | 0 server/{leanserver => }/lakefile.lean | 0 server/{leanserver => }/lean-toolchain | 0 server/leanserver/.gitignore | 1 - server/server.Dockerfile | 10 +++++++--- 20 files changed, 16 insertions(+), 10 deletions(-) create mode 100644 server/.gitignore rename server/{leanserver => }/.vscode/settings.json (100%) rename server/{leanserver => }/GameServer/AbstractCtx.lean (100%) rename server/{leanserver => }/GameServer/Commands.lean (100%) rename server/{leanserver => }/GameServer/EnvExtensions.lean (100%) rename server/{leanserver => }/GameServer/FileWorker.lean (100%) rename server/{leanserver => }/GameServer/Game.lean (100%) rename server/{leanserver => }/GameServer/Graph.lean (100%) rename server/{leanserver => }/GameServer/InteractiveGoal.lean (100%) rename server/{leanserver => }/GameServer/RpcHandlers.lean (99%) rename server/{leanserver => }/GameServer/Watchdog.lean (99%) rename server/{leanserver => }/Main.lean (100%) rename server/{leanserver => }/lake-manifest.json (100%) rename server/{leanserver => }/lakefile.lean (100%) rename server/{leanserver => }/lean-toolchain (100%) delete mode 100644 server/leanserver/.gitignore diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh index 34f979f..27ebc35 100644 --- a/UPDATE_LEAN.sh +++ b/UPDATE_LEAN.sh @@ -9,10 +9,10 @@ cd adam lake update cp lake-packages/mathlib/lean-toolchain lean-toolchain -cp lake-packages/mathlib/lean-toolchain ../leanserver/lean-toolchain +cp lake-packages/mathlib/lean-toolchain ../lean-toolchain cp lake-packages/mathlib/lean-toolchain ../nng/lean-toolchain -cd ../leanserver +cd ../ lake update cd ../nng diff --git a/package.json b/package.json index 67cab6b..7d7b64c 100644 --- a/package.json +++ b/package.json @@ -58,7 +58,7 @@ }, "scripts": { "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"", - "start_server": "cd server && (cd leanserver && lake build) && (cd adam && lake exe cache get && lake build) && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", + "start_server": "cd server && lake build && (cd adam && lake exe cache get && lake build) && (cd nng && lake build) && NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", "start_client": "NODE_ENV=development webpack-dev-server --hot", "build": "npm run build_server && npm run build_client", "build_server": "server/build.sh", diff --git a/server/.gitignore b/server/.gitignore new file mode 100644 index 0000000..103f95b --- /dev/null +++ b/server/.gitignore @@ -0,0 +1,3 @@ +build +adam +nng diff --git a/server/leanserver/.vscode/settings.json b/server/.vscode/settings.json similarity index 100% rename from server/leanserver/.vscode/settings.json rename to server/.vscode/settings.json diff --git a/server/leanserver/GameServer/AbstractCtx.lean b/server/GameServer/AbstractCtx.lean similarity index 100% rename from server/leanserver/GameServer/AbstractCtx.lean rename to server/GameServer/AbstractCtx.lean diff --git a/server/leanserver/GameServer/Commands.lean b/server/GameServer/Commands.lean similarity index 100% rename from server/leanserver/GameServer/Commands.lean rename to server/GameServer/Commands.lean diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean similarity index 100% rename from server/leanserver/GameServer/EnvExtensions.lean rename to server/GameServer/EnvExtensions.lean diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean similarity index 100% rename from server/leanserver/GameServer/FileWorker.lean rename to server/GameServer/FileWorker.lean diff --git a/server/leanserver/GameServer/Game.lean b/server/GameServer/Game.lean similarity index 100% rename from server/leanserver/GameServer/Game.lean rename to server/GameServer/Game.lean diff --git a/server/leanserver/GameServer/Graph.lean b/server/GameServer/Graph.lean similarity index 100% rename from server/leanserver/GameServer/Graph.lean rename to server/GameServer/Graph.lean diff --git a/server/leanserver/GameServer/InteractiveGoal.lean b/server/GameServer/InteractiveGoal.lean similarity index 100% rename from server/leanserver/GameServer/InteractiveGoal.lean rename to server/GameServer/InteractiveGoal.lean diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean similarity index 99% rename from server/leanserver/GameServer/RpcHandlers.lean rename to server/GameServer/RpcHandlers.lean index 8cdc928..8903a3d 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -28,7 +28,7 @@ def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) return none def gameDirFromInitParams (initParams : Lsp.InitializeParams) : Option String := - (splitRootUri initParams 0).map (s!"../../../{·}") + (splitRootUri initParams 0).map (s!"../../{·}") def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do let some levelId := levelIdFromFileName? initParams fileName diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/GameServer/Watchdog.lean similarity index 99% rename from server/leanserver/GameServer/Watchdog.lean rename to server/GameServer/Watchdog.lean index e3ad48f..790cd56 100644 --- a/server/leanserver/GameServer/Watchdog.lean +++ b/server/GameServer/Watchdog.lean @@ -99,7 +99,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do throwServerError s!"Expected 3 command line arguments in addition to `--server`: game directory, the name of the main module, and the name of the game" let gameId := args[1]! - let gameDir := s!"../../../{gameId}" + let gameDir := s!"../../{gameId}" let module := args[2]! let gameName := args[3]! let workerPath := "./gameserver" diff --git a/server/leanserver/Main.lean b/server/Main.lean similarity index 100% rename from server/leanserver/Main.lean rename to server/Main.lean diff --git a/server/index.mjs b/server/index.mjs index cdb6db9..8dbec7a 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -43,7 +43,7 @@ function startServerProcess(gameId) { const serverProcess = isDevelopment ? cp.spawn("./gameserver", ["--server", gameId, games[gameId].module, games[gameId].name], - { cwd: "./leanserver/build/bin/" }) + { cwd: "./build/bin/" }) : cp.spawn("docker", ["run", "--runtime=runsc", "--network=none", "--rm", "-i", `${gameId}:latest`, "./gameserver", "--server", gameId, games[gameId].module, games[gameId].name], diff --git a/server/leanserver/lake-manifest.json b/server/lake-manifest.json similarity index 100% rename from server/leanserver/lake-manifest.json rename to server/lake-manifest.json diff --git a/server/leanserver/lakefile.lean b/server/lakefile.lean similarity index 100% rename from server/leanserver/lakefile.lean rename to server/lakefile.lean diff --git a/server/leanserver/lean-toolchain b/server/lean-toolchain similarity index 100% rename from server/leanserver/lean-toolchain rename to server/lean-toolchain diff --git a/server/leanserver/.gitignore b/server/leanserver/.gitignore deleted file mode 100644 index c795b05..0000000 --- a/server/leanserver/.gitignore +++ /dev/null @@ -1 +0,0 @@ -build \ No newline at end of file diff --git a/server/server.Dockerfile b/server/server.Dockerfile index 7cf6aee..2cc494c 100644 --- a/server/server.Dockerfile +++ b/server/server.Dockerfile @@ -4,12 +4,16 @@ FROM elan:latest WORKDIR / # Copy lean files -COPY leanserver ./leanserver +COPY GameServer ./GameServer +COPY Main ./Main +COPY lakefile.lean ./lakefile.lean +COPY lake-manifest.lean ./lake-manifest.lean +COPY lean-toolchain ./lean-toolchain COPY $GAME_DIR ./$GAME_DIR # TODO: make `adam` a build argument -WORKDIR /leanserver +WORKDIR / RUN rm -f ./build/bin/gameserver RUN lake build -WORKDIR /leanserver/build/bin/ +WORKDIR /build/bin/