[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>

9 files changed, 32 insertions, 12 deletions

diff --git a/dev/base_include b/dev/base_include
index 1f14fc2941..daee2d97c5 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,7 +29,6 @@
 #install_printer ppatom;;
 #install_printer ppwhd;;
 #install_printer ppvblock;;
-#install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
 #install_printer  (* substitution *) ppsubst;;
 
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index fd6ea9bb09..8eff2cf577 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -389,6 +389,7 @@ IF "%RUNSETUP%"=="Y" (
     -P libfontconfig1 ^

     -P gtk-update-icon-cache ^

     -P libtool,automake ^

+    -P libgmp-devel ^

     -P intltool ^

     -P bison,flex ^

     %EXTRAPACKAGES% ^

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index cc9fd13fdc..cde1d798a0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1006,6 +1006,7 @@ function make_ocaml_tools {
 
 function make_ocaml_libs {
   make_num
+  make_zarith
   make_findlib
   make_lablgtk
 }
@@ -1023,6 +1024,16 @@ function make_num {
   fi
 }
 
+function make_zarith {
+  make_ocaml
+  if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then
+    logn configure ./configure
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
 ##### OCAMLBUILD #####
 
 function make_ocamlbuild {
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
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 63071bba72..60618f6491 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -23,7 +23,6 @@ install_printer Top_printers.ppconstr_expr
 install_printer Top_printers.ppglob_constr
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
 install_printer Top_printers.ppnumtokunsigned
 install_printer Top_printers.ppnumtokunsignednat
 install_printer Top_printers.ppintset
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ea90e83a83..773170207e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,7 +80,6 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
-let ppbigint n = pp (str (Bigint.to_string n));;
 let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
 let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 65eab8daa3..b1bb5e4702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -53,7 +53,6 @@ val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
 val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
 
-val ppbigint : Bigint.bigint -> unit
 val ppnumtokunsigned : NumTok.Unsigned.t -> unit
 val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit