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 want to take a look at the coq-community project templates, which incorporate a template to generate a Travis CI configuration with docker-coq + opam as well as Nix.

Finally, you may be interested in Guillaume Claret's blog article Continuous testing for Coq projects, which describes a complete Travis CI configuration for a typical Coq project, endowed with a .opam conf file.

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 Debian/APT 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)
• If you need to install some OPAM dependencies, make sure to:
  • Run opam update -y before installing OPAM packages with opam install -y …
• If you need to install some OPAM dependencies and your project contains some file project-name.opam specifying them, you should adapt the templates above as follows:
  • Replace the line opam install -y -v -j ${NJOBS} coq-mathcomp-ssreflect with:
    ( opam pin add -n -k path project-name . && opam install -y -v -j ${NJOBS} --deps-only project-name )
  • Replace the line ( coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make install ) with:
    opam install -y -v -j ${NJOBS} project-name.
• The Docker-Coq images contain the following environment variables:
  • NJOBS: "2",
  • OPAM_VERSION: self-explanatory,
  • 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

• See also Guillaume Claret's blog article Continuous testing for Coq projects (Travis CI config + .opam file).

• Some additional 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.