Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 49 insertions, 50 deletions

diff --git a/configure.ml b/configure.ml
index 5bbf0111..4b468c7e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,21 +11,29 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.8.2"
-let coq_macos_version = "8.8.2" (** "[...] should be a string comprised of
+let coq_version = "8.9.0"
+let coq_macos_version = "8.9.0" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
-let vo_magic = 8800
-let state_magic = 58800
-let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
-"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
+let vo_magic = 8900
+let state_magic = 58900
+let distributed_exec =
+  ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
+   "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
 
+let red, yellow, reset =
+  if Unix.isatty Unix.stdout && Unix.isatty Unix.stderr && Sys.os_type = "Unix"
+  then "\027[31m", "\027[33m", "\027[0m"
+  else "", "", ""
+
 (** * Utility functions *)
 let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc
 let cprintf s = cfprintf stdout s
 let ceprintf s = cfprintf stderr s
-let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1
+let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1
+
+let warn s = kfprintf (fun oc -> cfprintf oc "%s" reset) stdout ("%sWarning: " ^^ s) yellow
 
 let s2i = int_of_string
 let i2s = string_of_int
@@ -109,7 +117,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args =
       let cmd = String.concat " " (prog::args) in
       let exn = match e with Failure s -> s | _ -> Printexc.to_string e in
       let msg = sprintf "Error while running '%s' (%s)" cmd exn in
-      if fatal then die msg else (cprintf "W: %s" msg; "", [])
+      if fatal then die msg else (warn "%s" msg; "", [])
 
 let tryrun prog args = run ~fatal:false ~err:DevNull prog args
 
@@ -205,7 +213,7 @@ let win_aware_quote_executable str =
     sprintf "%S" str
   else
     let _ = if contains_suspicious_characters str then
-      cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in
+      warn "The string %S contains suspicious characters; ocamlfind might fail" str in
     Str.global_replace (Str.regexp "\\\\") "/" str
 
 (** * Date *)
@@ -227,12 +235,6 @@ let get_date () =
 
 let short_date, full_date = get_date ()
 
-
-(** Create the bin/ directory if non-existent *)
-
-let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755
-
-
 (** * Command-line parsing *)
 
 type ide = Opt | Byte | No
@@ -248,7 +250,6 @@ type preferences = {
   datadir : string option;
   mandir : string option;
   docdir : string option;
-  emacslib : string option;
   coqdocdir : string option;
   ocamlfindcmd : string option;
   lablgtkdir : string option;
@@ -286,7 +287,6 @@ let default = {
   datadir = None;
   mandir = None;
   docdir = None;
-  emacslib = None;
   coqdocdir = None;
   ocamlfindcmd = None;
   lablgtkdir = None;
@@ -384,8 +384,6 @@ let args_options = Arg.align [
     "<dir> Where to install man files";
   "-docdir", arg_string_option (fun p docdir -> { p with docdir }),
     "<dir> Where to install doc files";
-  "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }),
-    "<dir> Where to install emacs files";
   "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }),
     "<dir> Where to install Coqdoc style files";
   "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }),
@@ -414,8 +412,8 @@ let args_options = Arg.align [
     " Do not add debugging information in the Coq executables";
   "-profiling", arg_set (fun p profile -> { p with profile }),
     " Add profiling information in the Coq executables";
-  "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."),
-    " Deprecated. Please use -annot or -bin-annot instead";
+  "-annotate", Arg.Unit (fun () -> die "-annotate has been removed. Please use -annot or -bin-annot instead."),
+    " Removed option. Please use -annot or -bin-annot instead";
   "-annot", arg_set (fun p annot -> { p with annot }),
     " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)";
   "-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }),
@@ -453,14 +451,19 @@ let _ = parse_args ()
 type camlexec =
  { mutable find : string;
    mutable top : string;
-   mutable lex : string; }
+   mutable lex : string;
+   mutable yacc : string;
+  }
 
 let camlexec =
   { find = "ocamlfind";
     top = "ocaml";
-    lex = "ocamllex"; }
+    lex = "ocamllex";
+    yacc = "ocamlyacc";
+  }
 
 let reset_caml_lex c o = c.lex <- o
+let reset_caml_yacc c o = c.yacc <- o
 let reset_caml_top c o = c.top <- o
 let reset_caml_find c o = c.find <- o
 
@@ -472,6 +475,7 @@ let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
 (* This variable can be overriden only for debug purposes, use with
    care. *)
 let coq_safe_string = "-safe-string"
+let coq_strict_sequence = "-strict-sequence"
 
 let cflags = "-Wall -Wno-unused -g -O2"
 
@@ -572,6 +576,9 @@ let camlbin, caml_version, camllib, findlib_version =
       if is_executable (camlbin / "ocamllex")
       then reset_caml_lex camlexec (camlbin / "ocamllex") in
     let () =
+      if is_executable (camlbin / "ocamlyacc")
+      then reset_caml_yacc camlexec (camlbin / "ocamlyacc") in
+    let () =
       if is_executable (camlbin / "ocaml")
       then reset_caml_top camlexec (camlbin / "ocaml") in
     camlbin, caml_version, camllib, findlib_version
@@ -598,7 +605,7 @@ let check_caml_version () =
   else
     let () = cprintf "Your version of OCaml is %s." caml_version in
     if !prefs.force_caml_version then
-      cprintf "*Warning* Your version of OCaml is outdated."
+      warn "Your version of OCaml is outdated."
     else
       die "You need OCaml 4.02.3 or later."
 
@@ -620,7 +627,7 @@ let check_findlib_version () =
   else
     let () = cprintf "Your version of OCamlfind is %s." findlib_version in
     if !prefs.force_findlib_version then
-      cprintf "*Warning* Your version of OCamlfind is outdated."
+      warn "Your version of OCamlfind is outdated."
     else
       die "You need OCamlfind 1.4.1 or later."
 
@@ -655,7 +662,7 @@ let coq_warn_error =
 
 (* Flags used to compile Coq and plugins (via coq_makefile) *)
 let caml_flags =
-  Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string
+  Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence
 
 (* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
 let coq_caml_flags =
@@ -733,17 +740,17 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir
 
 (** * Native compiler *)
 
-let msg_byteonly () =
-  cprintf "Only the bytecode version of Coq will be available."
+let msg_byteonly =
+  "Only the bytecode version of Coq will be available."
 
 let msg_no_ocamlopt () =
-  cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly ()
+  warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly
 
 let msg_no_camlp5_cmxa () =
-  cprintf "Cannot find the native-code library of camlp5."; msg_byteonly ()
+  warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly
 
 let msg_no_dynlink_cmxa () =
-  cprintf "Cannot find native-code dynlink library."; msg_byteonly ();
+  warn "Cannot find native-code dynlink library.\n%s" msg_byteonly;
   cprintf "For building a native-code Coq, you may try to first";
   cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
   cprintf "and then run ./configure -natdynlink no"
@@ -759,8 +766,7 @@ let check_native () =
   else
     let () =
       if version <> caml_version then
-        cprintf
-          "Warning: Native and bytecode compilers do not have the same version!"
+        warn "Native and bytecode compilers do not have the same version!"
     in cprintf "You have native-code compilation. Good!"
 
 let best_compiler =
@@ -815,7 +821,7 @@ let get_source = function
 (** Is some location a suitable LablGtk2 installation ? *)
 
 let check_lablgtkdir ?(fatal=false) src dir =
-  let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in
+  let yell msg = if fatal then die msg else (warn "%s" msg; false) in
   let msg = get_source src in
   if not (dir_exists dir) then
     yell (sprintf "No such directory '%s' (%s)." dir msg)
@@ -851,7 +857,7 @@ let get_lablgtkdir () =
 
 let check_lablgtk_version src dir = match src with
 | Manual | Stdlib ->
-  cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+  warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
   (true, "an unknown version")
 | OCamlFind ->
   let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
@@ -862,7 +868,11 @@ let check_lablgtk_version src dir = match src with
     else if vi < [2; 18; 3] then
       begin
         (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
-        cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v;
+        warn "Your installed lablgtk reports as %s.\n\
+It is possible that the installed version is actually more recent\n\
+but reports an incorrect version. If the installed version is\n\
+actually more recent than 2.18.3, that's fine; if it is not,\n
+CoqIDE will compile but may be very unstable." v;
         (true, "an unknown version")
       end
     else
@@ -997,8 +1007,6 @@ let install = [
     Relative "man", Relative "share/man", Relative "man";
   "DOCDIR", "the Coq documentation", !prefs.docdir,
     Relative "doc", Relative "share/doc/coq", Relative "doc";
-  "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib,
-    Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools";
   "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir,
     Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc";
  ]
@@ -1214,7 +1222,7 @@ let write_configml f =
 
   let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library";
                         "engine"; "pretyping"; "interp"; "parsing"; "proofs";
-                        "tactics"; "toplevel"; "printing"; "intf";
+                        "tactics"; "toplevel"; "printing";
                         "grammar"; "ide"; "stm"; "vernac" ] in
   let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
                                     ""
@@ -1239,17 +1247,6 @@ let write_configml f =
 
 let _ = write_configml "config/coq_config.ml"
 
-(** * Symlinks or copies for the checker *)
-
-let _ =
-  let prog, args, prf =
-    if arch = "win32" then "cp", [], ""
-    else "ln", ["-s"], "../" in
-  List.iter (fun file ->
-    ignore(run "rm" ["-f"; "checker/"^file]);
-    ignore(run ~fatal:true prog (args @ [prf^"kernel/"^file;"checker/"^file])))
-  [ "esubst.ml"; "esubst.mli"; "names.ml"; "names.mli" ]
-
 (** * Build the config/Makefile file *)
 
 let write_makefile f =
@@ -1282,6 +1279,7 @@ let write_makefile f =
   pr "OCAML=%S\n" camlexec.top;
   pr "OCAMLFIND=%S\n" camlexec.find;
   pr "OCAMLLEX=%S\n" camlexec.lex;
+  pr "OCAMLYACC=%S\n" camlexec.yacc;
   pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
   pr "BEST=%s\n\n" best_compiler;
   pr "# Ocaml version number\n";
@@ -1342,6 +1340,7 @@ let write_makefile f =
   pr "WITHDOC=%s\n\n" (if !prefs.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 "");
+  pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else "");
   close_out o;
   Unix.chmod f 0o444