aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/azure-opam.sh2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile20
-rw-r--r--dev/ci/user-overlays/08743-ejgallego-zarith.sh6
3 files changed, 20 insertions, 8 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 64936cd236..17d71ac52a 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -10,4 +10,4 @@ bash opam64/install.sh
opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing
eval "$(opam env)"
-opam install -y num ocamlfind dune ounit
+opam install -y num ocamlfind dune ounit zarith
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 67a8415891..78c8673299 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-08-18-V29"
+# CACHEKEY: "bionic_coq-V2020-08-28-V92"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -6,9 +6,14 @@ 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 stdlib and sphinx doc
@@ -35,10 +40,10 @@ ENV NJOBS="2" \
# Base opam is the set of base packages required by Coq
ENV COMPILER="4.05.0"
-# Common OPAM packages.
-# `num` does not have a version number as the right version to install varies
-# with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
+# Common OPAM packages, num to be removed once the migration to
+# micromega is complete, `num` also does not have a version number as
+# the right version to install varies with the compiler version.
+ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
BASE_ONLY_OPAM="elpi.1.11.0"
@@ -52,9 +57,10 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM
-# base+32bit switch
+# base+32bit switch, note the zarith hack
RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
- opam install $BASE_OPAM
+ i386 env CC='gcc -m32' opam install zarith.1.9.1 && \
+ opam install $BASE_OPAM
# EDGE switch
ENV COMPILER_EDGE="4.10.0" \
diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
new file mode 100644
index 0000000000..da1d30c1e9
--- /dev/null
+++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then
+
+ bignums_CI_REF=zarith
+ bignums_CI_GITURL=https://github.com/ejgallego/bignums
+
+fi