To install Docker CE, you can follow the installation instructions from the official documentation or (for Debian stable or Ubuntu ≥ 16.04) directly execute this script: bin/install-docker.sh

Follow one of the following approaches:

• https://docs.docker.com/docker-for-mac/install/ (Docker + docker-compose for macOS)
• https://docs.docker.com/docker-for-mac/docker-toolbox/ (alternative installation)

Follow one of the following approaches:

• https://docs.docker.com/docker-for-windows/install/ (Docker for Windows)
  (beware that this enable Hyper-V, which is incompatible with VirtualBox)
• https://docs.docker.com/toolbox/overview/ (Docker Toolbox for Windows)
  (legacy distribution using docker-machine and VirtualBox)

As the Docker daemon socket is owned by root, you will need to prepend all docker CLI commands by sudo. To do this automatically, a standard practice consists in adding the following alias in your ~/.bashrc file:

alias docker='sudo docker'

Warning: to avoid this, some tutorials on the web suggest instead to add your default Linux user to the docker group. Don't do this on your personal workstation, because this would amount to provide the default user with root permissions without sudo-like password prompt protection. (cf. doc)

The provided Docker images are useful for both:

1. Continous Integration for Coq-based projects (see the corresponding CI setup page)
2. Manual experiments: using Docker to easily fetch a image and use a given version of Coq (a stable release or the latest dev version)

The sequel of this section elaborates on the 2nd item.

A useful command to remember is the following one-liner:

docker run --rm -it coqorg/coq:dev rlwrap coqtop

which has the following outcome:

• it pulls from the Docker Hub registry the coqorg/coq:dev image (only the first time, subsequent executions of the same command will reuse the locally-available image);
• it creates a container from the image specification;
• it runs the container, overriding the default start program with rlwrap coqtop, enabling interactive mode (-i) and allocating a pseudo-TTY (-t) for more convenience;
• the option --rm tells the Docker Engine that the container should be removed when the started process (here, rlwrap) terminates (namely in this case, if one types the Ctrl+D keystroke).

First, check the list of supported versions in this table.

Then, run the desired version of Coq by typing the following command:

docker run -it coqorg/coq:$coq_version

(which is the same as docker run -it coqorg/coq:$coq_version bash --login).

This will run a container with an interactive Bash shell. Then type:

opam switch

(which will show the list of installed OPAM switches in the container).

From now on, usual opam 2.0 commands apply.

For example, to use the COMPILER_EDGE switch, you may type:

• either opam switch $COMPILER_EDGE,
• or eval $(opam env --switch=$COMPILER_EDGE --set-switch)

Beyond docker run, the following commands can be very useful:

• docker pull $image_name to fetch an image
  (this can be used to update a local image if it has been upgraded in the Docker registry)
• docker images to show the list of locally-available images;
• docker ps to show the list of running containers;
• docker ps -a to show the list of all containers;
• docker stop $container_name to stop a container;
• docker start -ai $container_name to start a stopped container and attach the terminal;
• docker rm $container_name to remove a container;
• docker rmi $image_name to remove a local image.

For more details, see the online doc.