gitpod

.docker/gitpod/Dockerfile

@@ -8,7 +8,7 @@ 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 install gcc npm
 RUN apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
@@ -36,12 +36,5 @@ 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
-RUN mkdir -p /workspace
-WORKDIR /workspace
-RUN git clone https://github.com/leanprover-community/lean4game.git
-WORKDIR /workspace/lean4game
-RUN npm install
-
 # run sudo once to suppress usage info
 RUN sudo echo finished

.gitpod.yml

@@ -7,6 +7,8 @@ vscode:
 
 tasks:
   - before: |
-      sudo apt-get --assume-yes install gcc
+      cd /workspace && git clone https://github.com/leanprover-community/lean4game.git && cd lean4game && npm install
   - init: |
-      lake exe cache get
+      lake update && lake exe cache get && lake build
+  - command: |
+      cd /workspace/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start