From d37c2ade127d696eb93cf203d3ebc3c4afdec6ff Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 4 May 2023 11:48:58 +0200
Subject: [PATCH] Clean up Dockerfile

---
 .github/workflows/build.yml | 17 +----------------
 Dockerfile                  | 29 ++++++++++++-----------------
 lake-manifest.json          | 33 +++++++++++++++++++++++++++++++++
 lakefile.lean               | 20 ++++++++++++++++++--
 4 files changed, 64 insertions(+), 35 deletions(-)
 create mode 100644 lake-manifest.json

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ca57f1e..6b2148b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -7,23 +7,8 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      
+
       - uses: actions/checkout@v2
-      
-      - name: lake update
-        run: lake update
-        
-      - name: get cache
-        run: lake exe cache get
-      
-      - name: build game
-        run: env LEAN_ABORT_ON_PANIC=1 lake build
 
       - name: build docker image
         run: docker build . --file Dockerfile --tag nng:latest
diff --git a/Dockerfile b/Dockerfile
index cf9fbc2..be47069 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,5 +1,3 @@
-ARG GAME_DIR
-
 FROM ubuntu:18.04
 
 WORKDIR /
@@ -14,22 +12,19 @@ RUN ./elan-init -y --default-toolchain leanprover/lean4:nightly-2022-09-23
 # TODO: Read out lean version from lean-toolchain file
 ENV PATH="${PATH}:/root/.elan/bin"
 
-# Copy lean files
-COPY lake-packages/GameServer/server/GameServer ./GameServer
-COPY lake-packages/GameServer/server/Main.lean ./Main.lean
-COPY lake-packages/GameServer/server/lakefile.lean ./lakefile.lean
-COPY lake-packages/GameServer/server/lake-manifest.json ./lake-manifest.json
-COPY lake-packages/GameServer/server/lean-toolchain ./lean-toolchain
+# Copy the game to `game`
+COPY . ./game
 
-# Copy the game to `nng`
-COPY NNG ./nng/NNG
-COPY NNG.lean ./nng/NNG.lean
-COPY lakefile.lean ./nng/lakefile.lean
-COPY lake-manifest.json ./nng/lake-manifest.json
-COPY lean-toolchain ./nng/lean-toolchain
+WORKDIR /game
+RUN lake update
+RUN lake exe cache get
 
-WORKDIR /
-RUN rm -f ./build/bin/gameserver
+WORKDIR /game/lake-packages/GameServer/server/
+RUN lake clean
 RUN lake build
 
-WORKDIR /build/bin/
+WORKDIR /game
+RUN lake clean
+RUN lake build
+
+WORKDIR /game/lake-packages/GameServer/server/build/bin/
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..fc82033
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,33 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "fc4a489c2af75f687338fe85c8901335360f8541",
+    "name": "mathlib",
+    "inputRev?": "fc4a489c2af75f687338fe85c8901335360f8541"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "cc915afc9526e904a7b61f660d330170f9d60dd7",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/lean4game.git",
+    "subDir?": "server",
+    "rev": "dd7f1a8e20f26ae391abba51f8dcddba4c2a30d9",
+    "name": "GameServer",
+    "inputRev?": "main"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
+    "name": "std",
+    "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index f800041..750e815 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,8 +1,24 @@
 import Lake
 open Lake DSL
 
-require GameServer from  git
-  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"
+def LocalGameServer : Dependency := {
+  name := `GameServer
+  src := Source.path "../lean4game/server"
+}
+
+def RemoteGameServer : Dependency := {
+  name := `GameServer
+  src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
+}
+
+/- Choose dependency depending on the environment variable NODE_ENV -/
+open Lean in
+#eval (do
+  let gameServerName :=
+    if (← IO.getEnv "NODE_ENV") == some "development" then ``LocalGameServer else ``RemoteGameServer
+  modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
+   : Elab.Command.CommandElabM Unit)
+
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"