Dev Container npm/node issues

[Trequetrum]

When I clone the GameSkeleton template and then start a Dev Container in Vs Code, I get the following error:

> lean4-game@0.1.0 start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client"

sh: 1: concurrently: not found

Attempting to update npm and node in order to install concurrently:

npm WARN tarball tarball data for lean4@[...] seems to be corrupted. Trying again.
...
npm ERR! code 1
npm ERR! git dep preparation failed

I don't have a lot of experience with Docker and Web Stack stuff, but I can't get this off the ground anymore. Any suggestions?

[joneugster]

I cherry-picked some fixes for this from the dev branch to main (see new v4.5.0-release)

That should get your dev-container working again, too.

You'll want to do one of

• reclone GameSkeleton
• in your game folder: git pull; then call rm -rf .lake/ lake-manifest.json && lake update -R; then "Rebuild Container Without Cache" in VSCode

(somehow the integrity-SHA for the lean4-vscode module changed for the version used here and that caused everything to fail)

Let me know if you experience any problems!

[Trequetrum]

So, even from a fresh download of the GameSkeleton, I'm still getting errors.

[265589 ms] onCreateCommand failed with exit code 1. Skipping any further user-provided commands.

[265597 ms] Exit code 1 [265602 ms] Command failed: /usr/share/code/code /home/treq/.vscode/extensions/ms-vscode-remote.remote-containers-0.338.1/dist/spec-node/devContainersSpecCLI.js run-user-commands --user-data-folder /home/treq/.config/Code/User/globalStorage/ms-vscode-remote.remote-containers/data --container-session-data-folder /tmp/devcontainers-1656a490-bc5e-487f-aa95-d80623b5ee101708807444032 --workspace-folder /home/treq/Dev_Current/lean4logicgame5 --id-label devcontainer.local_folder=/home/treq/Dev_Current/lean4logicgame5 --id-label devcontainer.config_file=/home/treq/Dev_Current/lean4logicgame5/.devcontainer/devcontainer.json --container-id ef7862971197b8f9bed017e0d5c470f0f51b537ff0f11e47fda51053b85c6f6d --log-level debug --log-format json --config /home/treq/Dev_Current/lean4logicgame5/.devcontainer/devcontainer.json --default-user-env-probe loginInteractiveShell --skip-non-blocking-commands true --prebuild false --stop-for-personalization true --remote-env REMOTE_CONTAINERS_IPC=/tmp/vscode-remote-containers-ipc-58940a6e-7b37-4d53-a62c-c972b729e4c8.sock --remote-env SSH_AUTH_SOCK=/tmp/vscode-ssh-auth-58940a6e-7b37-4d53-a62c-c972b729e4c8.sock --remote-env DISPLAY=:0 --remote-env REMOTE_CONTAINERS_DISPLAY_SOCK=/tmp/.X11-unix/X0 --remote-env REMOTE_CONTAINERS=true --mount-workspace-git-root --dotfiles-target-path ~/dotfiles [265602 ms] Exit code 1

And if I reopen the container:

Running the postStartCommand from devcontainer.json...

[3416 ms] Start: Run in container: /bin/sh -c cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start lean4-game@0.1.0 start

concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client" sh: 1: concurrently: not found

[3928 ms] postStartCommand failed with exit code 127. Skipping any further user-provided commands.