Port from 8.4 branch some build fixes concerning win32 :

 r15722:
   - CAMLBIN was cygwin-specific, leading to issues with coqmktop
   - A missing Filename.quote on the temp file used in coqmktop
   - Try to shorten the cmdline passed to Sys.command in coqmktop:
     way too many includes were passed to coqmktop -boot

 r15724: Coqmktop: the +compiler-libs for ocaml4 is back
 r15725: Coqmktop: better detection of ocaml 4 and above
 r15739: ocamlbuild : a missing include for camlp4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 16 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 6028bb7c8b..60dfeb28d6 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -12,6 +12,15 @@
 
 open Unix
 
+(* In Win32 outside cygwin, Sys.command calls cmd.exe. When it executes
+   a command that may contains many double-quote, we should double-quote
+   the whole ! *)
+
+let safe_sys_command =
+  if Sys.os_type = "Win32" then
+    fun cmd -> Sys.command ("\""^cmd^"\"")
+  else Sys.command
+
 (* Objects to link *)
 
 (* 1. Core objects *)
@@ -52,20 +61,19 @@ let top        = ref false
 let echo       = ref false
 let no_start   = ref false
 
-let is_ocaml4 = String.sub Coq_config.caml_version 0 2 = "4."
+let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
 
-let src_dirs () =
+let src_dirs =
   [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
 
 let includes () =
-  let coqlib = Envars.coqlib Errors.error in
-  let camlp4lib = Envars.camlp4lib () in
-    List.fold_right
-      (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
-      (src_dirs ())
-      (["-I"; "\"" ^ camlp4lib ^ "\""] @
-	  ["-I"; "\"" ^ coqlib ^ "\""] @
-         if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
+  (if !Flags.boot then [] (* the include flags are given on the cmdline *)
+   else
+      let coqlib = Envars.coqlib Errors.error in
+      let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
+      let camlp4incl = ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] in
+      List.fold_right (fun d l -> "-I" :: mkdir d :: l)	src_dirs camlp4incl)
+  @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -282,7 +290,7 @@ let main () =
       []
   in
   (* the list of the loaded modules *)
-  let main_file = create_tmp_main_file modules in
+  let main_file = Filename.quote (create_tmp_main_file modules) in
   try
     let args =
       options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
@@ -290,10 +298,6 @@ let main () =
     let args = if !top then args @ [ "topstart.cmo" ] else args in
       (* Now, with the .cma, we MUST use the -linkall option *)
     let command = String.concat " " (prog::"-rectypes"::args) in
-    (* In Win32, when Sys.command (and hence cmd.exe) executes a command
-       that may contains many double-quote, we should double-quote the whole ! *)
-    let command = if Sys.os_type = "Win32" then "\""^command^"\"" else command
-    in
       if !echo then
 	begin
 	  print_endline command;
@@ -302,7 +306,7 @@ let main () =
 	       (string_of_int (String.length command)) ^ " characters)");
 	  flush Pervasives.stdout
 	end;
-      let retcode = Sys.command command in
+      let retcode = safe_sys_command command in
 	clean main_file;
 	(* command gives the exit code in HSB, and signal in LSB !!! *)
 	if retcode > 255 then retcode lsr 8 else retcode