From 293746e7d709436a8e0ec94b8eb2e972ac0efde6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Feb 2014 16:34:12 +0100 Subject: Fix compilation of coq and plugins using coq_makefile under cygwin Problems: - strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config the value of "ranlinb" and replace ranlib by strip obtaining "i686-bla-strip" from "i686-bla-ranlib" - coq_makefile was not quoting the plugins/ paths - coq_makefile was quoting twice camlpX (the shell of cygwin was confused) --- configure.ml | 64 +++++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 40 insertions(+), 24 deletions(-) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index 5488904a1..1c037269d 100644 --- a/configure.ml +++ b/configure.ml @@ -8,6 +8,7 @@ You could also use our wrapper ./configure *) #load "unix.cma" +#load "str.cma" open Printf let coq_version = "trunk" @@ -47,12 +48,19 @@ let rec waitpid_non_intr pid = (** Below, we'd better read all lines on a channel before closing it, otherwise a SIGPIPE could be encountered by the sub-process *) -let read_first_line_and_close fd = +let read_lines_and_close fd = let cin = Unix.in_channel_of_descr fd in - let line = try remove_final_cr (input_line cin) with End_of_file -> "" in - (try while true do ignore (input_line cin) done with End_of_file -> ()); + let lines = ref [] in + begin + try + while true do + lines := remove_final_cr (input_line cin) :: !lines + done + with End_of_file -> () + end; close_in cin; - line + let lines = List.rev !lines in + try List.hd lines, lines with Failure _ -> "", [] (** Run some unix command and read the first line of its output. We avoid Unix.open_process and its non-fully-portable /bin/sh, @@ -80,17 +88,17 @@ let run ?(fatal=true) ?(err=StdErr) prog args = let pid = Unix.create_process prog argv Unix.stdin out_w fd_err in let () = Unix.close out_w in let () = Unix.close nul_w in - let line = read_first_line_and_close out_r in - let _ = read_first_line_and_close nul_r in + let line, all = read_lines_and_close out_r in + let _ = read_lines_and_close nul_r in let () = check_exit_code (waitpid_non_intr pid) in - line + line, all with - | _ when not fatal && not !verbose -> "" + | _ when not fatal && not !verbose -> "", [] | e -> 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 (printf "W: %s\n" msg; "", []) let tryrun prog args = run ~fatal:false ~err:DevNull prog args @@ -395,7 +403,7 @@ let query_arch () = let rec try_archs = function | (prog,args)::rest when is_executable prog -> - let arch = tryrun prog args in + let arch, _ = tryrun prog args in if arch <> "" then arch else try_archs rest | _ :: rest -> try_archs rest | [] -> query_arch () @@ -405,7 +413,7 @@ let os_type_cygwin = (Sys.os_type = "Cygwin") let arch = match !Prefs.arch with | Some a -> a | None -> - let arch = tryrun "uname" ["-s"] in + let arch,_ = tryrun "uname" ["-s"] in if starts_with arch "CYGWIN" then "win32" else if starts_with arch "MINGW32" then "win32" else if arch <> "" then arch @@ -433,7 +441,7 @@ let vcs = let make = try - let version_line = run !Prefs.makecmd ["-v"] in + let version_line, _ = run !Prefs.makecmd ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with | major::minor::_ when (s2i major, s2i minor) >= (3,81) -> @@ -466,8 +474,8 @@ let _ = if not (is_executable camlc) then die ("Error: cannot find the executable '"^camlc^"'.") -let caml_version = run camlc ["-version"] -let camllib = run camlc ["-where"] +let caml_version, _ = run camlc ["-version"] +let camllib, _ = run camlc ["-where"] let camlp4compat = "-loc loc" (** Caml version as a list of string, e.g. ["4";"00";"1"] *) @@ -525,7 +533,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with dir testcma in die msg | None -> - let dir = tryrun "camlp5" ["-where"] in + let dir,_ = tryrun "camlp5" ["-where"] in if dir <> "" then dir else if Sys.file_exists (camllib/"camlp5"/testcma) then camllib/"camlp5" @@ -543,7 +551,7 @@ let check_camlp5_version () = if s.[i] = '4' then s.[i] <- '5' done; try - let version_line = run ~err:StdOut camlexec.p4 ["-v"] in + let version_line, _ = run ~err:StdOut camlexec.p4 ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match string_split '.' version with | major::minor::_ when (s2i major, s2i minor) >= (5,1) -> @@ -605,7 +613,7 @@ let check_native () = (msg_no_camlp4_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 + 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"; @@ -625,7 +633,7 @@ let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt" let needs_MacOS_fix () = match hasnatdynlink, arch, caml_version_nums with | true, "Darwin", 3::11::_ -> - (match string_split '.' (run "uname" ["-r"]) with + (match string_split '.' (fst(run "uname" ["-r"])) with | "9"::_ -> true | "10"::("0"|"1"|"2")::_ -> true | "10"::_ when Sys.word_size = 32 -> true @@ -643,7 +651,7 @@ let osdeplibs = "-cclib -lunix" let operating_system, osdeplibs = if starts_with arch "sun4" then - let os = run "uname" ["-r"] in + let os, _ = run "uname" ["-r"] in if starts_with os "5" then "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket" else @@ -676,11 +684,11 @@ let get_lablgtkdir () = else "", "" | None -> let msg = "via ocamlfind" in - let d1 = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in + let d1,_ = tryrun "ocamlfind" ["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 "ocamlfind" ["query";"lablgtk2"] in if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg else let msg = "in OCaml library" in @@ -738,7 +746,7 @@ 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 + let osxdir,_ = tryrun "ocamlfind" ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; idearchflags := "lablgtkosx.cma"; @@ -760,8 +768,16 @@ let strip = if arch = "Darwin" then if hasnatdynlink then "true" else "strip" else - if !Prefs.profile || !Prefs.debug then "true" else "strip" - + if !Prefs.profile || !Prefs.debug then "true" else begin + let _, all = run camlexec.byte ["-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 + end (** * md5sum command *) -- cgit v1.2.3