test

.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": {

.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

.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
+  -

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.