Generalizing the patch to bug #2554 on fixing path looking with

correct case on MacOS X whose file system is case-insensitive but
case-preserving (HFS+ configured in case-insensitive mode).

Generalized it to any case-preserving case-insensitive file system,
which makes it applicable to Windows with NTFS used in
case-insensitive mode but also to Linux when mounting a
case-insensitive file system.

Removed the blow-up of the patch, improved the core of the patch by
checking whether the case is correct only for the suffix part of the
file to be found (not for the part which corresponds to the path in
which where to look), and finally used a cache so that the effect of
the patch is not observable.

Note that the cache is implemented in a way not synchronous with
backtracking what implies e.g. that a file compiled in the middle of
an interactive session would not be found until Coq is restarted, even
by backtracking before the corresponding Require.

For history see commits
 b712864e9cf499f1298c1aca1ad8a8b17e145079,
 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
 69941d4e195650bf59285b897c14d6287defea0f
 e7043eec55085f4101bfb126d8829de6f6086c5a.

as well as
 https://coq.inria.fr/bugs/show_bug.cgi?id=2554
 discussion on coq-club "8.5 and MathClasses" (May 2015)
 discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015)

3 files changed, 55 insertions, 2 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index b0eed8386..2b8af917f 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -39,6 +39,8 @@ let path_to_list p =
 let user_path () =
   path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
 
+(* Finding a name in path using the equality provided by the file system *)
+(* whether it is case-sensitive or case-insensitive *)
 let rec which l f =
   match l with
     | [] ->
@@ -99,7 +101,8 @@ let _ =
 (** [check_file_else ~dir ~file oth] checks if [file] exists in
     the installation directory [dir] given relatively to [coqroot].
     If this Coq is only locally built, then [file] must be in [coqroot].
-    If the check fails, then [oth ()] is evaluated. *)
+    If the check fails, then [oth ()] is evaluated.
+    Using file system equality seems well enough for this heuristic *)
 let check_file_else ~dir ~file oth =
   let path = if Coq_config.local then coqroot else coqroot / dir in
   if Sys.file_exists (path / file) then path else oth ()
diff --git a/lib/system.ml b/lib/system.ml
index ddc56956c..02d5e963f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,6 +53,49 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
+(* Caching directory contents for efficient syntactic equality of file
+   names even on case-preserving but case-insensitive file systems *)
+
+module StrMod = struct
+  type t = string
+  let compare = compare
+end
+
+module StrMap = Map.Make(StrMod)
+module StrSet = Set.Make(StrMod)
+
+let dirmap = ref StrMap.empty
+
+let make_dir_table dir =
+  let b = ref StrSet.empty in
+  let a = Unix.opendir dir in
+  (try
+    while true do
+      let s = Unix.readdir a in
+      if s.[0] != '.' then b := StrSet.add s !b
+    done
+  with
+  | End_of_file -> ());
+  Unix.closedir a; !b
+
+let exists_in_dir_respecting_case dir bf =
+  let contents =
+    try StrMap.find dir !dirmap with Not_found ->
+    let contents = make_dir_table dir in
+    dirmap := StrMap.add dir contents !dirmap;
+    contents in
+  StrSet.mem bf contents
+
+let file_exists_respecting_case path f =
+  (* This function ensures that a file with expected lowercase/uppercase
+     is the correct one, even on case-insensitive file systems *)
+  let rec aux f =
+    let bf = Filename.basename f in
+    let df = Filename.dirname f in
+    (String.equal df "." || aux df)
+    && exists_in_dir_respecting_case (Filename.concat path df) bf
+  in Sys.file_exists (Filename.concat path f) && aux f
+
 let rec search paths test =
   match paths with
   | [] -> []
@@ -77,7 +120,7 @@ let where_in_path ?(warn=true) path filename =
   in
   check_and_warn (search path (fun lpe ->
     let f = Filename.concat lpe filename in
-    if Sys.file_exists f then [lpe,f] else []))
+    if file_exists_respecting_case lpe filename then [lpe,f] else []))
 
 let where_in_path_rex path rex =
   search path (fun lpe ->
@@ -93,6 +136,8 @@ let where_in_path_rex path rex =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
+    (* the name is considered to be a physical name and we use the file
+       system rules (e.g. possible case-insensitivity) to find it *)
     if Sys.file_exists filename then
       let root = Filename.dirname filename in
       root, filename
@@ -100,6 +145,9 @@ let find_file_in_path ?(warn=true) paths filename =
       errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
+    (* the name is considered to be the transcription as a relative
+       physical name of a logical name, so we deal with it as a name
+       to be locate respecting case *)
     try where_in_path ~warn paths filename
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
diff --git a/lib/system.mli b/lib/system.mli
index 247d528b9..c2d64fe0d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -29,6 +29,8 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+val file_exists_respecting_case : string -> string -> bool
+
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]