Split Docker images in two: one for base and one for edge.

The base image will use the old Ubuntu LTS (currently 20.04) and the edge image will use the most recent Ubuntu version (currently 23.04). We temporarily switch the dev job to use the base image because the documentation jobs depend on it, but should be tested with our minimal dependency version bounds.
Zimmi48 · Jul 4, 2023 · 7a8c08c · 7a8c08c
1 parent 12fe911
commit 7a8c08c
Show file tree

Hide file tree

Showing 7 changed files with 120 additions and 76 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -1,4 +1,4 @@
-image: "$IMAGE"
+image: $BASE_IMAGE
 
 include:
   - local: '/dev/ci/gitlab-modes/protected-mode.yml'
@@ -31,15 +31,16 @@ stages:
 
 # some default values
 variables:
-  # Format: bionic_coq-V$DATE-$hash
+  # Format: image_name-V$DATE-$hash
   # $DATE is so we can tell what's what in the image list
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
-  # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
-  CACHEKEY: "bionic_coq-V2023-06-29-2b9dca3152"
-  IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
+  # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
+  # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
+  BASE_CACHEKEY: "old_ubuntu_lts-V2023-06-30-71b0df09d5"
+  EDGE_CACHEKEY: "edge_ubuntu-V2023-06-30-7d5f52e473"
+  BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
+  EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
-  # By default, jobs run in the base switch; override to select another switch
-  OPAM_SWITCH: "base"
   # Used to select special compiler switches such as flambda, 32bits, etc...
   OPAM_VARIANT: ""
   GIT_DEPTH: "10"
@@ -50,9 +51,7 @@ before_script:
   - ulimit -s
   - ls -a # figure out if artifacts are around
   - printenv -0 | sort -z | tr '\0' '\n'
-  - declare -A switch_table
-  - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
-  - opam switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
+  - opam switch set -y "${COMPILER}${OPAM_VARIANT}"
   - eval $(opam env)
   - opam list
   - opam config list
@@ -99,21 +98,15 @@ before_script:
 
 # Developer build, with build layout. Faster and useful for those
 # jobs needing _build
-.build-template:dev:
+.build-template:base:dev:
   stage: build
   interruptible: true
   extends: .auto-use-tags
   script:
-    # flambda can be pretty stack hungry, specially with -O3
-    # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244
-    # and https://github.com/coq/coq/pull/11916#issuecomment-609977375
-    - ulimit -S -s 16384
     - make $DUNE_TARGET
     - find _build -name '*.vio' -exec rm -f {} \;
     - tar cfj _build.tar.bz2 _build
   variables:
-    OPAM_SWITCH: edge
-    OPAM_VARIANT: "+flambda"
     DUNE_TARGET: world
   artifacts:
     name: "$CI_JOB_NAME"
@@ -125,19 +118,16 @@ before_script:
       - user-contrib/Ltac2/dune
     expire_in: 1 month
 
-.dev-ci-template:
+.doc-template:
   stage: build
   interruptible: true
   extends: .auto-use-tags
   needs:
-    - build:edge+flambda:dev
+    - build:base:dev
   script:
     - ulimit -S -s 16384
     - tar xfj _build.tar.bz2
     - make "$DUNE_TARGET"
-  variables:
-    OPAM_SWITCH: edge
-    OPAM_VARIANT: "+flambda"
   artifacts:
     when: always
     name: "$CI_JOB_NAME"
@@ -214,10 +204,10 @@ before_script:
 
 .ci-template-flambda:
   extends: .ci-template
+  image: $EDGE_IMAGE
   needs:
     - build:edge+flambda
   variables:
-    OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
 
 .deploy-template:
@@ -234,6 +224,7 @@ before_script:
 
 .pkg:opam-template:
   stage: build
+  image: $EDGE_IMAGE
   interruptible: true
   extends: .auto-use-tags
   # OPAM will build out-of-tree so no point in importing artifacts
@@ -243,7 +234,6 @@ before_script:
     - opam pin add --kind=path coqide-server.dev .
     - opam pin add --kind=path coqide.dev .
   variables:
-    OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
   only: *full-ci
 
@@ -284,10 +274,10 @@ docker-boot:
   script:
     - dev/tools/check-cachekey.sh
     - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
-    - cd dev/ci/docker/bionic_coq/
-    - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
-    - docker build -t "$IMAGE" .
-    - docker push "$IMAGE"
+    - cd dev/ci/docker/old_ubuntu_lts
+    - if docker pull "$BASE_IMAGE"; then echo "Base image prebuilt!"; else docker build -t "$BASE_IMAGE" .; docker push "$BASE_IMAGE"; fi
+    - cd ../edge_ubuntu
+    - if docker pull "$EDGE_IMAGE"; then echo "Edge image prebuilt!"; else docker build -t "$EDGE_IMAGE" .; docker push "$EDGE_IMAGE"; fi
   except:
     variables:
       - $SKIP_DOCKER == "true"
@@ -298,6 +288,7 @@ build:base:
   extends: .build-template
   variables:
     COQ_EXTRA_CONF: "-native-compiler yes"
+  only: *full-ci
 
 # no coqide for 32bit: libgtk installation problems
 build:base+32bit:
@@ -310,14 +301,13 @@ build:base+32bit:
 
 build:edge+flambda:
   extends: .build-template
+  image: $EDGE_IMAGE
   variables:
-    OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
     COQ_EXTRA_CONF: "-native-compiler yes"
-  only: *full-ci
 
-build:edge+flambda:dev:
-  extends: .build-template:dev
+build:base:dev:
+  extends: .build-template:base:dev
 
 build:base+async:
   extends: .build-template
@@ -343,7 +333,7 @@ build:base+async:
   timeout: 1h 30min
 
 build:vio:
-  extends: .build-template:dev
+  extends: .build-template:base:dev
   variables:
     COQ_EXTRA_CONF: "-native-compiler no"
     COQ_DUNE_EXTRA_OPT: "-vio"
@@ -362,11 +352,11 @@ build:vio:
 
 lint:
   stage: build
+  image: $EDGE_IMAGE
   script: dev/lint-repository.sh
   extends: .auto-use-tags
   variables:
     GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
-    OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
 
 # pkg:opam:
@@ -425,7 +415,7 @@ pkg:nix:
     - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K
 
 doc:refman:
-  extends: .dev-ci-template
+  extends: .doc-template
   variables:
     DUNE_TARGET: refman-html
   artifacts:
@@ -434,7 +424,7 @@ doc:refman:
       - _build/default/doc/refman-html
 
 doc:refman-pdf:
-  extends: .dev-ci-template
+  extends: .doc-template
   variables:
     DUNE_TARGET: refman-pdf
   artifacts:
@@ -443,7 +433,7 @@ doc:refman-pdf:
       - _build/default/doc/refman-pdf
 
 doc:stdlib:
-  extends: .dev-ci-template
+  extends: .doc-template
   variables:
     DUNE_TARGET: stdlib-html
   artifacts:
@@ -479,7 +469,7 @@ doc:refman:deploy:
     - git push # TODO: rebase and retry on failure
 
 doc:ml-api:odoc:
-  extends: .dev-ci-template
+  extends: .doc-template
   variables:
     DUNE_TARGET: apidoc
   artifacts:
@@ -491,6 +481,7 @@ test-suite:base:
   extends: .test-suite-template
   needs:
     - build:base
+  only: *full-ci
 
 test-suite:base+32bit:
   extends: .test-suite-template
@@ -502,25 +493,21 @@ test-suite:base+32bit:
 
 test-suite:edge+flambda:
   extends: .test-suite-template
+  image: $EDGE_IMAGE
   needs:
     - build:edge+flambda
   variables:
-    OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
-  only: *full-ci
 
-test-suite:edge:dev:
+test-suite:base:dev:
   stage: build
   interruptible: true
   extends: .auto-use-tags
   needs:
-    - build:edge+flambda:dev
+    - build:base:dev
   script:
     - tar xfj _build.tar.bz2
     - make test-suite
-  variables:
-    OPAM_SWITCH: edge
-    OPAM_VARIANT: "+flambda"
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
@@ -542,8 +529,6 @@ test-suite:edge:dev:
     - eval $(opam env)
     - export COQ_UNIT_TEST=noop
     - make test-suite
-  variables:
-    OPAM_SWITCH: base
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: always
@@ -568,6 +553,7 @@ validate:base:
   extends: .validate-template
   needs:
     - build:base
+  only: *full-ci
 
 validate:base+32bit:
   extends: .validate-template
@@ -579,12 +565,11 @@ validate:base+32bit:
 
 validate:edge+flambda:
   extends: .validate-template
+  image: $EDGE_IMAGE
   needs:
     - build:edge+flambda
   variables:
-    OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
-  only: *full-ci
 
 validate:vio:
   extends: .validate-template

diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
@@ -107,8 +107,8 @@ Some important points:
   The first one uses the minimum version of OCaml supported by Coq.
   The second one uses the highest version of OCaml supported by Coq,
   with flambda enabled (currently it actually uses OCaml 4.14.1 as 5.0
-  has significant performance issues). See also the
-  [`Dockerfile`](docker/bionic_coq/Dockerfile) to find out what
+  has significant performance issues). See also the corresponding
+  [`Dockerfiles`](docker/) to find out what
   specific packages are available in each switch.
 
   If your job depends on other jobs, you must use the same opam

diff --git a/dev/ci/docker/edge_ubuntu/Dockerfile b/dev/ci/docker/edge_ubuntu/Dockerfile
@@ -0,0 +1,59 @@
+# Update CACHEKEY in the .gitlab-ci.yml when modifying this file.
+
+FROM ubuntu:23.04
+LABEL maintainer="e@x80.org"
+
+ENV DEBIAN_FRONTEND="noninteractive"
+
+# We need libgmp-dev:i386 for zarith; maybe we could also install GTK
+RUN dpkg --add-architecture i386
+
+RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
+        # Dependencies of the image, the test-suite and external projects
+        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
+        # Dependencies of ZArith
+        perl libgmp-dev libgmp-dev:i386 \
+        # Dependencies of lablgtk (for CoqIDE)
+        libgtksourceview-3.0-dev \
+        # Dependencies of Gappa
+        libboost1.81-all-dev libmpfr-dev autoconf-archive bison flex \
+        # Dependencies of source-doc and coq-makefile
+        texlive-latex-extra texlive-science tipa \
+        # Dependencies of HB (test suite)
+        wdiff \
+        # Required to get the wget step to succeed
+        ca-certificates \
+        # Required for fiat-crypto and Coqtail
+        python-is-python3
+
+# We need to install OPAM 2.0 manually for now.
+RUN wget https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+
+# Basic OPAM setup
+ENV NJOBS="2" \
+    OPAMJOBS="2" \
+    OPAMROOT=/root/.opamcache \
+    OPAMROOTISOK="true" \
+    OPAMYES="true"
+
+# Edge opam is the set of edge packages required by Coq
+ENV COMPILER="4.14.1" \
+    BASE_OPAM="zarith.1.11 ounit2.2.2.6" \
+    CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
+    BASE_OPAM_EDGE="dune.3.6.1 dune-build-info.3.6.1 dune-release.1.6.2 ocamlfind.1.9.5 odoc.2.1.1" \
+    CI_OPAM_EDGE="elpi.1.16.5 ppx_import.1.10.0 cmdliner.1.1.1 sexplib.v0.15.1 ppx_sexp_conv.v0.15.1 ppx_hash.v0.15.0 ppx_compare.v0.15.0 ppx_deriving_yojson.3.7.0 yojson.1.7.0 uri.4.2.0 ppx_yojson_conv.v0.15.1 ppx_inline_test.v0.15.1 ppx_assert.v0.15.0" \
+    COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.3"
+
+# EDGE+flambda switch, we install CI_OPAM as to be able to use
+# `ci-template-flambda` with everything.
+RUN opam init -a --disable-sandboxing --bare && eval $(opam env) && opam update && \
+    opam switch create "${COMPILER}+flambda" \
+      --repositories default,ocaml-beta=git+https://github.com/ocaml/ocaml-beta-repository.git \
+      --packages="ocaml-variants.${COMPILER}+options,ocaml-option-flambda" && eval $(opam env) && \
+    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM $CI_OPAM_EDGE
+
+
+RUN opam clean -a -c
+
+# set the locale for the benefit of Python
+ENV LANG C.UTF-8
diff --git a/dev/ci/docker/bionic_coq/Dockerfile → dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile → dev/ci/docker/old_ubuntu_lts/Dockerfile
@@ -1,6 +1,6 @@
 # Update CACHEKEY in the .gitlab-ci.yml when modifying this file.
 
-FROM ubuntu:bionic
+FROM ubuntu:20.04
 LABEL maintainer="e@x80.org"
 
 ENV DEBIAN_FRONTEND="noninteractive"
@@ -16,14 +16,16 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of lablgtk (for CoqIDE)
         libgtksourceview-3.0-dev \
         # Dependencies of Gappa
-        libboost1.65-all-dev libmpfr-dev autoconf-archive bison flex \
+        libboost1.67-all-dev libmpfr-dev autoconf-archive bison flex \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
         # Dependencies of source-doc and coq-makefile
         texlive-science tipa \
         # Dependencies of HB (test suite)
-        wdiff
+        wdiff \
+        # Required for fiat-crypto and Coqtail
+        python-is-python3
 
 # More dependencies of the sphinx doc, pytest for coqtail
 RUN pip3 install docutils==0.17.1 sphinx==4.5.0 sphinx_rtd_theme==1.0.0 \
@@ -63,19 +65,6 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
         i386 env CC='gcc -m32' opam install zarith.1.11 && \
         opam install $BASE_OPAM
 
-# EDGE switch
-ENV COMPILER_EDGE="4.14.1" \
-    BASE_OPAM_EDGE="dune.3.6.1 dune-build-info.3.6.1 dune-release.1.6.2 ocamlfind.1.9.5 odoc.2.1.1" \
-    CI_OPAM_EDGE="elpi.1.16.5 ppx_import.1.10.0 cmdliner.1.1.1 sexplib.v0.15.1 ppx_sexp_conv.v0.15.1 ppx_hash.v0.15.0 ppx_compare.v0.15.0 ppx_deriving_yojson.3.7.0 yojson.1.7.0 uri.4.2.0 ppx_yojson_conv.v0.15.1 ppx_inline_test.v0.15.1 ppx_assert.v0.15.0" \
-    COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.3"
-
-# EDGE+flambda switch, we install CI_OPAM as to be able to use
-# `ci-template-flambda` with everything.
-RUN opam switch create "${COMPILER_EDGE}+flambda" \
-      --repositories default,ocaml-beta=git+https://github.com/ocaml/ocaml-beta-repository.git \
-      --packages="ocaml-variants.${COMPILER_EDGE}+options,ocaml-option-flambda" && eval $(opam env) && \
-    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM $CI_OPAM_EDGE
-
 RUN opam clean -a -c
 
 # set the locale for the benefit of Python