Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)

3 files changed, 58 insertions, 34 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 7d281977af..f1e519d038 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -87,6 +87,9 @@ COQDEP   ?= "$(COQBIN)coqdep"
 GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
 COQMKTOP ?= "$(COQBIN)coqmktop"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+# Timing scripts
 COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
 COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
 COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
@@ -181,10 +184,6 @@ endif
 
 PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
 
-COQLIBINSTALL = $(COQLIB)user-contrib
-COQDOCINSTALL = $(DOCDIR)user-contrib
-COQTOPINSTALL = $(COQLIB)toploop
-
 ifneq (,$(TIMING))
 TIMING_ARG=-time
 ifeq (after,$(TIMING))
@@ -205,6 +204,12 @@ ifneq "$(DSTROOT)" ""
 DESTDIR := $(DSTROOT)
 endif
 
+concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2))
+
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
+
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -437,13 +442,13 @@ beautify: $(BEAUTYFILES)
 
 install: install-extra
 	$(HIDE)for f in $(FILESTOINSTALL); do\
-	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
-	 if [ -z "$$df" ]; then\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
 	   echo SKIP "$$f" since it has no logical path;\
 	 else\
-	   install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
-	   install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
-	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
 	 fi;\
 	done
 install-extra::
@@ -452,28 +457,28 @@ install-extra::
 
 install-byte:
 	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
-	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
-	 if [ -z "$$df" ]; then\
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ "$$?" != "0" -o -z "$$df" ]; then\
 	   echo SKIP "$$f" since it has no logical path;\
 	 else\
-	   install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
-	   install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
-	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	   install -d "$(COQLIBINSTALL)/$$df" &&\
+	   install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
+	   echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
 	 fi;\
 	done
 
 install-doc:: html mlihtml
 	@# Extension point
-	$(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
 	$(HIDE)for i in html/*; do \
-	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
 	 install -m 0644 "$$i" "$$dest";\
 	 echo INSTALL "$$i" "$$dest";\
 	done
 	$(HIDE)install -d \
-		"$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+		"$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
 	$(HIDE)for i in mlihtml/*; do \
-	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
 	 install -m 0644 "$$i" "$$dest";\
 	 echo INSTALL "$$i" "$$dest";\
 	done
@@ -482,21 +487,21 @@ install-doc:: html mlihtml
 uninstall::
 	@# Extension point
 	$(HIDE)for f in $(FILESTOINSTALL); do \
-	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
-	 instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \
-	 rm -f "$$instf";\
-	 echo RM "$$instf"; \
-	 rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \
+	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
+	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
+	 rm -f "$$instf" &&\
+	 echo RM "$$instf" &&\
+	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \
 	done
 .PHONY: uninstall
 
 uninstall-doc::
 	@# Extension point
-	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
-	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
-	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
-	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
-	$(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
 .PHONY: uninstall-doc
 
 # Cleaning ####################################################################
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c3aedf538e..327f53520c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -118,7 +118,7 @@ let makefile_template =
   let template = "/tools/CoqMakefile.in" in
   Coq_config.coqlib ^ template
 
-let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
+let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s
 
 let generate_makefile oc conf_file local_file args project =
   let s = read_whole_file makefile_template in
@@ -193,13 +193,19 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
     (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
 ;;
 
+let windrive s =
+  if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0)
+  then Str.matched_string s
+  else s
+;;
+
 let generate_conf_coq_config oc args bypass_API =
   section oc "Coq configuration.";
   let src_dirs = if bypass_API
                  then Coq_config.all_src_dirs
                  else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in
   Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
-  fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); 
+  fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
 ;;
 
 let generate_conf_files oc
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index c0d2e4d6b5..a9da27ba23 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -293,15 +293,28 @@ let usage () =
 module Coqide = Spawn.Sync(struct end)
 
 let main =
-  Sys.set_signal Sys.sigpipe
+  if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
   let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
-  let coqtop_name, coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> "coqtop", Array.of_list def_args, f
+  let coqtop_name = (* from ide/ideutils.ml *)
+    let prog_name = "fake_ide" in
+    let len_prog_name = String.length prog_name in
+    let fake_ide_path = Sys.executable_name in
+    let fake_ide_path_len = String.length fake_ide_path in
+    let pos = fake_ide_path_len - len_prog_name in
+    let rex = Str.regexp_string prog_name in
+    try
+      let i = Str.search_backward rex fake_ide_path pos in
+      String.sub fake_ide_path 0 i ^ "coqtop" ^
+      String.sub fake_ide_path (i + len_prog_name)
+        (fake_ide_path_len - i - len_prog_name) 
+    with Not_found -> assert false in
+  let coqtop_args, input_file = match Sys.argv with
+    | [| _; f |] -> Array.of_list def_args, f
     | [| _; f; ct |] ->
         let ct = Str.split (Str.regexp " ") ct in
-        List.hd ct, Array.of_list (def_args @ List.tl ct), f
+        Array.of_list (def_args @ ct), f
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =