diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 3aee7fe..e768e0a 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -16,16 +16,7 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh - leanc --version; \ lake --version; -WORKDIR / +USER node + +WORKDIR /home/node 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 diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index a245237..90d7155 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,18 +1,20 @@ { "dockerComposeFile": "./docker-compose.yml", "service": "game", - "workspaceFolder": "/game", + "workspaceFolder": "/home/node/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 + // 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)", + // I don't know why I need this, but I did... + "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", "customizations": { "vscode": { "settings": { diff --git a/.devcontainer/docker-compose.yml b/.devcontainer/docker-compose.yml index 574f0d2..3dcf40c 100644 --- a/.devcontainer/docker-compose.yml +++ b/.devcontainer/docker-compose.yml @@ -2,11 +2,10 @@ version: "3.9" services: game: - user: root build: context: . dockerfile: Dockerfile volumes: - - ..:/game + - ..:/home/node/game ports: - "3000:3000"