From 094e4649c29e2426daca0476c140439de901dafe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 16 Oct 2018 14:55:30 +0200
Subject: [numeral] [plugins] Switch from `Big_int` to ZArith.

We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
---
 dev/ci/docker/bionic_coq/Dockerfile | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'dev/ci/docker/bionic_coq')

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" \
-- 
cgit v1.2.3