1 files changed, 43 insertions, 17 deletions

diff --git a/configure.ml b/configure.ml
index 490954eba..06aa5e766 100644
--- a/configure.ml
+++ b/configure.ml
@@ -16,7 +16,7 @@ let coq_macos_version = "8.7.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8791
 let state_magic = 58791
-let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
+let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
@@ -178,6 +178,20 @@ let which prog =
 let program_in_path prog =
   try let _ = which prog in true with Not_found -> false
 
+(** Choose a command among a list of candidates
+    (command name, mandatory arguments, arguments for this test).
+    Chooses the first one whose execution outputs a non-empty (first) line.
+    Dies with message [msg] if none is found. *)
+
+let select_command msg candidates =
+  let rec search = function
+    | [] -> die msg
+    | (p, x, y) :: tl ->
+      if fst (tryrun p (x @ y)) <> ""
+      then List.fold_left (Printf.sprintf "%s %s") p x
+      else search tl
+  in search candidates
+
 (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it
     a quoted path to camlpXo via -pp.  So we only quote camlpXo on not
     Windows, and warn on Windows if the path contains spaces *)
@@ -669,18 +683,32 @@ let natdynlinkflag =
 
 (** * OS dependent libraries *)
 
-let osdeplibs = "-cclib -lunix"
-
-let operating_system, osdeplibs =
+let operating_system =
   if starts_with arch "sun4" then
     let os, _ = run "uname" ["-r"] in
     if starts_with os "5" then
-      "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket"
+      "Sun Solaris "^os
     else
-      "Sun OS "^os, osdeplibs
+      "Sun OS "^os
   else
-    (try Sys.getenv "OS" with Not_found -> ""), osdeplibs
+    (try Sys.getenv "OS" with Not_found -> "")
 
+(** Num library *)
+
+(* since 4.06, the Num library is no longer distributed with OCaml (replaced
+   by Zarith)
+*)
+
+let check_for_numlib () =
+  if caml_version_nums >= [4;6;0] then
+    let numlib,_ = tryrun camlexec.find ["query";"num"] in
+    match numlib with
+    | ""  ->
+       die "Num library not installed, required for OCaml 4.06 or later"
+    | _   -> printf "You have the Num library installed. Good!\n"
+
+let numlib =
+  check_for_numlib ()
 
 (** * lablgtk2 and CoqIDE *)
 
@@ -714,11 +742,11 @@ let get_lablgtkdir () =
     else "", msg
   | None ->
     let msg = OCamlFind in
-    let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in
+    let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
       (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
-      let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in
+      let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
         let msg = Stdlib in
@@ -744,7 +772,7 @@ let check_lablgtk_version src dir = match src with
   if ans then printf "Warning: could not check the version of lablgtk2.\n";
   (ans, "an unknown version")
 | OCamlFind ->
-  let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in
+  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
   try
     let vi = List.map s2i (numeric_prefix_list v) in
     ([2; 16] <= vi, v)
@@ -801,7 +829,7 @@ let coqide_flags () =
   if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir;
   match coqide, arch with
     | "opt", "Darwin" when !Prefs.macintegration ->
-      let osxdir,_ = tryrun "ocamlfind" ["query";"lablgtkosx"] in
+      let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in
       if osxdir <> "" then begin
         lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
         idearchflags := "lablgtkosx.cma";
@@ -840,9 +868,10 @@ let strip =
 (** * md5sum command *)
 
 let md5sum =
-  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
-  then "md5 -q" else "md5sum"
-
+  select_command "Don’t know how to compute MD5 checksums…" [
+    "md5sum", [], [ "--version" ];
+    "md5", ["-q"], [ "-s" ; "''" ];
+  ]
 
 (** * Documentation : do we have latex, hevea, ... *)
 
@@ -988,7 +1017,6 @@ let print_summary () =
     pr "  Operating system            : %s\n" operating_system;
   pr "  Coq VM bytecode link flags  : %s\n" (String.concat " " vmbyteflags);
   pr "  Other bytecode link flags   : %s\n" custom_flag;
-  pr "  OS dependent libraries      : %s\n" osdeplibs;
   pr "  OCaml version               : %s\n" caml_version;
   pr "  OCaml binaries in           : %s\n" (esc camlbin);
   pr "  OCaml library in            : %s\n" (esc camllib);
@@ -1081,7 +1109,6 @@ let write_configml f =
   pr_s "cflags" cflags;
   pr_s "caml_flags" caml_flags;
   pr_s "best" best_compiler;
-  pr_s "osdeplibs" osdeplibs;
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
   pr_li "caml_version_nums" caml_version_nums;
@@ -1213,7 +1240,6 @@ let write_makefile f =
   pr "# Supplementary libs for some systems, currently:\n";
   pr "#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n";
   pr "#  . others     : -cclib -lunix\n";
-  pr "OSDEPLIBS=%s\n\n" osdeplibs;
   pr "# executable files extension, currently:\n";
   pr "#  Unix systems:\n";
   pr "#  Win32 systems : .exe\n";