diff options
| -rw-r--r-- | INSTALL.md | 2 | ||||
| -rw-r--r-- | 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"); |