diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/cUnix.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/cUnix.mli')
-rw-r--r-- | lib/cUnix.mli | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/lib/cUnix.mli b/lib/cUnix.mli new file mode 100644 index 00000000..2d0d202d --- /dev/null +++ b/lib/cUnix.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** {5 System utilities} *) + +type physical_path = string +type load_path = physical_path list + +val physical_path_of_string : string -> physical_path +val string_of_physical_path : physical_path -> string + +val canonical_path_name : string -> string + +(** 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 + +(** correct_path f dir = dir/f if f is relative *) +val correct_path : string -> string -> string + +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 + +(** Return the extension of a file, i.e. its smaller suffix starting + with "." if any, or "" otherwise. *) +val get_extension : string -> string + +val file_readable_p : string -> bool + +(** {6 Executing commands } *) + +(** [run_command com] launches command [com], and returns + the contents of stdout and stderr. If given, [~hook] + is called on each elements read on stdout or stderr. *) + +val run_command : + ?hook:(string->unit) -> string -> Unix.process_status * string + +(** [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. *) + +val sys_command : string -> string list -> Unix.process_status + +(** A version of [Unix.waitpid] immune to EINTR exceptions *) + +val waitpid_non_intr : int -> Unix.process_status + +(** checks if two file names refer to the same (existing) file *) +val same_file : string -> string -> bool + |