diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 378 |
1 files changed, 140 insertions, 238 deletions
diff --git a/lib/system.ml b/lib/system.ml index 8f436366..73095f9c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,126 +9,10 @@ (* $Id$ *) open Pp +open Errors open Util open Unix -(* Expanding shell variables and home-directories *) - -let safe_getenv_def var def = - try - Sys.getenv var - with Not_found -> - warning ("Environment variable "^var^" not found: using '"^def^"' ."); - flush_all (); - def - -let getenv_else s dft = try Sys.getenv s with Not_found -> dft - -(* On win32, the home directory is probably not in $HOME, but in - some other environment variable *) - -let home = - try Sys.getenv "HOME" with Not_found -> - try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> - try Sys.getenv "USERPROFILE" with Not_found -> - warning ("Cannot determine user home directory, using '.' ."); - flush_all (); - Filename.current_dir_name - -let safe_getenv n = safe_getenv_def n ("$"^n) - -let rec expand_atom s i = - let l = String.length s in - if i<l && (is_digit s.[i] or is_letter s.[i] or s.[i] = '_') - then expand_atom s (i+1) - else i - -let rec expand_macros s i = - let l = String.length s in - if i=l then s else - match s.[i] with - | '$' -> - let n = expand_atom s (i+1) in - let v = safe_getenv (String.sub s (i+1) (n-i-1)) in - let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in - expand_macros s (i + String.length v) - | '~' when i = 0 -> - let n = expand_atom s (i+1) in - let v = - if n=i+1 then home - else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir - in - let s = v^(String.sub s n (l-n)) in - expand_macros s (String.length v) - | c -> expand_macros s (i+1) - -let expand_path_macros s = expand_macros s 0 - -(* Files and load path. *) - -type physical_path = string -type load_path = physical_path list - -let physical_path_of_string s = s -let string_of_physical_path p = p - -(* - * Split a path into a list of directories. A one-liner with Str, but Coq - * doesn't seem to use this library at all, so here is a slighly longer version. - *) - -let lpath_from_path path path_separator = - let n = String.length path in - let rec aux i l = - if i < n then - let j = - try String.index_from path i path_separator - with Not_found -> n - in - let dir = String.sub path i (j-i) in - aux (j+1) (dir::l) - else - l - in List.rev (aux 0 []) - -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - let l = String.length p in - if l > n && String.sub p 0 n = curdir then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - let l = String.length p in - if l > n && String.sub p 0 n = cwd then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - (* All subdirectories, recursively *) let exists_dir dir = @@ -139,9 +23,9 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames let ok_dirname f = - f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && - try ignore (check_ident f); true - with e when e <> Sys.Break -> false + not (String.is_empty f) && f.[0] != '.' && + not (String.List.mem f !skipped_dirnames) && + (match Unicode.ident_refutation f with None -> true | _ -> false) let all_subdirs ~unix_path:root = let l = ref [] in @@ -154,11 +38,13 @@ let all_subdirs ~unix_path:root = if ok_dirname f then let file = Filename.concat dir f in try - if (stat file).st_kind = S_DIR then begin - let newrel = rel@[f] in + begin match (stat file).st_kind with + | S_DIR -> + let newrel = rel @ [f] in add file newrel; traverse file newrel - end + | _ -> () + end with Unix_error (e,s1,s2) -> () done with End_of_file -> @@ -167,28 +53,43 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l +let rec search paths test = + match paths with + | [] -> [] + | lpe :: rem -> test lpe @ search rem test + let where_in_path ?(warn=true) path filename = - let rec search = function - | lpe :: rem -> - let f = Filename.concat lpe filename in - if Sys.file_exists f - then (lpe,f) :: search rem - else search rem - | [] -> [] in - let rec check_and_warn l = - match l with - | [] -> raise Not_found - | (lpe, f) :: l' -> - if warn & l' <> [] then - 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); - (lpe, f) in - check_and_warn (search path) + 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) + | _ -> () + in + (lpe, f) + in + check_and_warn (search path (fun lpe -> + let f = Filename.concat lpe filename in + if Sys.file_exists f then [lpe,f] else [])) + +let where_in_path_rex path rex = + search path (fun lpe -> + try + let files = Sys.readdir lpe in + CList.map_filter (fun name -> + try + ignore(Str.search_forward rex name 0); + Some (lpe,Filename.concat lpe name) + with Not_found -> None) + (Array.to_list files) + with Sys_error _ -> []) let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then @@ -209,56 +110,87 @@ let is_in_path lpath filename = try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false -let path_separator = if Sys.os_type = "Unix" then ':' else ';' - let is_in_system_path filename = - let path = try Sys.getenv "PATH" + let path = try Sys.getenv "PATH" with Not_found -> error "system variable PATH not found" in - let lpath = lpath_from_path path path_separator in + let lpath = CUnix.path_to_list path in is_in_path lpath filename -let make_suffix name suffix = - if Filename.check_suffix name suffix then name else (name ^ suffix) - -let file_readable_p name = - try access name [R_OK];true with Unix_error (_, _, _) -> false - let open_trapping_failure name = try open_out_bin name - with e when e <> Sys.Break -> error ("Can't open " ^ name) + with e when Errors.noncritical e -> error ("Can't open " ^ name) let try_remove filename = try Sys.remove filename - with e when e <> Sys.Break -> - msgnl (str"Warning: " ++ str"Could not remove file " ++ - str filename ++ str" which is corrupted!" ) + with e when Errors.noncritical e -> + msg_warning + (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let marshal_out ch v = Marshal.to_channel ch v [] +let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.") + +let input_binary_int f ch = + try input_binary_int ch + with + | End_of_file -> error_corrupted f "premature end of file" + | Failure s -> error_corrupted f s +let output_binary_int ch x = output_binary_int ch x; flush ch + +let marshal_out ch v = Marshal.to_channel ch v []; flush ch let marshal_in filename ch = try Marshal.from_channel ch with - | End_of_file -> error "corrupted file: reached end of file" - | Failure _ (* e.g. "truncated object" *) -> - error (filename ^ " is corrupted, try to rebuild it.") + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s -> error_corrupted filename s + +let digest_out = Digest.output +let digest_in filename ch = + try Digest.input ch + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s -> error_corrupted filename s + +let marshal_out_segment f ch v = + let start = pos_out ch in + output_binary_int ch 0; (* dummy value for stop *) + marshal_out ch v; + let stop = pos_out ch in + seek_out ch start; + output_binary_int ch stop; + seek_out ch stop; + digest_out ch (Digest.file f) + +let marshal_in_segment f ch = + let stop = (input_binary_int f ch : int) in + let v = marshal_in f ch in + let digest = digest_in f ch in + v, stop, digest + +let skip_in_segment f ch = + let stop = (input_binary_int f ch : int) in + seek_in ch stop; + stop, digest_in f ch exception Bad_magic_number of string -let raw_extern_intern magic suffix = - let extern_state name = - let filename = make_suffix name suffix in +let raw_extern_intern magic = + let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename,channel + filename, channel and intern_state filename = - let channel = open_in_bin filename in - if input_binary_int channel <> magic then - raise (Bad_magic_number filename); - channel + 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) -let extern_intern ?(warn=true) magic suffix = - let (raw_extern,raw_intern) = raw_extern_intern magic suffix in +let extern_intern ?(warn=true) magic = + let (raw_extern,raw_intern) = raw_extern_intern magic in let extern_state name val_0 = try let (filename,channel) = raw_extern name in @@ -266,11 +198,13 @@ let extern_intern ?(warn=true) magic suffix = marshal_out channel val_0; close_out channel with reraise -> - begin try_remove filename; raise reraise end + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in + 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; @@ -284,79 +218,47 @@ 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 () ++ + (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") -(* Communication through files with another executable *) - -let connect writefun readfun com = - let name = Filename.basename com in - let tmp_to = Filename.temp_file ("coq-"^name^"-in") ".xml" in - let tmp_from = Filename.temp_file ("coq-"^name^"-out") ".xml" in - let ch_to_in,ch_to_out = - try open_in tmp_to, open_out tmp_to - with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in - let ch_from_in,ch_from_out = - try open_in tmp_from, open_out tmp_from - with Sys_error s -> - close_out ch_to_out; close_in ch_to_in; - error ("Cannot set connection from "^com^"("^s^")") in - writefun ch_to_out; - close_out ch_to_out; - let pid = - let ch_to' = Unix.descr_of_in_channel ch_to_in in - let ch_from' = Unix.descr_of_out_channel ch_from_out in - try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout - with Unix.Unix_error (err,_,_) -> - close_in ch_to_in; close_in ch_from_in; close_out ch_from_out; - unlink tmp_from; unlink tmp_to; - error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in - close_in ch_to_in; - close_out ch_from_out; - (match snd (Unix.waitpid [] pid) with - | Unix.WEXITED 127 -> error (com^": cannot execute") - | Unix.WEXITED 0 -> () - | _ -> error (com^" exited abnormally")); - let a = readfun ch_from_in in - close_in ch_from_in; - unlink tmp_from; - unlink tmp_to; - a - -let run_command converter f c = - let result = Buffer.create 127 in - let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in - let n = ref 0 in - let ne = ref 0 in - - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; - !n+ !ne <> 0 - do - let r = converter (String.sub buff 0 !n) in - f r; - Buffer.add_string result r; - let r = converter (String.sub buffe 0 !ne) in - f r; - Buffer.add_string result r - done; - (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) - (* Time stamps. *) type time = float * float * float let get_time () = - let t = times () in - (time(), t.tms_utime, t.tms_stime) + let t = Unix.times () in + (Unix.gettimeofday(), t.tms_utime, t.tms_stime) -let time_difference (t1,_,_) (t2,_,_) = t2 -. t1 +(* Keep only 3 significant digits *) +let round f = (floor (f *. 1e3)) *. 1e-3 + +let time_difference (t1,_,_) (t2,_,_) = round (t2 -. t1) let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = - real (stopreal -. startreal) ++ str " secs " ++ + real (round (stopreal -. startreal)) ++ str " secs " ++ str "(" ++ - real ((-.) ustop ustart) ++ str "u" ++ + real (round (ustop -. ustart)) ++ str "u" ++ str "," ++ - real ((-.) sstop sstart) ++ str "s" ++ + real (round (sstop -. sstart)) ++ str "s" ++ str ")" + +let with_time time f x = + let tstart = get_time() in + let msg = if time 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 + 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); + 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 ())) + |