From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- clib/cUnix.mli | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 clib/cUnix.mli (limited to 'clib/cUnix.mli') diff --git a/clib/cUnix.mli b/clib/cUnix.mli new file mode 100644 index 00000000..1b185345 --- /dev/null +++ b/clib/cUnix.mli @@ -0,0 +1,71 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 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 + +(** 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:(bytes->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 + +(** Check if two file names refer to the same (existing) file *) +val same_file : string -> string -> bool + -- cgit v1.2.3