update workflow files and readme

.devcontainer/Dockerfile

@@ -2,21 +2,27 @@ FROM node:20
 
 WORKDIR /
 
-ENV ELAN_HOME=/usr/local/elan \
-  PATH=/usr/local/elan/bin:$PATH \
-  LEAN_VERSION=leanprover/lean4:v4.1.0
-  # TODO: read toolchain from `lean-toolchain`
-
-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;
+COPY ./lean-toolchain /lean-toolchain
 
 USER node
 
 WORKDIR /home/node
-RUN git clone https://github.com/leanprover-community/lean4game.git
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain | grep -oE '[^:]+$')" && git clone --depth 1 --branch $LEAN_VERSION https://github.com/leanprover-community/lean4game.git
+
+WORKDIR /
+
+USER root
+
+ENV ELAN_HOME=/usr/local/elan \
+  PATH=/usr/local/elan/bin:$PATH
+
+SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain)" && \
+  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;

.devcontainer/devcontainer.json

@@ -13,9 +13,9 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update && lake exe cache get && lake build)"
+    "lake_build": "(cd ~/game && lake clean && lake exe cache get && lake build)"
   },
-  "postStartCommand": "cd ~/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start",
+  "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {
     "vscode": {
       "settings": {

.devcontainer/docker-compose.yml

@@ -3,8 +3,8 @@ version: "3.9"
 services:
   game:
     build:
-      context: .
-      dockerfile: Dockerfile
+      context: ..
+      dockerfile: .devcontainer/Dockerfile
     volumes:
       - ..:/home/node/game
     ports:

README.md

@@ -1,60 +1,24 @@
 # NNG4
 
-This is the lean4 version of the classical *Natural Number Game*. It uses the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is running live at [adam.math.hhu.de](https://adam.math.hhu.de/#/game/nng).
+This is the lean4 version of the classical *Natural Number Game*. It uses
+the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is
+running live at [adam.math.hhu.de](https://adam.math.hhu.de).
 
 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 while developing it:
-
-### VSCode Devcontainer
-
-The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/doc/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.
-
-You can then open [localhost:3000](http://localhost:3000) in a browser.
-
-After making changes to the code, you need to run `lake build` in a terminal and
-reload the web page inside the "Simple Browser".
-
-### Codespaces
-
-You can work on it using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for for example under "Ports" and clicking on
-"Open in Browser".
-
-Note: You have to wait until `npm` started properly.
-In particular, this is after a message like
-`[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
-
-As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
-
-### Local setup
-
-The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/doc/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).
-
-### Gitpod
-
-You can work on this repository using Gitpod : [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/hhu-adam/NNG4)
-
-Note that gitpod is *not* setup to start the game in the background to play.
-
+You can develop the game as any lean project and use `lake build` to build it.
 
+Moreover, there are multiple ways to run the game while developing it, which are described in
+[Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
 
 ## 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.
-
-See the [documentation](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md) for an explanation of the game commands.
-
+PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!
 
-## Creating a new game
+## Documentation
 
-In order to create a new game, click "use this template"  above to create your own game. That way there is a github action that can build a docker image from your `main` branch which can be used to add the game to the server at [adam.math.hhu.de](https://adam.math.hhu.de).
+See [Creating a Game](https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md) at
+the [lean4game repo](https://github.com/leanprover-community/lean4game) for a detailed
+explanation.

lakefile.lean

@@ -1,34 +1,57 @@
 import Lake
 open Lake DSL
 
+-- Using this assumes that each dependency has a tag of the form `v4.X.0`.
+def leanVersion : String := s!"v{Lean.versionString}"
+
 def LocalGameServer : Dependency := {
   name := `GameServer
   src := Source.path "../lean4game/server"
 }
 
 def RemoteGameServer : Dependency := {
   name := `GameServer
-  src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
+  src := Source.git "https://github.com/leanprover-community/lean4game.git" leanVersion "server"
 }
 
-/- Choose dependency depending on the environment variable NODE_ENV -/
+/- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/
 open Lean in
 #eval (do
-  let gameServerName :=
-    if (← IO.getEnv "NODE_ENV") == some "development" then ``LocalGameServer else ``RemoteGameServer
+  let gameServerName := match (← IO.getEnv "LEAN4GAME") with
+    | none => ``RemoteGameServer
+    | some "" => ``RemoteGameServer
+    | some "local" => ``LocalGameServer
+    | some _ => panic "env var LEAN4GAME must be 'local' or unset."
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
-   : Elab.Command.CommandElabM Unit)
+  : Elab.Command.CommandElabM Unit)
+
+/-! # USER SECTION
+
+Below are all the dependencies the game needs. Add or remove packages here as you need them.
+
+Note: If your package (like `mathlib` or `Std`) has tags of the form `v4.X.0` then
+you can use `require mathlib from git "[URL]" @ leanVersion`
+ -/
+
+
+
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion
+
+
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "v4.1.0"
+/-! # END USER SECTION -/
 
 -- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
 -- off when calling `lake build`. Ideally there would be a better way using `logInfo` and
 -- an option like `lean4game.verbose`.
 package Game where
-  moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false",
+  moreLeanArgs := #[
+    "-Dtactic.hygienic=false",
+    "-Dlinter.unusedVariables.funArgs=false",
     "-Dtrace.debug=false"]
-  moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true",
+  moreServerArgs := #[
+    "-Dtactic.hygienic=false",
+    "-Dlinter.unusedVariables.funArgs=true",
     "-Dtrace.debug=true"]
   weakLeanArgs := #[]