Using Docker is more difficult than using our virtual machine. You should first try using the virtual machine and only use Docker if the VM is not usable or you are already familiar with Docker.

If you encounter problems you can always ask questions on our Discord.

Installing Docker

Windows/macOS:

• Install Docker Desktop: https://www.docker.com/products/docker-desktop/

Linux:

• Install Docker using your package manager (apt, pacman, etc…)

Using Dev Containers (Recommended)

1. Install VS Code locally

2. Extract the following zip file into your repository (or any directory you want to work in)

   devcontainer.zip

3. Make sure the .devcontainer directory lies at the root of your repository

Example:

📁 Documents
└─ 📁 a1-repo
   ├─ 📄 a1.c
   └─ 📁 .devcontainer
      ├─ devcontainer.json
      ├─ Dockerfile
      └─ entrypoint.sh

1. Open your repository in VS Code
2. Add .devcontainer to your .gitignore file
3. Open the VS Code prompt (Control/Command + Shift + p) and select Dev Containers: Reopen in Container

Using Docker directly (Advanced)

Download Dockerfile & entrypoint.sh