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.ml | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 27e21204cc..d1cdd8efc9 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,18 +53,6 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l -let file_exists_respecting_case f = - if Coq_config.arch = "Darwin" then - (* ensure that the file exists with expected case on the - case-insensitive but case-preserving default MacOS file system *) - let rec aux f = - let bf = Filename.basename f in - let df = Filename.dirname f in - (String.equal df "." || String.equal df "/" || aux df) - && Array.exists (String.equal bf) (Sys.readdir df) - in aux f - else Sys.file_exists f - let rec search paths test = match paths with | [] -> [] @@ -89,7 +77,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 file_exists_respecting_case f then [lpe,f] else [])) + if Sys.file_exists f then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -105,7 +93,7 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - if file_exists_respecting_case filename then + if Sys.file_exists filename then let root = Filename.dirname filename in root, filename else -- 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.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc9..139effd9fa 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -178,7 +178,7 @@ let raw_extern_intern magic = let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename, channel + channel and intern_state filename = try let channel = open_in_bin filename in @@ -191,11 +191,11 @@ let raw_extern_intern magic = in (extern_state,intern_state) -let extern_intern ?(warn=true) magic = +let extern_intern magic = let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state name val_0 = + let extern_state filename val_0 = try - let (filename,channel) = raw_extern name in + let channel = raw_extern filename in try marshal_out channel val_0; close_out channel @@ -205,9 +205,8 @@ let extern_intern ?(warn=true) magic = iraise reraise with Sys_error s -> errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state paths name = + and intern_state filename = try - let _,filename = find_file_in_path ~warn paths name in let channel = raw_intern filename in let v = marshal_in filename channel in close_in channel; -- 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.ml | 71 +++++++++++++++++++++++++++-------------------------------- 1 file changed, 33 insertions(+), 38 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 139effd9fa..ddc56956c5 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -174,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int filename channel) magic) then + raise (Bad_magic_number filename); channel - and intern_state filename = - try - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s -let extern_intern magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state filename val_0 = - try - let channel = raw_extern filename in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state filename = +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a -- 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.ml | 50 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index ddc56956c5..02d5e963ff 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" -- cgit v1.2.3 From b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Nov 2015 22:22:17 +0100 Subject: Fix for case-insensitive path looking continued (#2554): Adding a second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.). --- lib/system.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 02d5e963ff..2e35a98f7f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -79,12 +79,20 @@ let make_dir_table dir = Unix.closedir a; !b let exists_in_dir_respecting_case dir bf = - let contents = - try StrMap.find dir !dirmap with Not_found -> + let contents, cached = + try StrMap.find dir !dirmap, true with Not_found -> let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents in - StrSet.mem bf contents + contents, false in + StrSet.mem bf contents || + if cached then begin + (* rescan, there is a new file we don't know about *) + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + StrSet.mem bf contents + end + else + false let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase -- cgit v1.2.3 From ce9e7c2a842d7ec7734b58af64de9283de963e37 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Dec 2015 19:25:08 +0100 Subject: Replace Unix.readdir by Sys.readdir in dir cache. This makes the function sightly more portable. --- lib/system.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 2e35a98f7f..91b2f5afaf 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -67,16 +67,8 @@ 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 filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) let exists_in_dir_respecting_case dir bf = let contents, cached = -- cgit v1.2.3 From 9d45d45f3a8718581a001af4576ca87feb741073 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 9 Dec 2015 14:56:17 +0100 Subject: Remove remaining occurrences of Unix.readdir. --- lib/system.ml | 30 ++++++++++-------------------- 1 file changed, 10 insertions(+), 20 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 91b2f5afaf..f860bd2f7e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -11,12 +11,11 @@ open Pp open Errors open Util -open Unix (* All subdirectories, recursively *) let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false + try Sys.is_directory dir with Sys_error _ -> false let skipped_dirnames = ref ["CVS"; "_darcs"] @@ -31,24 +30,15 @@ let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in let rec traverse dir rel = - let dirh = opendir dir in - try - while true do - let f = readdir dirh in - if ok_dirname f then - let file = Filename.concat dir f in - try - begin match (stat file).st_kind with - | S_DIR -> - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - | _ -> () - end - with Unix_error (e,s1,s2) -> () - done - with End_of_file -> - closedir dirh + Array.iter (fun f -> + if ok_dirname f then + let file = Filename.concat dir f in + if Sys.is_directory file then begin + let newrel = rel @ [f] in + add file newrel; + traverse file newrel + end) + (Sys.readdir dir) in if exists_dir root then traverse root []; List.rev !l -- cgit v1.2.3 From 20e1829ad3de42dd322af972c6f9a585f40738ef Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Dec 2015 16:40:38 +0100 Subject: Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing "open Unix" from lib/system.ml. --- lib/system.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index f860bd2f7e..a902229609 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -262,7 +262,7 @@ type time = float * float * float let get_time () = let t = Unix.times () in - (Unix.gettimeofday(), t.tms_utime, t.tms_stime) + (Unix.gettimeofday(), t.Unix.tms_utime, t.Unix.tms_stime) (* Keep only 3 significant digits *) let round f = (floor (f *. 1e3)) *. 1e-3 -- cgit v1.2.3 From d58957f63d36e2da41f6f839a2d94cb0db4c8125 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 14 Dec 2015 10:44:22 +0100 Subject: Remove some occurrences of Unix.opendir. --- lib/system.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index b57c02a14f..b641aad91b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -64,9 +64,7 @@ let apply_subdir f path name = | _ -> () let process_directory f path = - let dirh = Unix.opendir path in - try while true do apply_subdir f path (Unix.readdir dirh) done - with End_of_file -> Unix.closedir dirh + Array.iter (apply_subdir f path) (Sys.readdir path) let process_subdirectories f path = let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in -- cgit v1.2.3 From 13f014ba37e0af547d57854df8926d633f9ccb7b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 21 Dec 2015 17:51:38 +0100 Subject: Trust the directory cache in batch mode. When coqtop is a long-lived process (e.g. coqide), the user might be creating files on the fly. So we have to ask the operating system whether a file exists beforehand, so that we know whether the content of the directory cache is outdated. In batch mode, we can assume that the cache is always up-to-date, so we don't need to query the operating system before trusting the content of the cache. On a script doing "Require Import Reals", this brings down the number of stat syscalls from 42k to 2k. The number of syscalls could be further halved if all_subdirs was filling the directory cache. --- lib/system.ml | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index b641aad91b..31e9861d3a 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -56,7 +56,7 @@ let check_unix_dir warn dir = let apply_subdir f path name = (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) (* as well as skipped files like CVS, ... *) - if name.[0] <> '.' && ok_dirname name then + if ok_dirname name 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 -> f (FileDir (path,name)) @@ -109,20 +109,22 @@ let make_dir_table dir = Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) let exists_in_dir_respecting_case dir bf = - let contents, cached = - try StrMap.find dir !dirmap, true with Not_found -> + let cache_dir dir = let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents, false in + contents in + let contents, fresh = + try + (* in batch mode, assume the directory content is still fresh *) + StrMap.find dir !dirmap, !Flags.batch_mode + with Not_found -> + (* in batch mode, we are not yet sure the directory exists *) + if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true + else cache_dir dir, true in StrSet.mem bf contents || - if cached then begin + not fresh && (* rescan, there is a new file we don't know about *) - let contents = make_dir_table dir in - dirmap := StrMap.add dir contents !dirmap; - StrSet.mem bf contents - end - else - false + StrSet.mem bf (cache_dir dir) let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase @@ -132,7 +134,7 @@ let file_exists_respecting_case path f = 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 + in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f let rec search paths test = match paths with -- 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.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index a902229609..9bdcecef19 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* false let is_in_system_path filename = - let path = try Sys.getenv "PATH" - with Not_found -> error "system variable PATH not found" in - let lpath = CUnix.path_to_list path in - is_in_path lpath filename + try + let lpath = CUnix.path_to_list (Sys.getenv "PATH") in + is_in_path lpath filename + with Not_found -> + msg_warning (str "system variable PATH not found"); + false let open_trapping_failure name = try open_out_bin name -- cgit v1.2.3 From 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 19:56:52 +0100 Subject: Fix #4591: Uncaught exception in directory browsing. We protect Sys.readdir calls againts any nasty exception. --- lib/system.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 0ad43a7423..36fdf26089 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -26,6 +26,8 @@ let ok_dirname f = not (String.List.mem f !skipped_dirnames) && (match Unicode.ident_refutation f with None -> true | _ -> false) +let readdir dir = try Sys.readdir dir with any -> [||] + let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in @@ -38,7 +40,7 @@ let all_subdirs ~unix_path:root = add file newrel; traverse file newrel end) - (Sys.readdir dir) + (readdir dir) in if exists_dir root then traverse root []; List.rev !l @@ -58,7 +60,7 @@ let dirmap = ref StrMap.empty let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (readdir dir) let exists_in_dir_respecting_case dir bf = let contents, cached = -- cgit v1.2.3