CLI usage

Table of Contents

• Installing Docker
  • Under GNU/Linux (amd64)
  • Under macOS
  • Under Windows
  • Convenience config for GNU/Linux and macOS
• Using the Docker-Coq images
  • A useful one-liner
  • Selecting the version of Coq and OCaml
  • Other Docker commands
  • Tip: building a project on the host with a dockerized Coq

Installing Docker

Under GNU/Linux (amd64)

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

Under macOS

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)

Under Windows

Follow one of the following approaches:

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

Convenience config for GNU/Linux and macOS

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)

Using the Docker-Coq images

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 one-liner

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).

Selecting the version of Coq and OCaml

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)

Other Docker commands

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.

Tip: building a project on the host with a dockerized Coq

Docker allows one to bind-mount some directories or files from the host in containers. This can be used to build a project on the host. For example, assume that:

• the host machine contains a directory DIR=/home/user/Proj with some Coq theories and a _CoqProject file;
• the UID of user is 1000 (so there will be no permissions mismatch issue);

then we can build one such project with Coq 8.8 by typing:

docker run --rm -it -v $DIR:/tmp/foo -w /tmp/foo coqorg/coq:8.8 \
  bash --login -c "coq_makefile -f _CoqProject -o Makefile && make"