CI setup

Docker-Coq and CI setup

The provided Docker-Coq images can be used to easily setup CI for Coq-based projects. In particular, it is not needed anymore to recompile Coq at each test-build, and it is possible to install additional APT or OPAM packages using sudo apt-get or opam.

Travis CI config

The following two repos contain some Travis CI configuration template:

1. https://github.com/erikmd/docker-coq-travis-ci-demo-1
2. https://github.com/erikmd/docker-coq-travis-ci-demo-2

The former repo uses the docker run and docker exec commands, while the latter relies on docker build with a Dockerfile committed among the sources.

For additional documentation on using Docker with Travis CI, see e.g. this page.

Also, you might be interested in the coq-community project templates, which incorporates a template to generate a Travis CI configuration with docker-coq + opam as well as Nix.

GitLab CI config

The following two repos contain some GitLab CI configuration template:

1. https://gitlab.com/erikmd/docker-coq-gitlab-ci-demo-1
2. https://gitlab.com/erikmd/docker-coq-gitlab-ci-demo-2

The former repo uses GitLab CI's native Docker support (but uses no Docker CLI command) while the latter relies on docker build with a Dockerfile committed among the sources.

For comprehensive documentation on GitLab CI, see the following pages:

• https://docs.gitlab.com/ce/ci/
• https://docs.gitlab.com/ce/ci/yaml/
• https://docs.gitlab.com/ce/ci/docker/using_docker_build.html

Remarks

• The default working directory of the Docker-Coq images is /home/coq.
• If you need to install some dependencies, make sure to:
  • Run sudo apt-get update -y -q before installing packages with:
    sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q … (because the APT cache has been cleaned in the published images)
  • (Alternatively, you may use opam-depext as follows: sudo apt-get update -y -q && opam depext -i -y conf-gmp.1)
  • Also, run opam update -y before installing OPAM packages with opam install -y …
• The Docker-Coq images contain the following environment variables:
  • NJOBS: "2",
  • COMPILER: default switch name,
  • COMPILER_EDGE: secondary switch name (if applicable),
  • COQ_VERSION: self-explanatory,
  • COQ_EXTRA_OPAM: either "coq-bignums" or the empty string.
• If you need to use Coq with the bleeding-edge version of OCaml, select the COMPILER_EDGE switch using the appropriate opam 2.0 command as recalled in the page CLI usage.

Related links

• Other examples of templates, using both Nix and the docker-coq-travis-ci-demo-1 setup, are available in the templates/ directory of the coq-community/manifesto repository.
• If your project under test relies on math-comp, you might be interested in using the mathcomp/mathcomp or mathcomp/mathcomp-dev Docker images, which contain the opam package coq-mathcomp-character and its dependencies prebuilt.