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/build/windows/MakeCoq_MinGW.bat |  1 +
 dev/build/windows/makecoq_mingw.sh  | 11 +++++++++++
 2 files changed, 12 insertions(+)

(limited to 'dev/build')

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