diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/lib/system.ml b/lib/system.ml index 4b99de70..dfede29e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* $Id$ *) @@ -52,7 +54,10 @@ 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 (readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) + +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = @@ -62,10 +67,10 @@ let exists_in_dir_respecting_case dir bf = let contents, fresh = try (* in batch mode, assume the directory content is still fresh *) - StrMap.find dir !dirmap, !Flags.batch_mode + StrMap.find dir !dirmap, !trust_file_cache 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 + if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true else cache_dir dir, true in StrSet.mem bf contents || not fresh && @@ -80,7 +85,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 (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f + in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f let rec search paths test = match paths with @@ -131,7 +136,7 @@ let find_file_in_path ?(warn=true) paths filename = let root = Filename.dirname filename in root, filename else - CErrors.errorlabstrm "System.find_file_in_path" + CErrors.user_err ~hdr:"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 @@ -139,7 +144,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 -> - CErrors.errorlabstrm "System.find_file_in_path" + CErrors.user_err ~hdr:"System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) @@ -162,7 +167,7 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name with e when CErrors.noncritical e -> - CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name) + CErrors.user_err ~hdr:"System.open" (str "Can't open " ++ str name) let warn_cannot_remove_file = CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" @@ -174,7 +179,7 @@ let try_remove filename = warn_cannot_remove_file filename let error_corrupted file s = - CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -251,7 +256,7 @@ let extern_state magic filename val_0 = let () = try_remove filename in iraise reraise with Sys_error s -> - CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s) + CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s) let intern_state magic filename = try @@ -260,12 +265,12 @@ let intern_state magic filename = close_in channel; v with Sys_error s -> - CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s) + CErrors.user_err ~hdr:"System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> - CErrors.errorlabstrm "with_magic_number_check" + CErrors.user_err ~hdr:"with_magic_number_check" (str"File " ++ str fname ++ strbrk" has bad magic number " ++ int actual ++ str" (expected " ++ int expected ++ str")." ++ spc () ++ @@ -292,23 +297,18 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time time f x = +let with_time ~batch f x = let tstart = get_time() in - let msg = if time then "" else "Finished transaction in " in + let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in - let msg2 = if time then "" else " (successful)" in + let msg2 = if batch then "" else " (successful)" in 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 + let msg = if batch then "" else "Finished failing transaction in " in + let msg2 = if batch then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e - -let process_id () = - if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id - else Printf.sprintf "master:%d" (Thread.id (Thread.self ())) - |