diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-22 09:05:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-25 18:06:09 +0100 |
| commit | 3940441dffdfc3a8f968760c249f6a2e8a1e0912 (patch) | |
| tree | 59a05c937688147fd12c7334d82ed291a21266a1 /lib/envars.ml | |
| parent | ef8718a7fd3bcd960d954093d8c636525e6cc492 (diff) | |
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)
Diffstat (limited to 'lib/envars.ml')
| -rw-r--r-- | lib/envars.ml | 5 |
1 files changed, 4 insertions, 1 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 () |