Deployment with Docker Compose

[aziis98]

I didn't find a way to easily self-host this project so I wrote the following basic Dockerfile and docker-compose for easily deploying this project to a server. The server uses bubblewrap to sandbox the lean server so the container needs to be privileged to run.

• Dockerfile

  FROM node:23-bookworm
  
  RUN apt update && apt upgrade -y
  RUN apt install -y bubblewrap
  
  WORKDIR /app
  
  # Install elan
  RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz && \
      ./elan-init -y
  
  ENV PATH="/root/.elan/bin:${PATH}"
  
  # Copy package files
  COPY package.json package-lock.json ./
  
  # Install dependencies
  RUN npm install
  
  # Copy project files
  COPY . .
  
  # Build the project
  RUN npm run build
  
  EXPOSE 8080
  
  # Set the entrypoint
  CMD ["npm", "run", "production"]
  

• docker-compose.yml

  services:
    lean4game:
      build: .
      privileged: true # needed to run bubblewrap inside docker
      environment:
        - LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
        - LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
      ports:
        - "8080:8080"
      volumes:
        - games_data:/app/games
  
  volumes:
    games_data:
  

I looked around a bit in the project and saw that previously you used docker for the server but then changed to bubblewrap. I don't know much about the history of the project and haven't found the reason for the change to that for sandboxing. Maybe it's the fact that this is already a demanding project and you think it's best to host it as a whole on a single VPS instance?

[abentkamp]

Using Docker for deployment and using Docker for sandboxing Lean are two different things, and I don't think you can use one container to do both. A container for deployment must include everything, including for instance the landing page. A container for sandboxing should only contain the Lean server of a single user, so that the user cannot manipulate for instance the landing page of other users.

The reasons for switching from Docker to bubblewrap for sandboxing were that (1) it was hard to automatically delete outdated Docker containers and they often filled up the disc and (2) bubblewrap allows us to enable memory sharing (mmap) between multiple Lean servers.

As you suspected, having everything on a single VPS instance is useful because it makes loading new games easier. But also, a single instance is simply what the university gave us to host the games.