From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- configure.ml | 99 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 49 insertions(+), 50 deletions(-) (limited to 'configure.ml') 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 [ " Where to install man files"; "-docdir", arg_string_option (fun p docdir -> { p with docdir }), " Where to install doc files"; - "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), - " Where to install emacs files"; "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), " 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" @@ -571,6 +575,9 @@ let camlbin, caml_version, camllib, findlib_version = let () = 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 @@ -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 -- cgit v1.2.3