diff options
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 289 |
1 files changed, 169 insertions, 120 deletions
diff --git a/configure.ml b/configure.ml index bd6cb4805..c75c3d7e1 100644 --- a/configure.ml +++ b/configure.ml @@ -11,11 +11,11 @@ #load "str.cma" open Printf -let coq_version = "8.6.1" -let coq_macos_version = "8.6.1" (** "[...] should be a string comprised of +let coq_version = "trunk" +let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8600 -let state_magic = 58600 +let vo_magic = 8691 +let state_magic = 58691 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] @@ -251,7 +251,6 @@ module Prefs = struct 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 @@ -261,12 +260,17 @@ module Prefs = struct let withdoc = ref false let geoproof = ref false let byteonly = ref false - let debug = ref false + let debug = ref true let profile = ref false let annotate = ref false + (* Note, disabling this should be OK, but be careful with the + sharing invariants. + *) + let safe_string = 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 + let warn_error = ref false end (* TODO : earlier any option -foo was also available as --foo *) @@ -297,58 +301,69 @@ let args_options = Arg.align [ "-emacslib", arg_string_option Prefs.emacslib, "<dir> Where to install emacs files"; "-emacs", Arg.String (fun s -> - printf "Warning: obsolete -emacs option\n"; + prerr_endline "Warning: -emacs option is deprecated. Use -emacslib instead."; Prefs.emacslib := Some s), - "<dir> Obsolete: same as -emacslib"; + "<dir> Deprecated: same as -emacslib"; "-coqdocdir", arg_string_option Prefs.coqdocdir, "<dir> Where to install Coqdoc style files"; "-ocamlfind", arg_string_option Prefs.ocamlfindcmd, "<dir> Specifies the ocamlfind command to use"; "-lablgtkdir", arg_string_option Prefs.lablgtkdir, "<dir> 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"; + "-usecamlp5", Arg.Unit (fun () -> + prerr_endline "Warning: -usecamlp5 option is deprecated. Camlp5 is already a required dependency."), + " Deprecated: Camlp5 is a required dependency (Camlp4 is not supported anymore)"; "-camlp5dir", - Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s), + Arg.String (fun s -> Prefs.camlp5dir:=Some s), "<dir> Specifies where is the Camlp5 library and tells to use it"; "-arch", arg_string_option Prefs.arch, "<arch> Specifies the architecture"; - "-opt", Arg.Unit (fun () -> printf "Warning: obsolete -opt option\n"), - " Obsolete: native OCaml executables detected automatically"; + "-opt", Arg.Unit (fun () -> + prerr_endline "Warning: -opt option is deprecated. Native OCaml executables are detected automatically."), + " Deprecated: native OCaml executables detected automatically"; "-natdynlink", arg_bool Prefs.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"; + "(opt|byte|no) Specifies whether or not to compile CoqIDE"; "-nomacintegration", Arg.Clear Prefs.macintegration, - " Do not try to build coqide mac integration"; + " Do not try to build CoqIDE MacOS integration"; "-browser", arg_string_option Prefs.browser, "<command> Use <command> to open URL %s"; - "-nodoc", Arg.Clear Prefs.withdoc, - " Do not compile the documentation"; + "-nodoc", Arg.Unit (fun () -> + prerr_endline "Warning: -nodoc option is deprecated. Use -with-doc no instead."; + Prefs.withdoc := false), + " Deprecated: use -with-doc no instead"; "-with-doc", arg_bool Prefs.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, - " Compiles only bytecode version of Coq"; - "-debug", Arg.Set Prefs.debug, - " Add debugging information in the Coq executables"; + "-byteonly", Arg.Unit (fun () -> + prerr_endline "Warning: -byteonly option is deprecated. Use -byte-only instead."; + Prefs.byteonly := true), + " Deprecated: use -byte-only instead"; + "-debug", Arg.Unit (fun () -> + prerr_endline "Warning: -debug option is deprecated. Coq is compiled in debug mode by default."; + Prefs.debug := true), + " Deprecated: Coq is compiled in debug mode by default"; + "-nodebug", Arg.Clear Prefs.debug, + " Do not add debugging information in the Coq executables"; "-profile", Arg.Set Prefs.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"), - "<command> Obsolete: name of GNU Make command"; + "-makecmd", Arg.String (fun _ -> + prerr_endline "Warning: -makecmd option is deprecated and doesn't have any effect."), + "<command> Deprecated"; "-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.Set Prefs.force_caml_version, " Force OCaml version"; + "-warn-error", Arg.Set Prefs.warn_error, + " Make OCaml warnings into errors"; "-camldir", Arg.String (fun _ -> ()), "<dir> Specifies path to 'ocaml' for running configure script"; ] @@ -383,9 +398,12 @@ 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" + then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot" else "" +let coq_safe_string = + if !Prefs.safe_string then "-safe-string" else "" + let cflags = "-Wall -Wno-unused -g -O2" (** * Architecture *) @@ -418,11 +436,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 @@ -442,7 +460,7 @@ let vcs = let browser = 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 &" @@ -489,19 +507,14 @@ 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;1] then + 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 printf "*Warning* Your version of OCaml is outdated.\n" else - die "You need OCaml 4.01 or later." + die "You need OCaml 4.02.1 or later." let _ = check_caml_version () @@ -512,8 +525,31 @@ let camltag = match caml_version_list with | x::y::_ -> "OCAML"^x^y | _ -> assert false -let coq_warn_flag = - if caml_version_nums > [4;2;3] then "-w -3-52-56" else "" +(** 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 +*) +let coq_warn_flags = + let warnings = "-w +a-4-9-27-41-42-44-45-48-50" in + let errors = + if !Prefs.warn_error + then "-warn-error +a" + ^ (if caml_version_nums > [4;2;3] + then "-56" + else "") + else "" + in + warnings ^ " " ^ errors + + (** * CamlpX configuration *) @@ -540,8 +576,6 @@ let which_camlpX 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 | Some dir -> if Sys.file_exists (dir/testcma) then @@ -560,9 +594,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with 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 @@ -572,36 +604,15 @@ let check_camlp5_version camlp5o = printf "You have Camlp5 %s. Good!\n" 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 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" + "camlp5", "Camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version -let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX () +let camlpX, capitalized_camlpX, camlpXo, + camlpXbindir, fullcamlpXlibdir, + camlpXmod, camlpX_version = config_camlpX () let shorten_camllib s = if starts_with s (camllib^"/") then @@ -855,73 +866,91 @@ let withdoc = check_doc () 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 *) +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"; + Relative "bin", Relative "bin", Relative "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"); + Relative "lib", Relative "lib/coq", Relative ""; "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"); + Relative "config", Absolute "/etc/xdg/coq", Relative "ide"; "DATADIR", "the Coqide data files", Prefs.datadir, - (if unix then "/usr/local/share/coq" else "C:/coq/share"), - "/share/coq"; + Relative "share", Relative "share/coq", Relative "ide"; "MANDIR", "the Coq man pages", Prefs.mandir, - (if unix then "/usr/local/share/man" else "C:/coq/man"), - "/share/man"; + Relative "man", Relative "share/man", Relative "man"; "DOCDIR", "the Coq documentation", Prefs.docdir, - (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"), - "/share/doc/coq"; + Relative "doc", Relative "share/doc/coq", Relative "doc"; "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"); + Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; "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"); + 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) - -let do_one_noinst (var,msg,_,_,_) = - if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true) - else (var,msg,"",false) + if line = "" then (dflt,suffix) else (line,find_suffix p line) + in (var,msg,dir,suffix) -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 coqlib,coqlibsuffix = let (_,_,d,s) = select "COQLIBINSTALL" in d,s -let docdir = let (_,_,d,_) = select "DOCDIR" in d +let docdir,docdirsuffix = let (_,_,d,s) = select "DOCDIR" in d,s -let configdir = - let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None - -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 | Some b -> b @@ -941,7 +970,7 @@ let config_runtime () = | _ -> 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 () @@ -960,9 +989,9 @@ let print_summary () = 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 " %s version : %s\n" capitalized_camlpX camlpX_version; + pr " %s binaries in : %s\n" capitalized_camlpX camlpXbindir; + pr " %s library in : %s\n" capitalized_camlpX camlpXlibdir; if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then @@ -1019,18 +1048,22 @@ 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) + let pr_p s o = pr "let %s = %S\n" s + (match o with Relative s -> s | Absolute s -> s) 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 "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; @@ -1049,7 +1082,7 @@ let write_configml f = 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; @@ -1066,7 +1099,19 @@ let write_configml f = pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "no_native_compiler" (not !Prefs.nativecompiler); + + let core_src_dirs = [ "config"; "dev"; "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 api_dirs = [\"API\"; \"lib\"]\n"; pr "\nlet plugins_dirs = [\n"; + let plugins = Sys.readdir "plugins" in Array.sort compare plugins; Array.iter @@ -1075,6 +1120,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 @ api_dirs @ plugins_dirs\n"; + close_out o; Unix.chmod f 0o444 @@ -1111,6 +1159,7 @@ let write_makefile f = 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; @@ -1132,7 +1181,7 @@ 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 %s\n" coq_annotate_flag coq_warn_flag; + pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; |