Merge PR #8435: [dune] Fix build of coq_dune in 4.02.3

1 files changed, 27 insertions, 3 deletions

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index c89c78c8ec..ab60920fbc 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -80,6 +80,7 @@ module Aux = struct
   module DirMap = Map.Make(DirOrd)
 
   (* Functions available in newer OCaml versions *)
+  (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *)
   module Legacy = struct
 
     (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
@@ -103,6 +104,29 @@ module Aux = struct
         end
       done;
       sub s 0 !j :: !r
+
+    (* Available in OCaml >= 4.04 *)
+    let is_dir_sep = match Sys.os_type with
+      | "Win32" -> fun s i -> s.[i] = '\\'
+      | _ -> fun s i -> s.[i] = '/'
+
+    let extension_len name =
+      let rec check i0 i =
+        if i < 0 || is_dir_sep name i then 0
+        else if name.[i] = '.' then check i0 (i - 1)
+        else String.length name - i0
+      in
+      let rec search_dot i =
+        if i < 0 || is_dir_sep name i then 0
+        else if name.[i] = '.' then check i (i - 1)
+        else search_dot (i - 1)
+      in
+      search_dot (String.length name - 1)
+
+    let remove_extension name =
+      let l = extension_len name in
+      if l = 0 then name else String.sub name 0 (String.length name - l)
+
   end
 
   let add_map_list key elem map =
@@ -181,18 +205,18 @@ let pp_vo_dep dir fmt vo =
   (* 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
   (* 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 = String.concat "/" dir ^ "/" ^ Legacy.(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
 
 let pp_ml4_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
+  let target = Legacy.(remove_extension ml) ^ ".ml" in
   let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
   pp_rule fmt [target] [ml] ml4_rule
 
 let pp_mlg_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
+  let target = Legacy.(remove_extension ml) ^ ".ml" in
   let ml4_rule = "(run coqpp %{pp-file})" in
   pp_rule fmt [target] [ml] ml4_rule