diff options
Diffstat (limited to 'configure.ml')
-rw-r--r-- | configure.ml | 169 |
1 files changed, 54 insertions, 115 deletions
diff --git a/configure.ml b/configure.ml index 3a55fb570..b8bb650b1 100644 --- a/configure.ml +++ b/configure.ml @@ -11,11 +11,11 @@ #load "str.cma" open Printf -let coq_version = "8.5beta3" -let coq_macos_version = "8.4.93" (** "[...] should be a string comprised of +let coq_version = "trunk" +let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of three non-negative, period-separed integers [...]" *) -let vo_magic = 8493 -let state_magic = 58503 +let vo_magic = 8511 +let state_magic = 58511 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] @@ -236,7 +236,7 @@ module Prefs = struct let docdir = ref (None : string option) let emacslib = ref (None : string option) let coqdocdir = ref (None : string option) - let camldir = 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) @@ -290,8 +290,8 @@ let args_options = Arg.align [ "<dir> Obsolete: same as -emacslib"; "-coqdocdir", arg_string_option Prefs.coqdocdir, "<dir> Where to install Coqdoc style files"; - "-camldir", arg_string_option Prefs.camldir, - "<dir> Specifies the path to the OCaml binaries"; + "-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, @@ -352,42 +352,18 @@ let _ = parse_args () (** Default OCaml binaries *) type camlexec = - { mutable byte : string; - mutable opt : string; + { mutable find : string; mutable top : string; - mutable mklib : string; - mutable dep : string; - mutable doc : string; - mutable lex : string; - mutable yacc : string } - -(* TODO: autodetect .opt binaries ? *) + mutable lex : string; } let camlexec = - { byte = "ocamlc"; - opt = "ocamlopt"; + { find = "ocamlfind"; top = "ocaml"; - mklib = "ocamlmklib"; - dep = "ocamldep"; - doc = "ocamldoc"; - lex = "ocamllex"; - yacc = "ocamlyacc" } - -let reset_caml_byte c o = c.byte <- o -let reset_caml_opt c o = c.opt <- o -let reset_caml_doc c o = c.doc <- o + lex = "ocamllex"; } + let reset_caml_lex c o = c.lex <- o -let reset_caml_dep c o = c.dep <- o - -let rebase_camlexec dir c = - c.byte <- Filename.concat dir c.byte; - c.opt <- Filename.concat dir c.opt; - c.top <- Filename.concat dir c.top; - c.mklib <- Filename.concat dir c.mklib; - c.dep <- Filename.concat dir c.dep; - c.doc <- Filename.concat dir c.doc; - c.lex <- Filename.concat dir c.lex; - c.yacc <- Filename.concat dir c.yacc +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 "" @@ -471,32 +447,28 @@ let browser = (** * OCaml programs *) let camlbin, caml_version, camllib = - let camlbin, camlc = match !Prefs.camldir with - | Some dir -> - rebase_camlexec dir camlexec; - Filename.dirname camlexec.byte, camlexec.byte - | None -> - try let camlc = which camlexec.byte in - let dir = Filename.dirname camlc in - if not arch_win32 then rebase_camlexec dir camlexec; (* win32: TOCHECK *) - dir, camlc - with Not_found -> - die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^ - "Please adjust your path or use the -camldir option of ./configure") + let () = match !Prefs.ocamlfindcmd with + | Some cmd -> reset_caml_find camlexec cmd + | None -> + try reset_caml_find camlexec (which camlexec.find) + with Not_found -> + die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.find ^ + "Please adjust your path or use the -ocamlfind option of ./configure") in - let camlcopt = camlc ^ ".opt" in - let camlc = - if is_executable camlcopt then begin - reset_caml_byte camlexec (camlexec.byte ^ ".opt"); - camlcopt - end - else if is_executable camlc then - camlc - else - die ("Error: cannot find the executable '"^camlc^"'.") in - let caml_version, _ = run camlc ["-version"] in - let camllib, _ = run camlc ["-where"] in - camlbin, caml_version, camllib + if not (is_executable camlexec.find) + then die ("Error: cannot find the executable '"^camlexec.find^"'.") + else + let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in + let camllib, _ = run camlexec.find ["printconf";"stdlib"] in + let camlbin = (* TODO beurk beurk beurk *) + Filename.dirname (Filename.dirname camllib) / "bin/" in + let () = + if is_executable (camlbin / "ocamllex") + then reset_caml_lex camlexec (camlbin / "ocamllex") in + let () = + if is_executable (camlbin / "ocaml") + then reset_caml_top camlexec (camlbin / "ocaml") in + camlbin, caml_version, camllib let camlp4compat = "-loc loc" @@ -544,12 +516,8 @@ let camltag = match caml_version_list with (* Convention: we use camldir as a prioritary location for camlpX, if given *) let which_camlpX base = - match !Prefs.camldir with - | Some dir -> - let file = Filename.concat dir base in - if is_executable file then file else which base - | None -> - which 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 *) @@ -646,40 +614,23 @@ let msg_no_dynlink_cmxa () = printf "and then run ./configure -natdynlink no\n" let check_native () = - if !Prefs.byteonly then raise Not_found; - let camloptopt = camlexec.opt ^ ".opt" in - if (is_executable camloptopt || program_in_path camloptopt) then - reset_caml_opt camlexec camloptopt - else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then - (msg_no_ocamlopt (); raise Not_found); - if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) then - (msg_no_camlpX_cmxa (); raise Not_found); - if not (Sys.file_exists (camllib/"dynlink.cmxa")) then - (msg_no_dynlink_cmxa (); raise Not_found); - let version, _ = run camlexec.opt ["-version"] in - if version <> caml_version then - printf - "Warning: Native and bytecode compilers do not have the same version!\n"; - printf "You have native-code compilation. Good!\n" + 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 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" let best_compiler = try check_native (); "opt" with Not_found -> "byte" -let _ = - let camllexopt = camlexec.lex ^ ".opt" in - if is_executable camllexopt || program_in_path camllexopt then - reset_caml_lex camlexec camllexopt - -let _ = - let camldepopt = camlexec.dep ^ ".opt" in - if is_executable camldepopt || program_in_path camldepopt then - reset_caml_dep camlexec camldepopt - -let _ = - let camldocopt = camlexec.doc ^ ".opt" in - if is_executable camldocopt || program_in_path camldocopt then - reset_caml_doc camlexec camldocopt - (** * Native dynlink *) let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt" @@ -862,14 +813,14 @@ let strip = if hasnatdynlink then "true" else "strip" else if !Prefs.profile || !Prefs.debug then "true" else begin - let _, all = run camlexec.byte ["-config"] in + let _, all = run camlexec.find ["ocamlc";"-config"] in let strip = String.concat "" (List.map (fun l -> match string_split ' ' l with | "ranlib:" :: cc :: _ -> (* on windows, we greb the right strip *) Str.replace_first (Str.regexp "ranlib") "strip" cc | _ -> "" ) all) in - if strip = "" then "stip" else strip + if strip = "" then "strip" else strip end (** * md5sum command *) @@ -1079,12 +1030,7 @@ let write_configml f = pr_o "datadir" datadir; pr_s "docdir" docdir; pr_s "ocaml" camlexec.top; - pr_s "ocamlc" camlexec.byte; - pr_s "ocamlopt" camlexec.opt; - pr_s "ocamlmklib" camlexec.mklib; - pr_s "ocamldep" camlexec.dep; - pr_s "ocamldoc" camlexec.doc; - pr_s "ocamlyacc" camlexec.yacc; + pr_s "ocamlfind" camlexec.find; pr_s "ocamllex" camlexec.lex; pr_s "camlbin" camlbin; pr_s "camllib" camllib; @@ -1168,13 +1114,8 @@ let write_makefile f = pr "VERSION4MACOS=%s\n\n" coq_macos_version; pr "# Objective-Caml compile command\n"; pr "OCAML=%S\n" camlexec.top; - pr "OCAMLC=%S\n" camlexec.byte; - pr "OCAMLMKLIB=%S\n" camlexec.mklib; - pr "OCAMLOPT=%S\n" camlexec.opt; - pr "OCAMLDEP=%S\n" camlexec.dep; - pr "OCAMLDOC=%S\n" camlexec.doc; + pr "OCAMLFIND=%S\n" camlexec.find; pr "OCAMLLEX=%S\n" camlexec.lex; - pr "OCAMLYACC=%S\n\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"; @@ -1184,8 +1125,6 @@ let write_makefile f = pr "# Ocaml .h directory\n"; pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; - pr "CAMLLINK=%S\n" camlexec.byte; - pr "CAMLOPTLINK=%S\n\n" camlexec.opt; pr "# Caml flags\n"; pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag; pr "# User compilation flag\n"; |