From 08d1e172865401513aa930f081aaf3c470234d52 Mon Sep 17 00:00:00 2001
From: seasawher <tellagoodstory@icloud.com>
Date: Wed, 7 Jun 2023 14:13:09 +0000
Subject: [PATCH] add devcontainer and tasks.json

---
 .devcontainer/Dockerfile         | 29 +++++++++++++++++++++++++++++
 .devcontainer/devcontainer.json  |  5 +++++
 .devcontainer/docker-compose.yml | 14 ++++++++++++++
 .vscode/tasks.json               | 15 +++++++++++++++
 4 files changed, 63 insertions(+)
 create mode 100644 .devcontainer/Dockerfile
 create mode 100644 .devcontainer/devcontainer.json
 create mode 100644 .devcontainer/docker-compose.yml
 create mode 100644 .vscode/tasks.json

diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
new file mode 100644
index 0000000..d02495f
--- /dev/null
+++ b/.devcontainer/Dockerfile
@@ -0,0 +1,29 @@
+FROM node:20
+
+WORKDIR /
+
+ENV ELAN_HOME=/usr/local/elan \
+  PATH=/usr/local/elan/bin:$PATH \
+  LEAN_VERSION=leanprover/lean4:nightly
+
+SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
+  chmod -R a+w $ELAN_HOME; \
+  elan --version; \
+  lean --version; \
+  leanc --version; \
+  lake --version;
+
+RUN git clone https://github.com/hhu-adam/NNG4.git
+
+WORKDIR /NNG4
+RUN lake update && lake build
+
+WORKDIR /
+RUN git clone https://github.com/leanprover-community/lean4game.git
+
+WORKDIR /lean4game
+RUN npm install
+
+EXPOSE 3000
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 0000000..72dfc5f
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,5 @@
+{
+  "dockerComposeFile": "./docker-compose.yml",
+  "service": "nng4",
+  "workspaceFolder": "/NNG4"
+}
diff --git a/.devcontainer/docker-compose.yml b/.devcontainer/docker-compose.yml
new file mode 100644
index 0000000..416d4a3
--- /dev/null
+++ b/.devcontainer/docker-compose.yml
@@ -0,0 +1,14 @@
+version: "3.9"
+
+services:
+  nng4:
+    build:
+      context: .
+      dockerfile: Dockerfile
+    image: lean4-game-dev
+    container_name: lean4-develop
+    command: npm start
+    volumes:
+      - ..:/NNG4
+    ports:
+      - "3000:3000"
diff --git a/.vscode/tasks.json b/.vscode/tasks.json
new file mode 100644
index 0000000..6cc5dba
--- /dev/null
+++ b/.vscode/tasks.json
@@ -0,0 +1,15 @@
+{
+  "version": "2.0.0",
+  "tasks": [
+    {
+      "label": "lake: build",
+      "detail": "build lean files",
+      "type": "shell",
+      "command": "lake build",
+      "group": {
+        "kind": "build",
+        "isDefault": true
+      },
+    }
+  ]
+}