From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 lib/system.ml | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'lib/system.ml')

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 ()))
-    
-- 
cgit v1.2.3