add dockerfile

Dockerfile

@@ -0,0 +1,35 @@
+ARG GAME_DIR
+
+FROM ubuntu:18.04
+
+WORKDIR /
+
+RUN apt-get update
+RUN apt-get upgrade -y
+RUN apt-get install -y git curl libatomic1
+
+# Install elan
+RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+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"
+
+
+FROM elan:latest
+
+WORKDIR /
+
+# Copy lean files
+COPY lake-packages/lean4game/server/GameServer ./GameServer
+COPY lake-packages/lean4game/server/Main.lean ./Main
+COPY lake-packages/lean4game/server/lakefile.lean ./lakefile.lean
+COPY lake-packages/lean4game/server/lake-manifest.json ./lake-manifest.json
+COPY lake-packages/lean4game/server/lean-toolchain ./lean-toolchain
+COPY $GAME_DIR ./$GAME_DIR
+# TODO: make `adam` a build argument
+
+WORKDIR /
+RUN rm -f ./build/bin/gameserver
+RUN lake build
+
+WORKDIR /build/bin/

lake-manifest.json

@@ -1,33 +0,0 @@
-{"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": "759e9722f869364695ab32a4b624668268ff5d13",
-    "name": "GameServer",
-    "inputRev?": "main"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
-    "name": "std",
-    "inputRev?": "main"}}]}

lakefile.lean

@@ -1,8 +1,8 @@
 import Lake
 open Lake DSL
 
-require GameServer from  git
+require GameServer from
-  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"
+  ".."/"lean4game"/"server"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"