fix devcontainer to not write files as root

.devcontainer/Dockerfile

@@ -22,4 +22,10 @@ RUN git clone https://github.com/leanprover-community/lean4game.git
 WORKDIR /lean4game
 RUN npm install
 
+# For some reason `node:node` results in 1000:1000, but user `node` has UID 30000...??
+# TODO: This alone takes 2min for me. can we refactor this so that `npm install` is already
+# run as the `node` user
+WORKDIR /
+RUN chown -R 30000:30003 /lean4game
+
 EXPOSE 3000

.devcontainer/devcontainer.json

@@ -3,6 +3,16 @@
   "service": "game",
   "workspaceFolder": "/game",
   "forwardPorts": [3000],
+  // These settings make sure that the created files (lake-packages etc.) are owned
+  // by the user and not `root`.
+  // see also https://containers.dev/implementors/json_reference/
+  // // and https://code.visualstudio.com/remote/advancedcontainers/add-nonroot-user
+  "remoteUser": "node",
+  "overrideCommand": true,
+  "updateRemoteUserUID": true,
+  // TODO: A problem with this setup is that the cache file is downloaded newly every time
+  // can we use the global cache storage? or already download it when creating the docker image?
+  "postAttachCommand": "(cd /game && lake update && lake exe cache get && lake build) && (cd /lean4game && npm start)",
   "customizations": {
     "vscode": {
       "settings": {

.devcontainer/docker-compose.yml

@@ -2,10 +2,10 @@ version: "3.9"
 
 services:
   game:
+    user: root
     build:
       context: .
       dockerfile: Dockerfile
-    command: bash -c "(cd /game && lake update && lake build) && npm start"
     volumes:
       - ..:/game
     ports: