12 Docker

12.1 install and clean

sudo apt -y install docker.io

Then you need to add your acount into docker group

## you may need to relogin to let it effect
sudo usermod -a -G docker $USER

Docker image takes a lot of space, so remember to clean periodically.

docker system prune
docker rmi `docker images -f "dangling=true" -q`

12.2 container (docker run)

  • -dt keeps the container running in the background
  • --rm automatically remove the container
  • --restart unless-stopped restart the container when you restart OS
  • after mount, existing files’ user keeps unchanged, while new files belongs to user in the container (usually root). In other words, files produced by the container is very hard to manipulate on host OS.

12.3 Dockerfile

  • empty image: https://hub.docker.com/_/scratch
  • apt RUN apt update && apt -y install wget && rm -r /var/lib/apt/lists/
  • use environment variable for private information 15
    1. in Dockerfile: ARG GITHUB_PAT
    2. in docker build, add --build-arg GITHUB_PAT=${GITHUB_PAT

  1. The technique is firstly used for evading GitHub API limit in installing R packages.↩︎