From b5eb6d1f5d24c313668a074cf7d5e902844e2c95 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 28 Apr 2023 15:28:38 +0200
Subject: [PATCH] add dockerfile

---
 Dockerfile         | 35 +++++++++++++++++++++++++++++++++++
 lake-manifest.json | 33 ---------------------------------
 lakefile.lean      |  4 ++--
 3 files changed, 37 insertions(+), 35 deletions(-)
 create mode 100644 Dockerfile
 delete mode 100644 lake-manifest.json

diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..7c87f65
--- /dev/null
+++ b/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/
diff --git a/lake-manifest.json b/lake-manifest.json
deleted file mode 100644
index c01224e..0000000
--- a/lake-manifest.json
+++ /dev/null
@@ -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"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index f800041..0accbe5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,8 +1,8 @@
 import Lake
 open Lake DSL
 
-require GameServer from  git
-  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"
+require GameServer from
+  ".."/"lean4game"/"server"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"