Merge PR #9588: [azure] [ci] Build on Windows using Dune.

Reviewed-by: SkySkimmer

3 files changed, 18 insertions, 15 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f8f10b34ae..bd9d8c9221 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -187,7 +187,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
 COQMAKEFILE_VERSION:=@COQ_VERSION@
 
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
 
@@ -216,9 +216,9 @@ endif
 
 concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(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)
+COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
+COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
+COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
 
 # Files #######################################################################
 #
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4f01a6bd87..68281d6481 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -123,9 +123,10 @@ let read_whole_file s =
 let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s
 
 let generate_makefile oc conf_file local_file args project =
+  let coqlib = Envars.coqlib () in
   let makefile_template =
-    let template = "/tools/CoqMakefile.in" in
-    Envars.coqlib () ^ template in
+    let template = Filename.concat "tools" "CoqMakefile.in" in
+    Filename.concat coqlib template in
   let s = read_whole_file makefile_template in
   let s = List.fold_left
     (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
@@ -260,7 +261,7 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
          eprintf "Warning: in %s\n" destination;
          destination
       end else "$(INSTALLDEFAULTROOT)"
-    else String.concat "/" gcd in
+    else String.concat Filename.dir_sep gcd in
   Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)
 
 let generate_conf_defs oc { defs; extra_args } =
@@ -343,15 +344,13 @@ let chop_prefix p f =
   let len_f = String.length f in
   String.sub f len_p (len_f - len_p)
 
-let clean_path p =
-  Str.global_replace (Str.regexp_string "//") "/" p
-
 let destination_of { ml_includes; q_includes; r_includes; } file =
   let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
   let includes = q_includes @ r_includes in
   let mk_destination logic canonical_path =
-    clean_path (physical_dir_of_logical_dir logic ^ "/" ^
-                chop_prefix canonical_path file_dir ^ "/") in
+    Filename.concat
+      (physical_dir_of_logical_dir logic)
+      (chop_prefix canonical_path file_dir) in
   let candidates =
     CList.map_filter (fun {thing={ canonical_path }, logic} ->
       if is_prefix canonical_path file_dir then
@@ -368,8 +367,9 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
      with
         | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
             let destination =
-              clean_path (physical_dir_of_logical_dir logic ^ "/" ^
-                          chop_prefix p file_dir ^ "/") in
+              Filename.concat
+                (physical_dir_of_logical_dir logic)
+                (chop_prefix p file_dir) in
             Printf.printf "%s" (quote destination)
         | _ -> () (* skip *)
         | exception Not_found -> () (* skip *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 0d3fb77551..5dd6cc6c83 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -79,14 +79,17 @@ let use_suffix prefix suffix =
 
 (** A weaker analog of the function in Envars *)
 
+let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+
 let guess_coqlib () =
+  getenv_else "COQLIB" (fun () ->
   let file = "theories/Init/Prelude.vo" in
   let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
   let prefix = Filename.dirname coqbin in
   let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
   if Sys.file_exists (coqlib / file) then coqlib else
   if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
-  then Coq_config.coqlib else prefix
+  then Coq_config.coqlib else prefix)
 
 let header_trailer = ref true
 let header_file = ref ""