[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.

1 files changed, 0 insertions, 78 deletions

diff --git a/lib/minisys.ml b/lib/minisys.ml
deleted file mode 100644
index 389b18ad4e..0000000000
--- a/lib/minisys.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(** Minisys regroups some code that used to be in System.
-    Unlike System, this module has no dependency and could
-    be used for initial compilation target such as coqdep_boot.
-    The functions here are still available in System thanks to
-    an include. For the signature, look at the top of system.mli
-*)
-
-(** Dealing with directories *)
-
-type unix_path = string (* path in unix-style, with '/' separator *)
-
-type file_kind =
-  | FileDir of unix_path * (* basename of path: *) string
-  | FileRegular of string (* basename of file *)
-
-(* Copy of Filename.concat but assuming paths to always be POSIX *)
-
-let (//) dirname filename =
-  let l = String.length dirname in
-  if l = 0 || dirname.[l-1] = '/'
-  then dirname ^ filename
-  else dirname ^ "/" ^ filename
-
-(* Excluding directories; We avoid directories starting with . as well
-   as CVS and _darcs and any subdirs given via -exclude-dir *)
-
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
-
-(* Note: this test is possibly used for Coq module/file names but also for
-   OCaml filenames, whose syntax as of today is more restrictive for
-   module names (only initial letter then letter, digits, _ or quote),
-   but more permissive (though disadvised) for file names  *)
-
-let ok_dirname f =
-  not (f = "") && f.[0] != '.' &&
-  not (List.mem f !skipped_dirnames) &&
-  match Unicode.ident_refutation f with None -> true | _ -> false
-
-(* Check directory can be opened *)
-
-let exists_dir dir =
-  (* See BZ#5391 on windows failing on a trailing (back)slash *)
-  let rec strip_trailing_slash dir =
-    let len = String.length dir in
-    if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
-    then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
-  let dir = if Sys.os_type = "Win32" then strip_trailing_slash dir else dir in
-  try Sys.is_directory dir with Sys_error _ -> false
-
-let apply_subdir f path name =
-  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
-  (* as well as skipped files like CVS, ... *)
-  let base = try Filename.chop_extension name with Invalid_argument _ -> name in
-  if ok_dirname base then
-    let path = if path = "." then name else path//name in
-    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
-    | Unix.S_DIR when name = base -> f (FileDir (path,name))
-    | Unix.S_REG -> f (FileRegular name)
-    | _ -> ()
-
-let readdir dir = try Sys.readdir dir with any -> [||]
-
-let process_directory f path =
-  Array.iter (apply_subdir f path) (readdir path)
-
-let process_subdirectories f path =
-  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
-  process_directory f path