Imported Upstream version 8.5~beta3+dfsg

1 files changed, 26 insertions, 20 deletions

diff --git a/configure.ml b/configure.ml
index bbe43520..51033c3d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,11 +11,11 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.5beta2"
-let coq_macos_version = "8.4.92" (** "[...] should be a string comprised of
+let coq_version = "8.5beta3"
+let coq_macos_version = "8.4.93" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
-let vo_magic = 8591
-let state_magic = 58501
+let vo_magic = 8493
+let state_magic = 58503
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
@@ -252,7 +252,7 @@ module Prefs = struct
   let profile = ref false
   let annotate = ref false
   let makecmd = ref "make"
-  let nativecompiler = ref true
+  let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
   let coqwebsite = ref "http://coq.inria.fr/"
   let force_caml_version = ref false
 end
@@ -331,12 +331,12 @@ let args_options = Arg.align [
     " Dumps ml annotation files while compiling Coq";
   "-makecmd", Arg.Set_string Prefs.makecmd,
     "<command> Name of GNU Make command";
-  "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
-    " No compilation to native code for conversion and normalization";
+  "-native-compiler", arg_bool Prefs.nativecompiler,
+    "(yes|no) Compilation to native code for conversion and normalization";
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
     " URL of the coq website";
-  "-force-caml-version", arg_bool Prefs.force_caml_version,
-    " Force OCaml version";
+  "-force-caml-version", Arg.Set Prefs.force_caml_version,
+    "Force OCaml version";
 ]
 
 let parse_args () =
@@ -396,8 +396,7 @@ let coq_annotate_flag =
   then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
   else ""
 
-let cflags = "-Wall -Wno-unused"
-
+let cflags = "-Wall -Wno-unused -g -O2"
 
 (** * Architecture *)
 
@@ -477,7 +476,10 @@ let camlbin, caml_version, camllib =
     rebase_camlexec dir camlexec;
     Filename.dirname camlexec.byte, camlexec.byte
   | None ->
-    try let camlc = which camlexec.byte in Filename.dirname camlc, camlc
+    try let camlc = which camlexec.byte in
+        let dir = Filename.dirname camlc in
+        if not arch_win32 then rebase_camlexec dir camlexec; (* win32: TOCHECK *)
+        dir, camlc
     with Not_found ->
       die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^
            "Please adjust your path or use the -camldir option of ./configure")
@@ -514,7 +516,12 @@ let caml_version_nums =
 
 let check_caml_version () =
   if caml_version_nums >= [3;12;1] then
-    printf "You have OCaml %s. Good!\n" caml_version
+    if caml_version_nums = [4;2;0] && not !Prefs.force_caml_version then
+      die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^
+        "very slow compilation times. If you still want to use it, use \n" ^
+        "option -force-caml-version.\n")
+    else
+      printf "You have OCaml %s. Good!\n" caml_version
   else
     let () = printf "Your version of OCaml is %s.\n" caml_version in
     if !Prefs.force_caml_version then
@@ -839,12 +846,6 @@ let md5sum =
   if arch = "Darwin" then "md5 -q" else "md5sum"
 
 
-(** * md5sum command *)
-
-let md5sum =
-  if arch = "Darwin" then "md5 -q" else "md5sum"
-
-
 (** * Documentation : do we have latex, hevea, ... *)
 
 let check_doc () =
@@ -856,6 +857,9 @@ let check_doc () =
     if not !Prefs.withdoc then raise Not_found;
     if not (program_in_path "latex") then err "latex";
     if not (program_in_path "hevea") then err "hevea";
+    if not (program_in_path "hacha") then err "hacha";
+    if not (program_in_path "fig2dev") then err "fig2dev";
+    if not (program_in_path "convert") then err "convert";
     true
   with Not_found -> false
 
@@ -1200,7 +1204,9 @@ let write_makefile f =
   pr "# Defining REVISION\n";
   pr "CHECKEDOUT=%s\n\n" vcs;
   pr "# Option to control compilation and installation of the documentation\n";
-  pr "WITHDOC=%s\n" (if withdoc then "all" else "no");
+  pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no");
+  pr "# Option to produce precompiled files for native_compute\n";
+  pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else "");
   close_out o;
   Unix.chmod f 0o444