Skip to content

CI setup

Jump to bottom
Erik Martin-Dorel edited this page Apr 26, 2020 · 23 revisions

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.

GitHub Actions config

A GitHub container action (compatible with docker-coq) is available at:

along with an example workflow:

For comprehensive documentation on GitHub Actions, see the following page:

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 templates project, 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:

Remarks

  • The default working directory of the Docker-Coq images is /home/coq.
  • The images are run with coq as default user with UID = GID = 1000 (along with sudo permissions). If this UID does not match that of your CI provider environment, you may want to change the permissions of the cloned working directory at the beginning of the script, e.g. by doing sudo chown -R coq: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

Clone this wiki locally