[coq_dune] Abstract path operations wrt directory separator.

Even if cosmetic, this is useful for window-based hosts.

1 files changed, 25 insertions, 17 deletions

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 4f4e6d5d6f..f94da14cd0 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -72,6 +72,9 @@ module Aux = struct
 
   let sep fmt () = fprintf fmt "@;"
 
+  (* Creation of paths, aware of the platform separator. *)
+  let bpath l = String.concat Filename.dir_sep l
+
   module DirOrd = struct
     type t = string list
     let compare = list_compare String.compare
@@ -83,6 +86,14 @@ module Aux = struct
   (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *)
   module Legacy = struct
 
+
+    (* Fix once we move to OCaml >= 4.06.0 *)
+    let list_init len f =
+      let rec init_aux i n f =
+        if i >= n then []
+        else let r = f i in r :: init_aux (i+1) n f
+      in init_aux 0 len f
+
     (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
     let dirmap_update key f map =
       match begin
@@ -134,16 +145,9 @@ let filter_no_vo =
 
 (* We could have coqdep to output dune files directly *)
 
-(* Fix once we move to OCaml >= 4.06.0 *)
-let list_init len f =
-  let rec init_aux i n f =
-    if i >= n then []
-    else let r = f i in r :: init_aux (i+1) n f
-  in init_aux 0 len f
-
 let gen_sub n =
   (* Move to List.init once we can depend on OCaml >= 4.06.0 *)
-  String.concat "/" (list_init n (fun _ -> "..")) ^ "/"
+  bpath @@ Legacy.list_init n (fun _ -> "..")
 
 let pp_rule fmt targets deps action =
   (* Special printing of the first rule *)
@@ -164,13 +168,13 @@ let pp_vo_dep dir fmt vo =
   let depth = List.length dir in
   let sdir = gen_sub depth in
   (* All files except those in Init implicitly depend on the Prelude, we account for it here. *)
-  let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", ["theories/Init/Prelude.vo"] in
+  let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in
   (* Coq flags *)
   let cflag = Options.build_coq_flags () in
   (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
-  let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in
+  let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in
   (* The source file is also corrected as we will call coqtop from the top dir *)
-  let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in
+  let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in
   (* The final build rule *)
   let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in
   pp_rule fmt [vo.target] deps action
@@ -193,16 +197,16 @@ let pp_dep dir fmt oo = match oo with
 let out_install fmt dir ff =
   let itarget = String.concat "/" dir in
   let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in
-  let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (itarget^"/"^tg) in
+  let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (bpath [itarget;tg]) in
   fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n"
     (pp_list pp_ispec sep) ff
 
 (* For each directory, we must record two things, the build rules and
    the install specification. *)
 let record_dune d ff =
-  let sd = String.concat "/" d in
+  let sd = bpath d in
   if Sys.file_exists sd && Sys.is_directory sd then
-    let out = open_out (sd^"/dune") in
+    let out = open_out (bpath [sd;"dune"]) in
     let fmt = formatter_of_out_channel out in
     if List.nth d 0 = "plugins" then
       fprintf fmt "(include plugin_base.dune)@\n";
@@ -222,12 +226,12 @@ let scan_mlg4 m d =
   let dir = ["plugins"; d] in
   let m = DirMap.add dir [] m in
   let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg"))
-                   Array.(to_list @@ readdir String.(concat "/" dir))) in
+                   Array.(to_list @@ readdir (bpath dir))) in
   List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4
 
 let scan_plugins m =
-  let is_plugin_directory dir = Sys.(is_directory dir && file_exists (dir ^ "/plugin_base.dune")) in
-  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in
+  let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
+  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
   List.fold_left scan_mlg4 m dirs
 
 (* Process .vfiles.d and generate a skeleton for the dune file *)
@@ -240,6 +244,10 @@ let parse_coqdep_line l =
     begin match targets with
     | [target] ->
       let dir, target = Filename.(dirname target, basename target) in
+      (* coqdep outputs with the '/' directory separator regardless of
+         the platform. Anyways, I hope we can link to coqdep instead
+         of having to parse its output soon, that should solve this
+         kind of issues *)
       Some (String.split_on_char '/' dir, VO { target; deps; })
     (* Otherwise a vio file, we ignore *)
     | _ -> None