From 919b30f6d188fcfc6dc40b364d54c0458be3591e Mon Sep 17 00:00:00 2001 From: fkirchne Date: Fri, 28 May 2010 16:40:18 +0000 Subject: Use existing functions to reimplement search_exe. Most of the code in search_exe_in_path was about parsing the PATH into a list of directories, which is now done in function lpath_from_path. Existence of the file is checked using already existing functions, so that duplication is minimized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13033 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/system.ml | 325 --------------------------------------------------------- lib/system.mli | 1 + 2 files changed, 1 insertion(+), 325 deletions(-) delete mode 100644 lib/system.ml diff --git a/lib/system.ml b/lib/system.ml deleted file mode 100644 index 2391b99e0..000000000 --- a/lib/system.ml +++ /dev/null @@ -1,325 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - warning ("Environment variable "^var^" not found: using '"^def^"' ."); - flush Pervasives.stdout; - def - -let getenv_else s dft = try Sys.getenv s with Not_found -> dft - -let home = (safe_getenv_def "HOME" ".") - -let safe_getenv n = safe_getenv_def n ("$"^n) - -let rec expand_atom s i = - let l = String.length s in - if i - 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 - -(* 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 - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - 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 = - try let _ = opendir dir in true with Unix_error _ -> false - -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 _ -> false - -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 - if (stat file).st_kind = S_DIR then begin - 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 - in - if exists_dir root then traverse root []; - List.rev !l - -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 find_file_in_path ?(warn=true) paths filename = - if not (Filename.is_implicit filename) then - if Sys.file_exists filename then - let root = Filename.dirname filename in - root, filename - else - errorlabstrm "System.find_file_in_path" - (hov 0 (str "Can't find file" ++ spc () ++ str filename)) - else - try where_in_path ~warn paths filename - with Not_found -> - errorlabstrm "System.find_file_in_path" - (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ - str "on loadpath")) - -let is_in_path lpath filename = - try ignore (where_in_path ~warn:false lpath filename); true - with Not_found -> false - -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 _ -> error ("Can't open " ^ name) - -let try_remove filename = - try Sys.remove filename - with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++ - str filename ++ str" which is corrupted!" ) - -let marshal_out ch v = Marshal.to_channel ch v [] -let marshal_in ch = - try Marshal.from_channel ch - with End_of_file -> error "corrupted file: reached end of file" - -exception Bad_magic_number of string - -let raw_extern_intern magic suffix = - let extern_state name = - let filename = make_suffix name suffix in - let channel = open_trapping_failure filename in - output_binary_int channel magic; - 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 - 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_state name val_0 = - try - let (filename,channel) = raw_extern name in - try - marshal_out channel val_0; - close_out channel - with e -> - begin try_remove filename; raise e end - 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 channel = raw_intern filename in - let v = marshal_in channel in - close_in channel; - v - with Sys_error s -> - error("System error: " ^ s) - in - (extern_state,intern_state) - -(* 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) - -let path_separator = if Sys.os_type = "Unix" then ':' else ';' - -let search_exe_in_path exe = - try - let path = Sys.getenv "PATH" in - let n = String.length path in - let rec aux i = - 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 - let exe = Filename.concat dir exe in - if Sys.file_exists exe then Some exe else aux (i+1) - else - None - in aux 0 - with Not_found -> None - -(* Time stamps. *) - -type time = float * float * float - -let process_time () = - let t = times () in - (t.tms_utime, t.tms_stime) - -let get_time () = - let t = times () in - (time(), t.tms_utime, t.tms_stime) - -let time_difference (t1,_,_) (t2,_,_) = t2 -. t1 - -let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = - real (stopreal -. startreal) ++ str " secs " ++ - str "(" ++ - real ((-.) ustop ustart) ++ str "u" ++ - str "," ++ - real ((-.) sstop sstart) ++ str "s" ++ - str ")" diff --git a/lib/system.mli b/lib/system.mli index d8a4088d0..ce5fd8b01 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -23,6 +23,7 @@ val exclude_search_in_dirname : string -> unit val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool +val is_in_system_path : string -> bool val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string val physical_path_of_string : string -> physical_path -- cgit v1.2.3