diff options
Diffstat (limited to 'lib/cUnix.ml')
| -rw-r--r-- | lib/cUnix.ml | 139 |
1 files changed, 0 insertions, 139 deletions
diff --git a/lib/cUnix.ml b/lib/cUnix.ml deleted file mode 100644 index cb436511..00000000 --- a/lib/cUnix.ml +++ /dev/null @@ -1,139 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Files and load path. *) - -type physical_path = string -type load_path = physical_path list - -let physical_path_of_string s = s -let string_of_physical_path p = p - -let path_to_list p = - let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in - Str.split sep p - -(* Some static definitions concerning filenames *) - -let dirsep = Filename.dir_sep (* Unix: "/" *) -let dirsep_len = String.length dirsep -let curdir = Filename.concat Filename.current_dir_name "" (* Unix: "./" *) -let curdir_len = String.length curdir - -(* Hints to partially detects if two paths refer to the same directory *) - -(** cut path [p] after all the [/] that come at position [pos]. *) -let rec cut_after_dirsep p pos = - if CString.is_sub dirsep p pos then - cut_after_dirsep p (pos + dirsep_len) - else - String.sub p pos (String.length p - pos) - -(** remove all initial "./" in a path unless the path is exactly "./" *) -let rec remove_path_dot p = - if CString.is_sub curdir p 0 then - if String.length p = curdir_len - then Filename.current_dir_name - else remove_path_dot (cut_after_dirsep p curdir_len) - else - p - -(** 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. *) -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - if CString.is_sub cwd p 0 then - remove_path_dot (cut_after_dirsep p (String.length cwd)) - else - remove_path_dot p - -let canonical_path_name 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... *) - strip_path p - -let make_suffix name suffix = - if Filename.check_suffix name suffix then name else (name ^ suffix) - -let get_extension f = - let pos = try String.rindex f '.' with Not_found -> String.length f in - String.sub f pos (String.length f - pos) - -let correct_path f dir = - if Filename.is_relative f then Filename.concat dir f else f - -let file_readable_p name = - try Unix.access name [Unix.R_OK];true - with Unix.Unix_error (_, _, _) -> false - -(* As for [Unix.close_process], a [Unix.waipid] that ignores all [EINTR] *) - -let rec waitpid_non_intr pid = - try snd (Unix.waitpid [] pid) - with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid - -(** [run_command com] launches command [com] (via /bin/sh), - and returns the contents of stdout and stderr. If given, [~hook] - is called on each elements read on stdout or stderr. *) - -let run_command ?(hook=(fun _ ->())) c = - let result = Buffer.create 127 in - let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in - let n = ref 0 in - let ne = ref 0 in - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; - !n+ !ne <> 0 - do - let r = String.sub buff 0 !n in (hook r; Buffer.add_string result r); - let r = String.sub buffe 0 !ne in (hook r; Buffer.add_string result r); - done; - (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) - -(** [sys_command] launches program [prog] with arguments [args]. - It behaves like [Sys.command], except that we rely on - [Unix.create_process], it's hardly more complex and avoids dealing - with shells. In particular, no need to quote arguments - (against whitespace or other funny chars in paths), hence no need - to care about the different quoting conventions of /bin/sh and cmd.exe. *) - -let sys_command prog args = - let argv = Array.of_list (prog::args) in - 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 - accurately check if - -*) -(* Optimised for partial application (in case many candidates must be - compared to f1). *) -let same_file f1 = - try - let s1 = Unix.stat f1 in - (fun f2 -> - try - let s2 = Unix.stat f2 in - s1.Unix.st_dev = s2.Unix.st_dev && - if Sys.os_type = "Win32" then f1 = f2 - else s1.Unix.st_ino = s2.Unix.st_ino - with - Unix.Unix_error _ -> false) - with - Unix.Unix_error _ -> (fun _ -> false) |