modules profile, Coqinit et Coqtop (=main)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 8 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 9da302d30..5422bc465 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -44,7 +44,14 @@ let all_subdirs dir =
 
 let radd_path dir = List.iter add_path (all_subdirs dir)
 
+let safe_getenv_def var def =
+  try 
+    Sys.getenv var
+  with Not_found ->
+    warning ("Environnement variable "^var^" not found: using '"^def^"' .");
+    def
 
+let home = (safe_getenv_def "HOME" ".")
 
 (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *)
 let glob s = s
@@ -82,6 +89,9 @@ let 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 na =
+  try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false
+
 let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)
@@ -141,11 +151,22 @@ let (extern_intern :
 
 (* Time stamps. *)
 
-type time_stamp = float
-
-let get_time_stamp () = Unix.time()
-
-let compare_time_stamps t1 t2 =
-  let dt = t2 -. t1 in
-  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
-
+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")" >]