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)

1 files changed, 2 insertions, 0 deletions

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]