Skip to content

Commit

Permalink
[configure] Fix version checks for lablgtk and zarith
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
ejgallego committed Sep 17, 2020
1 parent 14f0e50 commit 21366f8
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 13 deletions.
2 changes: 1 addition & 1 deletion INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
24 changes: 12 additions & 12 deletions configure.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand All @@ -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"

Expand Down Expand Up @@ -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");
Expand Down

0 comments on commit 21366f8

Please sign in to comment.