From 5ffa147bd2fe548df3ac9053fe497d0871a5f6df Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 Dec 2017 18:51:45 +0100 Subject: [lib] Split auxiliary libraries into Coq-specific and general. Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM. --- lib/cUnix.mli | 69 ----------------------------------------------------------- 1 file changed, 69 deletions(-) delete mode 100644 lib/cUnix.mli (limited to 'lib/cUnix.mli') diff --git a/lib/cUnix.mli b/lib/cUnix.mli deleted file mode 100644 index d08dc4c403..0000000000 --- a/lib/cUnix.mli +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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