From 21366f8eab4ab9bd2c2af7a986b681704cd94c3f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 17 Sep 2020 17:32:16 +0200
Subject: [configure] Fix version checks for lablgtk and zarith

Fixes #13041 #13047

Configure is quite messy, but we will improve it once we can link it
with findlib and move to dune [that will actually allow to remove all
ad-hoc calls to `ocamlfind` in favor of `findlib` code.
---
 INSTALL.md   |  2 +-
 configure.ml | 24 ++++++++++++------------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/INSTALL.md b/INSTALL.md
index adc0f557ac..3d05fd65ab 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -32,7 +32,7 @@ To compile Coq yourself, you need:
 
 - for CoqIDE, the
   [lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library
-  (version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as
+  (version >= 3.1.0), and the corresponding GTK 3.x libraries, as
   of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18)
 
 The IEEE-754 compliance is required by primitive floating-point
diff --git a/configure.ml b/configure.ml
index 2dbc01651e..3bc912ef6a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -698,10 +698,16 @@ let check_for_numlib () =
       die "Num library not installed, required for OCaml 4.06 or later"
     | _   -> cprintf "You have the Num library installed. Good!");
   let zarith,_ = tryrun camlexec.find ["query";"zarith"] in
+  let zarith_version, _ = run camlexec.find ["query"; "zarith"; "-format"; "%v"] in
   match zarith with
   | ""  ->
     die "Zarith library not installed, required"
-  | _   -> cprintf "You have the Zarith library installed. Good!"
+  | _   ->
+    let zarith_version_int = List.map int_of_string (numeric_prefix_list zarith_version) in
+    if zarith_version_int >= [1;10;0] then
+      cprintf "You have the Zarith library %s installed. Good!" zarith_version
+    else
+      die ("Zarith version 1.10 is required, you have " ^ zarith_version)
 
 let numlib =
   check_for_numlib ()
@@ -717,20 +723,14 @@ let get_lablgtkdir () =
 
 let check_lablgtk_version () =
   let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
-  (true, v)
-
-(* ejgallego: we wait to do version checks until an official release is out *)
-(*  try
-    let vi = numeric_prefix_list v in
-    (* Temporary hack *)
-    if vi = ["3";"0";"beta3"] then (false, v) else
-    let vi = List.map s2i vi in
-    if vi < [3; 0; 0] then
+  try
+    let vl = numeric_prefix_list v in
+    let vn = List.map int_of_string vl in
+    if vn < [3; 1; 0] then
       (false, v)
     else
       (true, v)
   with _ -> (false, v)
-*)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -758,7 +758,7 @@ let check_coqide () =
   else
     let (ok, version) = check_lablgtk_version () in
     let found = sprintf "LablGtk3 and LablGtkSourceView3 found (%s)" version in
-    if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
+    if not ok then set_ide No (found^", but too old (required >= 3.1.0, found " ^ version ^ ")");
     (* We're now sure to produce at least one kind of coqide *)
     lablgtkdir := shorten_camllib dir;
     if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
-- 
cgit v1.2.3