build DUNE modules in parallel when building Docker images

.gitlab-ci.yml

@@ -98,21 +98,21 @@ dune:2.5:
 dune:git:
  stage: stage2
  script:
- - ./bin/duneci-build-docker-image --no-cache duneci/dune:git dune-git
+ - ./bin/duneci-build-docker-image --parallel --no-cache duneci/dune:git dune-git
  only:
  - master@ansgar/dune-docker
 
 dune-fufem:2.4:
  stage: stage3
  script:
- - ./bin/duneci-build-docker-image duneci/dune-fufem:2.4 dune-fufem
+ - ./bin/duneci-build-docker-image --parallel duneci/dune-fufem:2.4 dune-fufem
  only:
  - master@ansgar/dune-docker
 
 dune-fufem:git:
  stage: stage3
  script:
- - ./bin/duneci-build-docker-image --no-cache duneci/dune-fufem:git dune-fufem-git
+ - ./bin/duneci-build-docker-image --parallel --no-cache duneci/dune-fufem:git dune-fufem-git
  only:
  - master@ansgar/dune-docker
 

bin/duneci-build-docker-image

@@ -27,8 +27,14 @@ if [[ $# -lt 2 ]]; then
   usage
 fi
 
+parallel=
+
 while :; do
   case "${1}" in
+    --parallel)
+      parallel=1
+      shift
+      ;;
     -*)
       docker_opts+=("${1}")
       shift
@@ -41,6 +47,10 @@ done
 
 image="${1}"; shift
 
+if [[ -n "${parallel}" -a -v DUNECI_PARALLEL ]]; then
+  docker_opts+=(--build-arg=DUNECI_PARALLEL="${DUNECI_PARALLEL}")
+fi
+
 builddir="build/${image##*/}"
 if [[ -e ${builddir} ]]; then
   echo "E: ${builddir} already exists" >&2

dune-fufem-git/Dockerfile

 FROM duneci/dune:git
+ARG DUNECI_PARALLEL
 
 USER duneci
 WORKDIR /duneci/modules

dune-fufem/Dockerfile

 FROM duneci/dune:2.4
+ARG DUNECI_PARALLEL
 
 USER root
 WORKDIR /

dune-git/Dockerfile

 FROM duneci/base:9
+ARG DUNECI_PARALLEL
 
 USER duneci
 RUN duneci-install-module https://gitlab.dune-project.org/core/dune-common.git \