diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-06 18:17:12 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-06 18:17:12 +0200 |
commit | cee82a36b21c7a87fe4f626d8d72fd938a825648 (patch) | |
tree | dc6179d2fdf1b90b9ad4a32b188e712336071653 /dev | |
parent | dad4731deed5c09e4e6cb212cd81462f7896c363 (diff) | |
parent | daa023eba8044404fbc708b7ae6172a918f1f18b (diff) |
Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CI
Diffstat (limited to 'dev')
-rwxr-xr-x | dev/ci/ci-compcert.sh | 1 | ||||
-rw-r--r-- | dev/ci/docker/README.md | 65 | ||||
-rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 45 | ||||
-rwxr-xr-x | dev/ci/docker/bionic_coq/hooks/post_push | 8 |
4 files changed, 118 insertions, 1 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fbdeff20c..8d490591b 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")" CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" -opam install -j "$NJOBS" -y menhir git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md new file mode 100644 index 000000000..8e677f6f2 --- /dev/null +++ b/dev/ci/docker/README.md @@ -0,0 +1,65 @@ +## Overall Docker Setup for Coq's CI. + +This directory provides Docker images to be used by Coq's CI. The +images do support Docker autobuild on `hub.docker.com` + +Autobuild is the preferred build method [see below]; if you are a +member of the `coqci` organization, the automated build will push the +image to the `coqci/name:$VERSION` tag using a Docker hub hook. + +## Updating the Image and Syncronization with CI files + +Unfortunately, at this point some manual synchronization is needed +between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the +checklist is: + +- check the name and version of the image setup in `hooks/post_push` + have to match. +- check `COMPILER` variables do match. + +Once you are sure the variables are right, then proceed to trigger an +autobuild or do a manual build, et voilà ! + +## Docker Autobuilding. + +We provide basic support for auto-building, see: + +https://docs.docker.com/docker-cloud/builds/advanced/ + +If you are member of the `coqci` Docker organization, trigger an +autobuild in your account and the image will be pushed to it as we +set the proper tag in `hooks/post_push`. + +We still need to figure out how properly setup a more automated, +organization-wide auto-building process. + +## Manual Building + +You can also manually build and push any image: + +- Build the image `docker build -t base:$VERSION .` + +To upload/push to your hub: + +- Create a https://hub.docker.com account. +- Login into your space `docker login --username=$USER` +- Push the image: + + `docker tag base:$VERSION $USER/base:$VERSION` + + `docker push $USER/base:$VERSION` + +Now your docker image is ready to be used. To upload to `coqci`: +- `docker tag base:$VERSION coqci/base:$VERSION` +- `docker push coqci/base:$VERSION` + +## Debugging / Misc + +To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` + +Each `RUN` command creates an "layer", thus a Docker build is +incremental and it always help to put things updated more often at the +end. + +## Possible Improvements: + +- Use ARG for customizing versions, centralize variable setup; +- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry . diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile new file mode 100644 index 000000000..5698175c5 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,45 @@ +FROM ubuntu:bionic +LABEL maintainer="e@x80.org" + +ENV DEBIAN_FRONTEND="noninteractive" + +RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ + libgtk2.0-dev libgtksourceview2.0-dev \ + texlive-latex-extra texlive-fonts-recommended hevea \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +RUN pip3 install antlr4-python3-runtime + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="true" + +ENV COMPILER="4.02.3" \ + BASE_OPAM="num ocamlfind jbuilder" + +RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update + +# Setup of the base switch +ENV CAMLP5_VER="6.14" \ + COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \ + CI_OPAM="menhir elpi ocamlgraph" + +RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + +# base+32bit switch +RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER + +# BE switch +ENV COMPILER_BE="4.06.1" \ + CAMLP5_VER_BE="7.05" \ + COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2" + +RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE + +# BE+flambda switch +RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push new file mode 100755 index 000000000..008ef1af3 --- /dev/null +++ b/dev/ci/docker/bionic_coq/hooks/post_push @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +COQCI_VERSION=V2018-05-05 +docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION +docker push $DOCKER_REPO:$COQCI_VERSION + +docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION +docker push coqci/base:$COQCI_VERSION |