From b712864e9cf499f1298c1aca1ad8a8b17e145079 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Sep 2015 12:12:05 +0200 Subject: Revert "On MacOS X, ensuring that files found in the file system have the" and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X." This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 and 69941d4e195650bf59285b897c14d6287defea0f and e7043eec55085f4101bfb126d8829de6f6086c5a. Trying to emulate a case sensitive file system on top of a case aware one is too costly: 3x slowdown when compiling the stdlib or CompCert. --- lib/system.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 051e92f166..a3d66d577a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -29,8 +29,6 @@ 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 -> 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] -- cgit v1.2.3 From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:05:45 +0200 Subject: Prevent States.intern_state and System.extern_intern from looking up files in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. --- lib/system.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..5797502e9f 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -37,10 +37,10 @@ val find_file_in_path : exception Bad_magic_number of string val raw_extern_intern : int -> - (string -> string * out_channel) * (string -> in_channel) + (string -> out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> - (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) +val extern_intern : int -> + (string -> 'a -> unit) * (string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- lib/system.mli | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 5797502e9f..247d528b97 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From 3940441dffdfc3a8f968760c249f6a2e8a1e0912 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Sep 2015 09:05:44 +0200 Subject: 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) --- lib/system.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 247d528b97..c2d64fe0d0 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] -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- lib/system.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index c2d64fe0d0..062c8ea856 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*