From cb05a733533c28d4fc9bca5fba7e8d18ae549f97 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 10 Sep 2023 12:47:00 +0200
Subject: [PATCH] test

---
 .devcontainer/devcontainer.json |  6 ++++--
 .docker/gitpod/Dockerfile       | 11 ++++++++++-
 .gitpod.yml                     |  7 ++++---
 README.md                       | 31 +++++++++++++++++++++++++++++++
 4 files changed, 49 insertions(+), 6 deletions(-)

diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 8084f97..fb83b0f 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -13,8 +13,10 @@
   "overrideCommand": true,
   // TODO: `lake` and `npm install` could run simultaneously using `&`
   // the only reason I didn't do it is because the output gets mixed.
-  "postCreateCommand": "(cd ~/lean4game && npm install) && (cd ~/game && lake update && lake exe cache get && lake build)",
-  "postAttachCommand": "cd ~/lean4game && npm start",
+  "initializeCommand": "",
+  "onCreateCommand": "",
+  // "postCreateCommand": "(cd ~/lean4game && npm install) && (cd ~/game && lake update && lake exe cache get && lake build)",
+  // "postAttachCommand": "cd ~/lean4game && npm start",
   "customizations": {
     "vscode": {
       "settings": {
diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile
index ea458da..18b7797 100644
--- a/.docker/gitpod/Dockerfile
+++ b/.docker/gitpod/Dockerfile
@@ -2,12 +2,13 @@
 
 # gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
 # so we just install everything in one go
-FROM ubuntu:jammy
+FROM ubuntu:22.04
 
 USER root
 
 RUN apt-get update
 RUN apt-get install sudo git curl git bash-completion python3 -y
+RUN apt-get install npm
 RUN apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
@@ -35,5 +36,13 @@ ENV VSCODE_API_VERSION="1.50.0"
 # ssh to github once to bypass the unknown fingerprint warning
 RUN ssh -o StrictHostKeyChecking=no github.com || true
 
+# Lean4game specific stuff
+WORKDIR /workspace
+RUN git clone https://github.com/leanprover-community/lean4game.git
+WORKDIR /workspace/lean4game
+RUN npm install
+RUN npm start
+
+
 # run sudo once to suppress usage info
 RUN sudo echo finished
diff --git a/.gitpod.yml b/.gitpod.yml
index 5d8f97c..3199b78 100644
--- a/.gitpod.yml
+++ b/.gitpod.yml
@@ -1,12 +1,13 @@
 image:
-  file: ./Dockerfile
+  file: .devcontainer/Dockerfile
 
 vscode:
   extensions:
     - leanprover.lean4
 
 tasks:
+  - before: |
+      sudo apt-get --assume-yes install gcc
   - init: |
       lake exe cache get
-  - command: |
-      sudo apt-get --assume-yes install gcc
+  -
diff --git a/README.md b/README.md
index bc54379..802e47b 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,37 @@ This is the lean4 version of the classical *Natural Number Game*. It uses the [L
 
 The game was initially designed for lean3 and has been adapted for lean4. [See lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/).
 
+## Getting Started
+
+There are multiple ways to run the game locally:
+
+### Local setup
+
+### VSCode Devcontainer
+
+The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally).
+In particular, the recommended setup is to have `docker` installed on your computer
+and then click on the pop-up "Reopen in Container" which is shown when
+opening this project in VSCode.
+
+The game is then accessible at [localhost:3000/#/g/local/game](http://localhost:3000/#/g/local/game).
+
+### Codespaces
+
+If you open the repository in codespaces, it should open a
+"Simple Browser" which displays the game.
+
+#### Simple Browser
+
+To update the game, you have to run `lake build` in a terminal (make sure to be inside `~/game`).
+
+Afterwards you can reload the "Simple Browser". Unfortunately this seems to be extremely limited and will always put you back to the starting page.
+
+### Gitpod
+
+Not verified to work yet.
+
+
 ## Contributing
 
 If you want to contribute to the Natural Number Game, it is probably best if you ask us for access and push on a non-`main` branch in this repo. That way a github-action will build the game automatically.