Towards "cleaning" a bit cUnix.ml

boot/util.ml

@@ -48,7 +48,7 @@ let use_suffix prefix suffix =
   then suffix
   else Filename.concat prefix suffix
 
-let canonical_path_name p =
+let canonical_dir p =
   let current = Sys.getcwd () in
   try
     Sys.chdir p;
@@ -60,7 +60,7 @@ let canonical_path_name p =
     Filename.concat current p
 
 let coqbin =
-  canonical_path_name (Filename.dirname Sys.executable_name)
+  canonical_dir (Filename.dirname Sys.executable_name)
 
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)

checker/check.ml

@@ -144,7 +144,7 @@ let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
 
 let find_logical_path phys_dir =
-  let phys_dir = CUnix.canonical_path_name phys_dir in
+  let phys_dir = CUnix.canonical_dir phys_dir in
   let physical, logical = !load_paths in
   match List.filter2 (fun p d -> p = phys_dir) physical logical with
   | _,[dir] -> dir
@@ -159,14 +159,14 @@ let add_load_path (phys_path,coq_path) =
   if CDebug.(get_flag misc) then
     Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
-  let phys_path = CUnix.canonical_path_name phys_path in
+  let phys_path = CUnix.canonical_dir phys_path in
   let physical, logical = !load_paths in
     match List.filter2 (fun p d -> p = phys_path) physical logical with
       | _,[dir] ->
           if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = CUnix.canonical_path_name Filename.current_dir_name
+            (phys_path = CUnix.canonical_dir Filename.current_dir_name
                 && coq_path = default_root_prefix)
           then
             begin

clib/cUnix.ml

@@ -11,6 +11,7 @@
 (* Files and load path. *)
 
 type physical_path = string
+type physical_dir_path = string
 type load_path = physical_path list
 
 let physical_path_of_string s = s
@@ -60,16 +61,19 @@ let strip_path p =
   else
     remove_path_dot p
 
-let canonical_path_name p =
+let canonical_dir p =
   let current = Sys.getcwd () in
   try
     Sys.chdir p;
     let p' = Sys.getcwd () in
     Sys.chdir current;
     p'
   with Sys_error _ ->
-    (* We give up to find a canonical name and just simplify it... *)
-    current ^ dirsep ^ strip_path p
+    if Filename.is_relative p then
+      (* We give up to find a canonical name and just simplify it... *)
+      current ^ dirsep ^ strip_path p
+    else
+      p
 
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
@@ -118,7 +122,7 @@ let sys_command prog args =
   let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
   waitpid_non_intr pid
 
-(*
+(**
   checks if two file names refer to the same (existing) file by
   comparing their device and inode.
   It seems that under Windows, inode is always 0, so we cannot

clib/cUnix.mli

@@ -11,34 +11,38 @@
 (** {5 System utilities} *)
 
 type physical_path = string
-type load_path = physical_path list
+type physical_dir_path = string
+type load_path = physical_dir_path list
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
 
 (** Escape what has to be escaped (e.g. surround with quotes if with spaces) *)
 val escaped_string_of_physical_path : physical_path -> string
 
-val canonical_path_name : string -> string
+(** Return the absolute name corresponding to a directory, as given by
+    chdir in this directory, working from the current directory if the
+    name is relative *)
+val canonical_dir : physical_dir_path -> physical_dir_path
 
 (** Remove all initial "./" in a path *)
 val remove_path_dot : string -> string
 
 (** If a path [p] starts with the current directory $PWD then
     [strip_path p] returns the sub-path relative to $PWD.
     Any leading "./" are also removed from the result. *)
-val strip_path : string -> string
+val strip_path : physical_path -> physical_path
 
 (** correct_path f dir = dir/f if f is relative *)
-val correct_path : string -> string -> string
+val correct_path : physical_path -> physical_dir_path -> physical_path
 
 val path_to_list : string -> string list
 
 (** [make_suffix file suf] catenate [file] with [suf] when
     [file] does not already end with [suf]. *)
-val make_suffix : string -> string -> string
+val make_suffix : physical_path -> string -> physical_path
 
-val file_readable_p : string -> bool
+val file_readable_p : physical_path -> bool
 
 (** {6 Executing commands } *)
 
@@ -47,7 +51,7 @@ val file_readable_p : string -> bool
     is called on each elements read on stdout or stderr. *)
 
 val run_command :
-  ?hook:(bytes->unit) -> string -> Unix.process_status * string
+  ?hook:(bytes->unit) -> physical_path -> Unix.process_status * string
 
 (** [sys_command] launches program [prog] with arguments [args].
     It behaves like [Sys.command], except that we rely on
@@ -56,14 +60,14 @@ val run_command :
     (against whitespace or other funny chars in paths), hence no need
     to care about the different quoting conventions of /bin/sh and cmd.exe. *)
 
-val sys_command : string -> string list -> Unix.process_status
+val sys_command : physical_path -> string list -> Unix.process_status
 
 (** A version of [Unix.waitpid] immune to EINTR exceptions *)
 
 val waitpid_non_intr : int -> Unix.process_status
 
 (** Check if two file names refer to the same (existing) file *)
-val same_file : string -> string -> bool
+val same_file : physical_path -> physical_path -> bool
 
 (** Like [Stdlib.Filename.temp_file] but producing a directory. *)
-val mktemp_dir : ?temp_dir:string -> string -> string -> string
+val mktemp_dir : ?temp_dir:physical_dir_path -> string -> string -> physical_dir_path

ide/coqide/coqide.ml

@@ -1820,7 +1820,7 @@ let read_coqide_args argv =
     |"-f" :: file :: args ->
       if project_files <> None then
         (output_string stderr "Error: multiple -f options"; exit 1);
-      let d = CUnix.canonical_path_name (Filename.dirname file) in
+      let d = CUnix.canonical_dir (Filename.dirname file) in
       let warning_fn x = Format.eprintf "%s@\n%!" x in
       let p = CoqProject_file.read_project_file ~warning_fn file in
       filter_coqtop coqtop (Some (d,p)) bindings_files out args

lib/coqProject_file.ml

@@ -218,7 +218,7 @@ let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
   let mk_path d =
     let p = CUnix.correct_path d orig_dir in
     { path = CUnix.remove_path_dot (post_canonize p);
-      canonical_path = CUnix.canonical_path_name p } in
+      canonical_path = CUnix.canonical_dir p } in
   let rec aux proj = function
   | [] -> proj
   | "-impredicative-set" :: _ ->

lib/envars.ml

@@ -97,7 +97,7 @@ let expand_path_macros ~warn s =
 (** {2 Coq paths} *)
 
 let coqbin =
-  CUnix.canonical_path_name (Filename.dirname Sys.executable_name)
+  CUnix.canonical_dir (Filename.dirname Sys.executable_name)
 
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)

tools/coq_makefile.ml

@@ -395,7 +395,7 @@ let parse_extra f r opts = match f, r with
   | _ -> None
 
 let destination_of { ml_includes; q_includes; r_includes; } file =
-  let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
+  let file_dir = CUnix.canonical_dir (Filename.dirname file) in
   let includes = q_includes @ r_includes in
   let mk_destination logic canonical_path =
     Filename.concat

topbin/coqnative_bin.ml

@@ -34,14 +34,14 @@ let add_load_path (phys_path,coq_path) =
   if CDebug.(get_flag misc) then
     Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
-  let phys_path = CUnix.canonical_path_name phys_path in
+  let phys_path = CUnix.canonical_dir phys_path in
   let physical, logical = !load_paths in
     match List.filter2 (fun p d -> p = phys_path) physical logical with
       | _,[dir] ->
           if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = CUnix.canonical_path_name Filename.current_dir_name
+            (phys_path = CUnix.canonical_dir Filename.current_dir_name
                 && coq_path = default_root_prefix)
           then
             begin

vernac/loadpath.ml

@@ -36,7 +36,7 @@ let anomaly_too_many_paths path =
   CErrors.anomaly Pp.(str "Several logical paths are associated with" ++ spc () ++ str path ++ str ".")
 
 let find_load_path phys_dir =
-  let phys_dir = CUnix.canonical_path_name phys_dir in
+  let phys_dir = CUnix.canonical_dir phys_dir in
   let filter p = String.equal p.path_physical phys_dir in
   let paths = List.filter filter !load_paths in
   match paths with
@@ -95,7 +95,7 @@ let warn_overriding_logical_loadpath =
                ; DP.print coq_path]))
 
 let add_load_path root phys_path coq_path ~implicit =
-  let phys_path = CUnix.canonical_path_name phys_path in
+  let phys_path = CUnix.canonical_dir phys_path in
   let filter p = String.equal p.path_physical phys_path in
   let binding = {
     path_logical = coq_path;

vernac/mltop.ml

@@ -32,7 +32,7 @@ open Pp
 (* This path is where we look for .cmo/.cmxs using the legacy method *)
 let coq_mlpath_copy = ref [Sys.getcwd ()]
 let keep_copy_mlpath path =
-  let cpath = CUnix.canonical_path_name path in
+  let cpath = CUnix.canonical_dir path in
   let filter path' = not (String.equal cpath path') in
   coq_mlpath_copy := cpath :: List.filter filter !coq_mlpath_copy