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.
---
 clib/cUnix.ml | 144 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 144 insertions(+)
 create mode 100644 clib/cUnix.ml

(limited to 'clib/cUnix.ml')

diff --git a/clib/cUnix.ml b/clib/cUnix.ml
new file mode 100644
index 0000000000..34fb660db4
--- /dev/null
+++ b/clib/cUnix.ml
@@ -0,0 +1,144 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \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 escaped_string_of_physical_path p =
+  (* We assume a reasonable-enough path (typically utf8) and prevents
+     the presence of space; other escapings might be useful... *)
+  if String.contains p ' ' then "\"" ^ p ^ "\"" else 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 = Bytes.make 127 ' ' in
+  let buffe = Bytes.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 = Bytes.sub buff 0 !n in (hook r; Buffer.add_bytes result r);
+    let r = Bytes.sub buffe 0 !ne in (hook r; Buffer.add_bytes 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)
-- 
cgit v1.2.3