diff options
Diffstat (limited to 'lib/system.ml')
-rw-r--r-- | lib/system.ml | 147 |
1 files changed, 81 insertions, 66 deletions
diff --git a/lib/system.ml b/lib/system.ml index 9bdcecef..4b99de70 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -9,38 +9,32 @@ (* $Id$ *) open Pp -open Errors open Util -(* All subdirectories, recursively *) +include Minisys -let exists_dir dir = - try Sys.is_directory dir with Sys_error _ -> false +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (String.is_empty f) && f.[0] != '.' && - not (String.List.mem f !skipped_dirnames) && - (match Unicode.ident_refutation f with None -> true | _ -> false) +let warn_cannot_open_dir = + CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem" + (fun dir -> str ("Cannot open directory " ^ dir)) let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in - let rec traverse dir rel = - 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) + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path in - if exists_dir root then traverse root []; + if exists_dir root then traverse root [] + else warn_cannot_open_dir root; List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -58,23 +52,25 @@ 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 = - 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 @@ -84,26 +80,29 @@ 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 | [] -> [] | lpe :: rem -> test lpe @ search rem test +let warn_ambiguous_file_name = + CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem" + (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++ + hov 0 (str "[ " ++ + hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) + (fun (lpe,_) -> str lpe) l) + ++ str " ];") ++ fnl () ++ + str "loading " ++ str f) + + let where_in_path ?(warn=true) path filename = let check_and_warn l = match l with | [] -> raise Not_found | (lpe, f) :: l' -> let () = match l' with - | _ :: _ when warn -> - msg_warning - (str filename ++ str " has been found in" ++ spc () ++ - hov 0 (str "[ " ++ - hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) - (fun (lpe,_) -> str lpe) l) - ++ str " ];") ++ fnl () ++ - str "loading " ++ str f) + | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f) | _ -> () in (lpe, f) @@ -132,7 +131,7 @@ let find_file_in_path ?(warn=true) paths filename = let root = Filename.dirname filename in root, filename else - errorlabstrm "System.find_file_in_path" + CErrors.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 @@ -140,7 +139,7 @@ let find_file_in_path ?(warn=true) paths filename = to be locate respecting case *) try where_in_path ~warn paths filename with Not_found -> - errorlabstrm "System.find_file_in_path" + CErrors.errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) @@ -148,25 +147,34 @@ let is_in_path lpath filename = try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false +let warn_path_not_found = + CWarnings.create ~name:"path-not-found" ~category:"filesystem" + (fun () -> str "system variable PATH not found") + 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 -> + warn_path_not_found (); + false let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> - errorlabstrm "System.open" (str "Can't open " ++ str name) + with e when CErrors.noncritical e -> + CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name) + +let warn_cannot_remove_file = + CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" + (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!") let try_remove filename = try Sys.remove filename - with e when Errors.noncritical e -> - msg_warning - (str"Could not remove file " ++ str filename ++ str" which is corrupted!") + with e when CErrors.noncritical e -> + warn_cannot_remove_file filename let error_corrupted file s = - errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -210,7 +218,8 @@ let skip_in_segment f ch = seek_in ch stop; stop, digest_in f ch -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error let raw_extern_state magic filename = let channel = open_trapping_failure filename in @@ -220,8 +229,12 @@ let raw_extern_state magic filename = 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); + let actual_magic = input_binary_int filename channel in + if not (Int.equal actual_magic magic) then + raise (Bad_magic_number { + filename=filename; + actual=actual_magic; + expected=magic}); channel with | End_of_file -> error_corrupted filename "premature end of file" @@ -234,11 +247,11 @@ let extern_state magic filename val_0 = marshal_out channel val_0; close_out channel with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = try_remove filename in iraise reraise with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) + CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s) let intern_state magic filename = try @@ -247,13 +260,15 @@ let intern_state magic filename = close_in channel; v with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) + CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a - with Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> + CErrors.errorlabstrm "with_magic_number_check" + (str"File " ++ str fname ++ strbrk" has bad magic number " ++ + int actual ++ str" (expected " ++ int expected ++ str")." ++ + spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") (* Time stamps. *) @@ -284,13 +299,13 @@ let with_time time f x = let y = f x in let tend = get_time() in let msg2 = if time then "" else " (successful)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if time then "" else "Finished failing transaction in " in let msg2 = if time then "" else " (failure)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e let process_id () = |