From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- configure.ml | 872 ++++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 529 insertions(+), 343 deletions(-) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index 99f5ae54..5bbf0111 100644 --- a/configure.ml +++ b/configure.ml @@ -11,19 +11,21 @@ #load "str.cma" open Printf -let coq_version = "8.6" -let coq_macos_version = "8.6.00" (** "[...] should be a string comprised of +let coq_version = "8.8.2" +let coq_macos_version = "8.8.2" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8600 -let state_magic = 58600 -let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; +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 verbose = ref false (* for debugging this script *) (** * Utility functions *) - -let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1 +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 s2i = int_of_string let i2s = string_of_int @@ -107,7 +109,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 (printf "W: %s\n" msg; "", []) + if fatal then die msg else (cprintf "W: %s" msg; "", []) let tryrun prog args = run ~fatal:false ~err:DevNull prog args @@ -178,8 +180,22 @@ 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 + a quoted path to camlp5o via -pp. So we only quote camlp5o on not Windows, and warn on Windows if the path contains spaces *) let contains_suspicious_characters str = List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t'] @@ -189,7 +205,7 @@ let win_aware_quote_executable str = sprintf "%S" str else let _ = if contains_suspicious_characters str then - printf "*Warning* The string %S contains suspicious characters; ocamlfind might fail\n" str in + cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in Str.global_replace (Str.regexp "\\\\") "/" str (** * Date *) @@ -206,7 +222,7 @@ let get_date () = let year = 1900+now.Unix.tm_year in let month = months.(now.Unix.tm_mon) in sprintf "%s %d" month year, - sprintf "%s %d %d %d:%d:%d" (String.sub month 0 3) now.Unix.tm_mday year + sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec let short_date, full_date = get_date () @@ -221,6 +237,101 @@ let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755 type ide = Opt | Byte | No +type preferences = { + prefix : string option; + local : bool; + vmbyteflags : string option; + custom : bool option; + bindir : string option; + libdir : string option; + configdir : string option; + datadir : string option; + mandir : string option; + docdir : string option; + emacslib : string option; + coqdocdir : string option; + ocamlfindcmd : string option; + lablgtkdir : string option; + camlp5dir : string option; + arch : string option; + natdynlink : bool; + coqide : ide option; + macintegration : bool; + browser : string option; + withdoc : bool; + byteonly : bool; + flambda_flags : string list; + debug : bool; + profile : bool; + bin_annot : bool; + annot : bool; + bytecodecompiler : bool; + nativecompiler : bool; + coqwebsite : string; + force_caml_version : bool; + force_findlib_version : bool; + warn_error : bool; +} + +module Profiles = struct + +let default = { + prefix = None; + local = false; + vmbyteflags = None; + custom = None; + bindir = None; + libdir = None; + configdir = None; + datadir = None; + mandir = None; + docdir = None; + emacslib = None; + coqdocdir = None; + ocamlfindcmd = None; + lablgtkdir = None; + camlp5dir = None; + arch = None; + natdynlink = true; + coqide = None; + macintegration = true; + browser = None; + withdoc = false; + byteonly = false; + flambda_flags = []; + debug = true; + profile = false; + bin_annot = false; + annot = false; + bytecodecompiler = true; + nativecompiler = not (os_type_win32 || os_type_cygwin); + coqwebsite = "http://coq.inria.fr/"; + force_caml_version = false; + force_findlib_version = false; + warn_error = false; +} + +let devel state = { state with + local = true; + bin_annot = true; + annot = true; + warn_error = true; +} +let devel_doc = "-local -annot -bin-annot -warn-error yes" + +let get = function + | "devel" -> devel + | s -> raise (Arg.Bad ("profile name expected instead of "^s)) + +let doc = + " Sets a bunch of flags. Supported profiles: + devel = " ^ devel_doc + +end + +let prefs = ref Profiles.default + + let get_bool = function | "true" | "yes" | "y" | "all" -> true | "false" | "no" | "n" -> false @@ -232,123 +343,99 @@ let get_ide = function | "no" -> No | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s)) -let arg_bool r = Arg.String (fun s -> r := get_bool s) - -let arg_string_option r = Arg.String (fun s -> r := Some s) - -module Prefs = struct - let prefix = ref (None : string option) - let local = ref false - let vmbyteflags = ref (None : string option) - let custom = ref (None : bool option) - let bindir = ref (None : string option) - let libdir = ref (None : string option) - let configdir = ref (None : string option) - let datadir = ref (None : string option) - let mandir = ref (None : string option) - let docdir = ref (None : string option) - let emacslib = ref (None : string option) - let coqdocdir = ref (None : string option) - let ocamlfindcmd = ref (None : string option) - let lablgtkdir = ref (None : string option) - let usecamlp5 = ref true - let camlp5dir = ref (None : string option) - let arch = ref (None : string option) - let natdynlink = ref true - let coqide = ref (None : ide option) - let macintegration = ref true - let browser = ref (None : string option) - let withdoc = ref false - let geoproof = ref false - let byteonly = ref false - let debug = ref false - let profile = ref false - let annotate = ref false - let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) - let coqwebsite = ref "http://coq.inria.fr/" - let force_caml_version = ref false -end +let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s)) + +let arg_string f = Arg.String (fun s -> prefs := f !prefs s) +let arg_string_option f = Arg.String (fun s -> prefs := f !prefs (Some s)) +let arg_string_list c f = Arg.String (fun s -> prefs := f !prefs (string_split c s)) + +let arg_set f = Arg.Unit (fun () -> prefs := f !prefs true) +let arg_clear f = Arg.Unit (fun () -> prefs := f !prefs false) + +let arg_set_option f = Arg.Unit (fun () -> prefs := f !prefs (Some true)) +let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false)) + +let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s))) + +let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) let args_options = Arg.align [ - "-prefix", arg_string_option Prefs.prefix, + "-prefix", arg_string_option (fun p prefix -> { p with prefix }), " Set installation directory to "; - "-local", Arg.Set Prefs.local, + "-local", arg_set (fun p local -> { p with local }), " Set installation directory to the current source tree"; - "-vmbyteflags", arg_string_option Prefs.vmbyteflags, + "-vmbyteflags", arg_string_option (fun p vmbyteflags -> { p with vmbyteflags }), " Comma-separated link flags for the VM of coqtop.byte"; - "-custom", Arg.Unit (fun () -> Prefs.custom := Some true), + "-custom", arg_set_option (fun p custom -> { p with custom }), " Build bytecode executables with -custom (not recommended)"; - "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false), + "-no-custom", arg_clear_option (fun p custom -> { p with custom }), " Do not build with -custom on Windows and MacOS"; - "-bindir", arg_string_option Prefs.bindir, + "-bindir", arg_string_option (fun p bindir -> { p with bindir }), " Where to install bin files"; - "-libdir", arg_string_option Prefs.libdir, + "-libdir", arg_string_option (fun p libdir -> { p with libdir }), " Where to install lib files"; - "-configdir", arg_string_option Prefs.configdir, + "-configdir", arg_string_option (fun p configdir -> { p with configdir }), " Where to install config files"; - "-datadir", arg_string_option Prefs.datadir, + "-datadir", arg_string_option (fun p datadir -> { p with datadir }), " Where to install data files"; - "-mandir", arg_string_option Prefs.mandir, + "-mandir", arg_string_option (fun p mandir -> { p with mandir }), " Where to install man files"; - "-docdir", arg_string_option Prefs.docdir, + "-docdir", arg_string_option (fun p docdir -> { p with docdir }), " Where to install doc files"; - "-emacslib", arg_string_option Prefs.emacslib, + "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), " Where to install emacs files"; - "-emacs", Arg.String (fun s -> - printf "Warning: obsolete -emacs option\n"; - Prefs.emacslib := Some s), - " Obsolete: same as -emacslib"; - "-coqdocdir", arg_string_option Prefs.coqdocdir, + "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), " Where to install Coqdoc style files"; - "-ocamlfind", arg_string_option Prefs.ocamlfindcmd, + "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }), " Specifies the ocamlfind command to use"; - "-lablgtkdir", arg_string_option Prefs.lablgtkdir, + "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }), " Specifies the path to the Lablgtk library"; - "-usecamlp5", Arg.Set Prefs.usecamlp5, - " Specifies to use camlp5 instead of camlp4"; - "-usecamlp4", Arg.Clear Prefs.usecamlp5, - " Specifies to use camlp4 instead of camlp5"; - "-camlp5dir", - Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s), + "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }), " Specifies where is the Camlp5 library and tells to use it"; - "-arch", arg_string_option Prefs.arch, + "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }), + " Specifies additional flags to be passed to the flambda optimizing compiler"; + "-arch", arg_string_option (fun p arch -> { p with arch }), " Specifies the architecture"; - "-opt", Arg.Unit (fun () -> printf "Warning: obsolete -opt option\n"), - " Obsolete: native OCaml executables detected automatically"; - "-natdynlink", arg_bool Prefs.natdynlink, + "-natdynlink", arg_bool (fun p natdynlink -> { p with natdynlink }), "(yes|no) Use dynamic loading of native code or not"; - "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)), - "(opt|byte|no) Specifies whether or not to compile Coqide"; - "-nomacintegration", Arg.Clear Prefs.macintegration, - " Do not try to build coqide mac integration"; - "-browser", arg_string_option Prefs.browser, + "-coqide", arg_ide (fun p coqide -> { p with coqide }), + "(opt|byte|no) Specifies whether or not to compile CoqIDE"; + "-nomacintegration", arg_clear (fun p macintegration -> { p with macintegration }), + " Do not try to build CoqIDE MacOS integration"; + "-browser", arg_string_option (fun p browser -> { p with browser }), " Use to open URL %s"; - "-nodoc", Arg.Clear Prefs.withdoc, - " Do not compile the documentation"; - "-with-doc", arg_bool Prefs.withdoc, + "-with-doc", arg_bool (fun p withdoc -> { p with withdoc }), "(yes|no) Compile the documentation or not"; - "-with-geoproof", arg_bool Prefs.geoproof, - "(yes|no) Use Geoproof binding or not"; - "-byte-only", Arg.Set Prefs.byteonly, - " Compiles only bytecode version of Coq"; - "-byteonly", Arg.Set Prefs.byteonly, + "-byte-only", arg_set (fun p byteonly -> { p with byteonly }), " Compiles only bytecode version of Coq"; - "-debug", Arg.Set Prefs.debug, - " Add debugging information in the Coq executables"; - "-profile", Arg.Set Prefs.profile, + "-nodebug", arg_clear (fun p debug -> { p with debug }), + " 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.Set Prefs.annotate, - " Dumps ml annotation files while compiling Coq"; - "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"), - " Obsolete: name of GNU Make command"; - "-native-compiler", arg_bool Prefs.nativecompiler, + "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."), + " Deprecated. 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 }), + " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; + "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }), + "(yes|no) Enable Coq's bytecode reduction machine (VM)"; + "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }), "(yes|no) Compilation to native code for conversion and normalization"; - "-coqwebsite", Arg.Set_string Prefs.coqwebsite, + "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }), " URL of the coq website"; - "-force-caml-version", Arg.Set Prefs.force_caml_version, + "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }), " Force OCaml version"; + "-force-findlib-version", arg_set (fun p force_findlib_version -> { p with force_findlib_version }), + " Force findlib version"; + "-warn-error", arg_bool (fun p warn_error -> { p with warn_error }), + "(yes|no) Make OCaml warnings into errors (default no)"; + "-camldir", Arg.String (fun _ -> ()), + " Specifies path to 'ocaml' for running configure script"; + "-profile", arg_profile, + Profiles.doc ] let parse_args () = @@ -356,7 +443,7 @@ let parse_args () = args_options (fun s -> raise (Arg.Bad ("Unknown option: "^s))) "Available options for configure are:"; - if !Prefs.local && !Prefs.prefix <> None then + if !prefs.local && !prefs.prefix <> None then die "Options -prefix and -local are incompatible." let _ = parse_args () @@ -377,12 +464,14 @@ let reset_caml_lex c o = c.lex <- o let reset_caml_top c o = c.top <- o let reset_caml_find c o = c.find <- o -let coq_debug_flag = if !Prefs.debug then "-g" else "" -let coq_profile_flag = if !Prefs.profile then "-p" else "" -let coq_annotate_flag = - if !Prefs.annotate - then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes" - else "" +let coq_debug_flag = if !prefs.debug then "-g" else "" +let coq_profile_flag = if !prefs.profile then "-p" else "" +let coq_annot_flag = if !prefs.annot then "-annot" else "" +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 cflags = "-Wall -Wno-unused -g -O2" @@ -396,8 +485,8 @@ let arch_progs = ("/usr/ucb/arch", []) ] let query_arch () = - printf "I can not automatically find the name of your architecture.\n"; - printf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; + cprintf "I can not automatically find the name of your architecture."; + cprintf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; read_line () let rec try_archs = function @@ -407,7 +496,7 @@ let rec try_archs = function | _ :: rest -> try_archs rest | [] -> query_arch () -let arch = match !Prefs.arch with +let arch = match !prefs.arch with | Some a -> a | None -> let arch,_ = tryrun "uname" ["-s"] in @@ -416,11 +505,11 @@ let arch = match !Prefs.arch with else if arch <> "" then arch else try_archs arch_progs -(** NB: [arch_win32] is broader than [os_type_win32], cf. cygwin *) +(** NB: [arch_is_win32] is broader than [os_type_win32], cf. cygwin *) -let arch_win32 = (arch = "win32") +let arch_is_win32 = (arch = "win32") -let exe = exe := if arch_win32 then ".exe" else ""; !exe +let exe = exe := if arch_is_win32 then ".exe" else ""; !exe let dll = if os_type_win32 then ".dll" else ".so" (** * VCS @@ -435,19 +524,35 @@ let vcs = else if dir_exists "{arch}" then "gnuarch" else "none" +(** * Git Precommit Hook *) +let _ = + let f = ".git/hooks/pre-commit" in + if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin + cprintf "Creating pre-commit hook in %s" f; + let o = open_out f in + let pr s = fprintf o s in + pr "#!/bin/sh\n"; + pr "\n"; + pr "if [ -x dev/tools/pre-commit ]; then\n"; + pr " exec dev/tools/pre-commit\n"; + pr "fi\n"; + close_out o; + Unix.chmod f 0o775 + end + (** * Browser command *) let browser = - match !Prefs.browser with + match !prefs.browser with | Some b -> b - | None when arch_win32 -> "start %s" + | None when arch_is_win32 -> "start %s" | None when arch = "Darwin" -> "open %s" | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &" (** * OCaml programs *) -let camlbin, caml_version, camllib = - let () = match !Prefs.ocamlfindcmd with +let camlbin, caml_version, camllib, findlib_version = + let () = match !prefs.ocamlfindcmd with | Some cmd -> reset_caml_find camlexec cmd | None -> try reset_caml_find camlexec (which camlexec.find) @@ -458,6 +563,7 @@ let camlbin, caml_version, camllib = if not (is_executable camlexec.find) then die ("Error: cannot find the executable '"^camlexec.find^"'.") else + let findlib_version, _ = run camlexec.find ["query"; "findlib"; "-format"; "%v"] in let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in let camllib, _ = run camlexec.find ["printconf";"stdlib"] in let camlbin = (* TODO beurk beurk beurk *) @@ -468,9 +574,9 @@ let camlbin, caml_version, camllib = let () = if is_executable (camlbin / "ocaml") then reset_caml_top camlexec (camlbin / "ocaml") in - camlbin, caml_version, camllib + camlbin, caml_version, camllib, findlib_version -let camlp4compat = "-loc loc" +let camlp5compat = "-loc loc" (** Caml version as a list of string, e.g. ["4";"00";"1"] *) @@ -487,48 +593,104 @@ let caml_version_nums = "Is it installed properly?") let check_caml_version () = - if caml_version_nums >= [4;1;0] then - 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 + if caml_version_nums >= [4;2;3] then + cprintf "You have OCaml %s. Good!" caml_version else - let () = printf "Your version of OCaml is %s.\n" caml_version in - if !Prefs.force_caml_version then - printf "*Warning* Your version of OCaml is outdated.\n" + 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." else - die "You need OCaml 4.01 or later." + die "You need OCaml 4.02.3 or later." let _ = check_caml_version () -let coq_debug_flag_opt = - if caml_version_nums >= [3;10] then coq_debug_flag else "" +let findlib_version_list = numeric_prefix_list findlib_version -let camltag = match caml_version_list with - | x::y::_ -> "OCAML"^x^y - | _ -> assert false +let findlib_version_nums = + try + if List.length findlib_version_list < 2 then failwith "bad version"; + List.map s2i findlib_version_list + with _ -> + die ("I found ocamlfind but cannot read its version number!\n" ^ + "Is it installed properly?") +let check_findlib_version () = + if findlib_version_nums >= [1;4;1] then + cprintf "You have OCamlfind %s. Good!" 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." + else + die "You need OCamlfind 1.4.1 or later." -(** * CamlpX configuration *) +let _ = check_findlib_version () -(* Convention: we use camldir as a prioritary location for camlpX, if given *) +let camltag = match caml_version_list with + | x::y::_ -> "OCAML"^x^y + | _ -> assert false -let which_camlpX base = +(** Explanation of disabled warnings: + 4: fragile pattern matching: too common in the code and too annoying to avoid in general + 9: missing fields in a record pattern: too common in the code and not worth the bother + 27: innocuous unused variable: innocuous + 41: ambiguous constructor or label: too common + 42: disambiguated counstructor or label: too common + 44: "open" shadowing already defined identifier: too common, especially when some are aliases + 45: "open" shadowing a label or constructor: see 44 + 48: implicit elimination of optional arguments: too common + 50: unexpected documentation comment: too common and annoying to avoid + 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 + 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 + 59: "potential assignment to a non-mutable value": See Coq's issue #8043 +*) +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59" +let coq_warn_error = + if !prefs.warn_error + then "-warn-error +a" + ^ (if caml_version_nums > [4;2;3] + then "-56" + else "") + else "" + +(* 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 + +(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *) +let coq_caml_flags = + coq_warn_error + +(** * Camlp5 configuration *) + +(* Convention: we use camldir as a prioritary location for camlp5, if given *) +(* i.e., in the case of camlp5, we search for a copy of camlp5o which *) +(* answers the right camlp5 lib dir *) + +let strip_slash dir = + let n = String.length dir in + if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir + +let which_camlp5o_for camlp5lib = + let camlp5o = Filename.concat camlbin "camlp5o" in + let camlp5lib = strip_slash camlp5lib in + if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else + let camlp5o = which "camlp5o" in + if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else + die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) + +let which_camlp5 base = let file = Filename.concat camlbin base in if is_executable file then file else which base (* TODO: camlp5dir should rather be the *binary* location, just as camldir *) (* TODO: remove the late attempts at finding gramlib.cma *) -exception NoCamlp5 - -let check_camlp5 testcma = match !Prefs.camlp5dir with +let check_camlp5 testcma = match !prefs.camlp5dir with | Some dir -> if Sys.file_exists (dir/testcma) then let camlp5o = - try which_camlpX "camlp5o" + try which_camlp5o_for dir with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in dir, camlp5o else @@ -538,52 +700,28 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with in die msg | None -> try - let camlp5o = which_camlpX "camlp5o" in + let camlp5o = which_camlp5 "camlp5o" in let dir,_ = tryrun camlp5o ["-where"] in dir, camlp5o with Not_found -> - let () = printf "No Camlp5 installation found." in - let () = printf "Looking for Camlp4 instead...\n" in - raise NoCamlp5 + die "No Camlp5 installation found." let check_camlp5_version camlp5o = let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in - match string_split '.' version with + match numeric_prefix_list version with | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> - printf "You have Camlp5 %s. Good!\n" version; version + cprintf "You have Camlp5 %s. Good!" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" -let check_caml_version_for_camlp4 () = - if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then - die ("Your version of OCaml is detected to be 4.01.0 which fails to compile\n" ^ - "Coq in -debug mode with Camlp4. Remove -debug option or use a different\n" ^ - "version of OCaml or use Camlp5, or bypass this test by using option\n" ^ - "-force-caml-version.\n") - -let config_camlpX () = - try - if not !Prefs.usecamlp5 then raise NoCamlp5; +let config_camlp5 () = let camlp5mod = "gramlib" in let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in let camlp5_version = check_camlp5_version camlp5o in - "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version - with NoCamlp5 -> - (* We now try to use Camlp4, either by explicit choice or - by lack of proper Camlp5 installation *) - let camlp4mod = "camlp4lib" in - let camlp4libdir = camllib/"camlp4" in - if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then - die "No Camlp4 installation found.\n"; - try - let camlp4orf = which_camlpX "camlp4orf" in - let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in - let camlp4_version = List.nth (string_split ' ' version_line) 2 in - check_caml_version_for_camlp4 (); - "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version - with _ -> die "No Camlp4 installation found.\n" + camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version -let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX () +let camlp5o, camlp5bindir, fullcamlp5libdir, + camlp5mod, camlp5_version = config_camlp5 () let shorten_camllib s = if starts_with s (camllib^"/") then @@ -591,46 +729,46 @@ let shorten_camllib s = "+" ^ String.sub s l (String.length s - l) else s -let camlpXlibdir = shorten_camllib fullcamlpXlibdir +let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) let msg_byteonly () = - printf "Only the bytecode version of Coq will be available.\n" + cprintf "Only the bytecode version of Coq will be available." let msg_no_ocamlopt () = - printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly () + cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly () -let msg_no_camlpX_cmxa () = - printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly () +let msg_no_camlp5_cmxa () = + cprintf "Cannot find the native-code library of camlp5."; msg_byteonly () let msg_no_dynlink_cmxa () = - printf "Cannot find native-code dynlink library.\n"; msg_byteonly (); - printf "For building a native-code Coq, you may try to first\n"; - printf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)\n"; - printf "and then run ./configure -natdynlink no\n" + cprintf "Cannot find native-code dynlink library."; 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" let check_native () = - let () = if !Prefs.byteonly then raise Not_found in + let () = if !prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found - else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) - then let () = msg_no_camlpX_cmxa () in raise Not_found + else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) + then let () = msg_no_camlp5_cmxa () in raise Not_found else if fst (tryrun camlexec.find ["query";"dynlink"]) = "" then let () = msg_no_dynlink_cmxa () in raise Not_found else let () = if version <> caml_version then - printf - "Warning: Native and bytecode compilers do not have the same version!\n" - in printf "You have native-code compilation. Good!\n" + cprintf + "Warning: Native and bytecode compilers do not have the same version!" + in cprintf "You have native-code compilation. Good!" let best_compiler = try check_native (); "opt" with Not_found -> "byte" (** * Native dynlink *) -let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt" +let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt" let natdynlinkflag = if hasnatdynlink then "true" else "false" @@ -638,18 +776,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" + | _ -> cprintf "You have the Num library installed. Good!" +let numlib = + check_for_numlib () (** * lablgtk2 and CoqIDE *) @@ -663,7 +815,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 (printf "%s\n" msg; false) in + let yell msg = if fatal then die msg else (cprintf "%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) @@ -676,18 +828,18 @@ let check_lablgtkdir ?(fatal=false) src dir = (** Detect and/or verify the Lablgtk2 location *) let get_lablgtkdir () = - match !Prefs.lablgtkdir with + match !prefs.lablgtkdir with | Some dir -> let msg = Manual in if check_lablgtkdir ~fatal:true msg dir then dir, msg 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 @@ -699,24 +851,22 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - let test accu f = - if accu then - let test = sprintf "grep -q -w %s %S/glib.mli" f dir in - Sys.command test = 0 - else false - in - let heuristics = [ - "convert_with_fallback"; - "wrap_poll_func"; (** Introduced in lablgtk 2.16 *) - ] in - let ans = List.fold_left test true heuristics in - if ans then printf "Warning: could not check the version of lablgtk2.\n"; - (ans, "an unknown version") + cprintf "Warning: 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 "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) + if vi < [2; 16; 0] then + (false, v) + 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; + (true, "an unknown version") + end + else + (true, v) with _ -> (false, v) let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -725,11 +875,11 @@ exception Ide of ide (** If the user asks an impossible coqide, we abort the configuration *) -let set_ide ide msg = match ide, !Prefs.coqide with +let set_ide ide msg = match ide, !prefs.coqide with | No, Some (Byte|Opt) | Byte, Some Opt -> die (msg^":\n=> cannot build requested CoqIde") | _ -> - printf "%s:\n=> %s CoqIde will be built.\n" msg (pr_ide ide); + cprintf "%s:\n=> %s CoqIde will be built." msg (pr_ide ide); raise (Ide ide) let lablgtkdir = ref "" @@ -738,15 +888,15 @@ let lablgtkdir = ref "" This function also sets the lablgtkdir reference in case of success. *) let check_coqide () = - if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; + if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; let (ok, version) = check_lablgtk_version via dir in let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in - if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")"); + if not ok then set_ide No (found^", but too old (required >= 2.18.3, 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"); + if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler"); if not (Sys.file_exists (dir/"gtkThread.cmx")) then set_ide Byte (found^", but no native LablGtk2"); @@ -769,8 +919,8 @@ let idearchdef = ref "X11" 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 + | "opt", "Darwin" when !prefs.macintegration -> + let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; idearchflags := "lablgtkosx.cma"; @@ -795,7 +945,7 @@ let strip = if arch = "Darwin" then if hasnatdynlink then "true" else "strip" else - if !Prefs.profile || !Prefs.debug then "true" else begin + if !prefs.profile || !prefs.debug then "true" else begin let _, all = run camlexec.find ["ocamlc";"-config"] in let strip = String.concat "" (List.map (fun l -> match string_split ' ' l with @@ -806,106 +956,113 @@ let strip = if strip = "" then "strip" else strip end -(** * md5sum command *) - -let md5sum = - if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] - then "md5 -q" else "md5sum" - (** * Documentation : do we have latex, hevea, ... *) +let check_sphinx_deps () = + ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"]) + let check_doc () = let err s = - printf "%s was not found; documentation will not be available\n" s; - raise Not_found + die (sprintf "A documentation build was requested, but %s was not found." s); in - try - 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 - -let withdoc = check_doc () + if not (program_in_path "python3") then err "python3"; + if not (program_in_path "sphinx-build") then err "sphinx-build"; + check_sphinx_deps () +let _ = if !prefs.withdoc then check_doc () (** * Installation directories : bindir, libdir, mandir, docdir, etc *) let coqtop = Sys.getcwd () -let unix = os_type_cygwin || not arch_win32 +let unix = os_type_cygwin || not arch_is_win32 + +(** Variable name, description, ref in prefs, default dir, prefix-relative *) -(** Variable name, description, ref in Prefs, default dir, prefix-relative *) +type path_style = + | Absolute of string (* Should start with a "/" *) + | Relative of string (* Should not start with a "/" *) let install = [ - "BINDIR", "the Coq binaries", Prefs.bindir, - (if unix then "/usr/local/bin" else "C:/coq/bin"), - "/bin"; - "COQLIBINSTALL", "the Coq library", Prefs.libdir, - (if unix then "/usr/local/lib/coq" else "C:/coq/lib"), - (if arch_win32 then "" else "/lib/coq"); - "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, - (if unix then "/etc/xdg/coq" else "C:/coq/config"), - (if arch_win32 then "/config" else "/etc/xdg/coq"); - "DATADIR", "the Coqide data files", Prefs.datadir, - (if unix then "/usr/local/share/coq" else "C:/coq/share"), - "/share/coq"; - "MANDIR", "the Coq man pages", Prefs.mandir, - (if unix then "/usr/local/share/man" else "C:/coq/man"), - "/share/man"; - "DOCDIR", "the Coq documentation", Prefs.docdir, - (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"), - "/share/doc/coq"; - "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, - (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"), - (if arch_win32 then "/emacs" else "/share/emacs/site-lisp"); - "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, - (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"), - (if arch_win32 then "/latex" else "/share/emacs/site-lisp"); + "BINDIR", "the Coq binaries", !prefs.bindir, + Relative "bin", Relative "bin", Relative "bin"; + "COQLIBINSTALL", "the Coq library", !prefs.libdir, + Relative "lib", Relative "lib/coq", Relative ""; + "CONFIGDIR", "the Coqide configuration files", !prefs.configdir, + Relative "config", Absolute "/etc/xdg/coq", Relative "ide"; + "DATADIR", "the Coqide data files", !prefs.datadir, + Relative "share", Relative "share/coq", Relative "ide"; + "MANDIR", "the Coq man pages", !prefs.mandir, + 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"; ] -let do_one_instdir (var,msg,r,dflt,suff) = - let dir = match !r, !Prefs.prefix with - | Some d, _ -> d - | _, Some p -> p^suff - | _ -> +let strip_trailing_slash_if_any p = + if p.[String.length p - 1] = '/' then String.sub p 0 (String.length p - 1) else p + +let use_suffix prefix = function + | Relative "" -> prefix + | Relative suff -> prefix ^ "/" ^ suff + | Absolute path -> path + +let relativize = function + (* Turn a global layout based on some prefix to a relative layout *) + | Relative _ as suffix -> suffix + | Absolute path -> Relative (String.sub path 1 (String.length path - 1)) + +let find_suffix prefix path = match prefix with + | None -> Absolute path + | Some p -> + let p = strip_trailing_slash_if_any p in + let lpath = String.length path in + let lp = String.length p in + if lpath > lp && String.sub path 0 lp = p then + Relative (String.sub path (lp+1) (lpath - lp - 1)) + else + Absolute path + +let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = + let dir,suffix = + if !prefs.local then (use_suffix coqtop locallayout,locallayout) + else match uservalue, !prefs.prefix with + | Some d, p -> d,find_suffix p d + | _, Some p -> + let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in + use_suffix p suffix, suffix + | _, p -> + let suffix = if unix then unixlayout else selfcontainedlayout in + let base = if unix then "/usr/local" else "C:/coq" in + let dflt = use_suffix base suffix in let () = printf "Where should I install %s [%s]? " msg dflt in let line = read_line () in - if line = "" then dflt else line - in (var,msg,dir,dir<>dflt) + if line = "" then (dflt,suffix) else (line,find_suffix p line) + in (var,msg,dir,suffix) -let do_one_noinst (var,msg,_,_,_) = - if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true) - else (var,msg,"",false) - -let install_dirs = - let f = if !Prefs.local then do_one_noinst else do_one_instdir in - List.map f install +let install_dirs = List.map do_one_instdir install let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs -let libdir = let (_,_,d,_) = select "COQLIBINSTALL" in d - -let docdir = let (_,_,d,_) = select "DOCDIR" in d +let coqlib,coqlibsuffix = let (_,_,d,s) = select "COQLIBINSTALL" in d,s -let configdir = - let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None +let docdir,docdirsuffix = let (_,_,d,s) = select "DOCDIR" in d,s -let datadir = - let (_,_,d,b) = select "DATADIR" in if b then Some d else None +let configdir,configdirsuffix = let (_,_,d,s) = select "CONFIGDIR" in d,s +let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s (** * OCaml runtime flags *) (** Do we use -custom (yes by default on Windows and MacOS) *) -let custom_os = arch_win32 || arch = "Darwin" +let custom_os = arch_is_win32 || arch = "Darwin" -let use_custom = match !Prefs.custom with +let use_custom = match !prefs.custom with | Some b -> b | None -> custom_os @@ -915,18 +1072,19 @@ let build_loadpath = ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!" let config_runtime () = - match !Prefs.vmbyteflags with + match !prefs.vmbyteflags with | Some flags -> string_split ',' flags | _ when use_custom -> [custom_flag] - | _ when !Prefs.local -> + | _ when !prefs.local -> ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"] | _ -> let ld="CAML_LD_LIBRARY_PATH" in build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld; - ["-dllib";"-lcoqrun";"-dllpath";libdir] + ["-dllib";"-lcoqrun";"-dllpath";coqlib/"kernel/byterun"] let vmbyteflags = config_runtime () +let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s (** * Summary of the configuration *) @@ -938,32 +1096,32 @@ 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" camlbin; - pr " OCaml library in : %s\n" camllib; - pr " %s version : %s\n" (String.capitalize camlpX) camlpX_version; - pr " %s binaries in : %s\n" (String.capitalize camlpX) camlpXbindir; - pr " %s library in : %s\n" (String.capitalize camlpX) camlpXlibdir; + pr " OCaml binaries in : %s\n" (esc camlbin); + pr " OCaml library in : %s\n" (esc camllib); + pr " OCaml flambda flags : %s\n" (String.concat " " !prefs.flambda_flags); + pr " Camlp5 version : %s\n" camlp5_version; + pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); + pr " Camlp5 library in : %s\n" (esc camlp5libdir); if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then - pr " Lablgtk2 library in : %s\n" !lablgtkdir; + pr " Lablgtk2 library in : %s\n" (esc !lablgtkdir); if !idearchdef = "QUARTZ" then pr " Mac OS integration is on\n"; pr " CoqIde : %s\n" coqide; pr " Documentation : %s\n" - (if withdoc then "All" else "None"); + (if !prefs.withdoc then "All" else "None"); pr " Web browser : %s\n" browser; - pr " Coq web site : %s\n\n" !Prefs.coqwebsite; - if not !Prefs.nativecompiler then - pr " Native compiler for conversion and normalization disabled\n\n"; - if !Prefs.local then + pr " Coq web site : %s\n" !prefs.coqwebsite; + pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; + pr " Native Compiler enabled : %B\n\n" !prefs.nativecompiler; + if !prefs.local then pr " Local build, no installation...\n" else (pr " Paths for true installation:\n"; List.iter - (fun (_,msg,dir,_) -> pr " - %s will be copied in %s\n" msg dir) + (fun (_,msg,dir,_) -> pr " - %s will be copied in %s\n" msg (esc dir)) install_dirs); pr "\n"; pr "If anything is wrong above, please restart './configure'.\n\n"; @@ -977,21 +1135,20 @@ let _ = print_summary () let write_dbg_wrapper f = safe_remove f; - let o = open_out f in + let o = open_out_bin f in (* _bin to avoid adding \r on Cygwin/Windows *) let pr s = fprintf o s in pr "#!/bin/sh\n\n"; pr "###### ocamldebug-coq : a wrapper around ocamldebug for Coq ######\n\n"; pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n"; pr "export COQTOP=%S\n" coqtop; pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug"); - pr "CAMLP4LIB=%S\n\n" camlpXlibdir; + pr "CAMLP5LIB=%S\n\n" camlp5libdir; pr ". $COQTOP/dev/ocamldebug-coq.run\n"; close_out o; Unix.chmod f 0o555 let _ = write_dbg_wrapper "dev/ocamldebug-coq" - (** * Build the config/coq_config.ml file *) let write_configml f = @@ -1001,54 +1158,71 @@ let write_configml f = let pr_s = pr "let %s = %S\n" in let pr_b = pr "let %s = %B\n" in let pr_i = pr "let %s = %d\n" in - let pr_o s o = pr "let %s = %s\n" s - (match o with None -> "None" | Some d -> sprintf "Some %S" d) - in + let pr_p s o = pr "let %s = %S\n" s + (match o with Relative s -> s | Absolute s -> s) in + let pr_l n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) in + let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); - pr_b "local" !Prefs.local; + pr_b "local" !prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; - pr_o "coqlib" (if !Prefs.local then None else Some libdir); - pr_o "configdir" configdir; - pr_o "datadir" datadir; + pr_s "coqlib" coqlib; + pr_s "configdir" configdir; + pr_s "datadir" datadir; pr_s "docdir" docdir; + pr_p "coqlibsuffix" coqlibsuffix; + pr_p "configdirsuffix" configdirsuffix; + pr_p "datadirsuffix" datadirsuffix; + pr_p "docdirsuffix" docdirsuffix; pr_s "ocaml" camlexec.top; pr_s "ocamlfind" camlexec.find; pr_s "ocamllex" camlexec.lex; pr_s "camlbin" camlbin; pr_s "camllib" camllib; - pr_s "camlp4" camlpX; - pr_s "camlp4o" camlpXo; - pr_s "camlp4bin" camlpXbindir; - pr_s "camlp4lib" camlpXlibdir; - pr_s "camlp4compat" camlp4compat; + pr_s "camlp5o" camlp5o; + pr_s "camlp5bin" camlp5bindir; + pr_s "camlp5lib" camlp5libdir; + pr_s "camlp5compat" camlp5compat; 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; pr_s "date" short_date; pr_s "compile_date" full_date; pr_s "arch" arch; - pr_b "arch_is_win32" arch_win32; + pr_b "arch_is_win32" arch_is_win32; pr_s "exec_extension" exe; pr_s "coqideincl" !lablgtkincludes; pr_s "has_coqide" coqide; pr "let gtk_platform = `%s\n" !idearchdef; pr_b "has_natdynlink" hasnatdynlink; pr_s "natdynlinkflag" natdynlinkflag; + pr_l "flambda_flags" !prefs.flambda_flags; pr_i "vo_magic_number" vo_magic; pr_i "state_magic_number" state_magic; - pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; - pr_s "wwwcoq" !Prefs.coqwebsite; - pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); - pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); - pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); + pr_s "wwwcoq" !prefs.coqwebsite; + pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/"); + pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/refman/"); + pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); - pr_b "no_native_compiler" (not !Prefs.nativecompiler); + pr_b "bytecode_compiler" !prefs.bytecodecompiler; + pr_b "native_compiler" !prefs.nativecompiler; + + let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; + "engine"; "pretyping"; "interp"; "parsing"; "proofs"; + "tactics"; "toplevel"; "printing"; "intf"; + "grammar"; "ide"; "stm"; "vernac" ] in + let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") + "" + core_src_dirs in + + pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs; pr "\nlet plugins_dirs = [\n"; + let plugins = Sys.readdir "plugins" in Array.sort compare plugins; Array.iter @@ -1057,6 +1231,9 @@ let write_configml f = if Sys.is_directory f' && f.[0] <> '.' then pr " %S;\n" f') plugins; pr "]\n"; + + pr "\nlet all_src_dirs = core_src_dirs @ plugins_dirs\n"; + close_out o; Unix.chmod f 0o444 @@ -1090,9 +1267,10 @@ let write_makefile f = pr "#Variable used to detect whether ./configure has run successfully.\n"; pr "COQ_CONFIGURED=yes\n\n"; pr "# Local use (no installation)\n"; - pr "LOCAL=%B\n\n" !Prefs.local; + pr "LOCAL=%B\n\n" !prefs.local; pr "# Bytecode link flags : should we use -custom or not ?\n"; pr "CUSTOM=%s\n" custom_flag; + pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); pr "%s\n\n" !build_loadpath; pr "# Paths for true installation\n"; List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs; @@ -1114,22 +1292,23 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag; + pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; + (* XXX make this configurable *) + pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !prefs.flambda_flags); pr "# Flags for GCC\n"; pr "CFLAGS=%s\n\n" cflags; pr "# Compilation debug flags\n"; pr "CAMLDEBUG=%s\n" coq_debug_flag; - pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag_opt; + pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag; pr "# Compilation profile flag\n"; pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag; - pr "# Camlp4 : flavor, binaries, libraries ...\n"; - pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n"; - pr "CAMLP4=%s\n" camlpX; - pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo); - pr "CAMLP4COMPAT=%s\n" camlp4compat; - pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir; + pr "# Camlp5 : flavor, binaries, libraries ...\n"; + pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n"; + pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o); + pr "CAMLP5COMPAT=%s\n" camlp5compat; + pr "MYCAMLP5LIB=%S\n\n" camlp5libdir; pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; @@ -1137,7 +1316,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"; @@ -1149,8 +1327,6 @@ let write_makefile f = pr "# Unix systems and profiling: true\n"; pr "# Unix systems and no profiling: strip\n"; pr "STRIP=%s\n\n" strip; - pr "#the command md5sum\n"; - pr "MD5SUM=%s\n\n" md5sum; pr "# LablGTK\n"; pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; @@ -1163,9 +1339,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\n" (if withdoc then "all" else "no"); + 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 "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 @@ -1197,3 +1373,13 @@ let write_macos_metadata exec = let () = if arch = "Darwin" then List.iter write_macos_metadata distributed_exec + +let write_configpy f = + safe_remove f; + let o = open_out f in + let pr s = fprintf o s in + let pr_s = pr "%s = '%s'\n" in + pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n"; + pr_s "version" coq_version + +let _ = write_configpy "config/coq_config.py" -- cgit v1.2.3