From dacb4b76afe554f1a1e17d981bc98d9fc3a8e807 Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 2 Jul 2010 12:54:57 +0000
Subject: Remove dependency to Unix from module Profile

Looking at the source code of Sys.time reveals that it is exactly what
is computed by Profile.get_time. This can also be tested by evaluating:

  Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);;

in an OCaml toplevel with Unix.

This allows to put Profile in grammar.cma without the dependency to
unix.cma while preprocessing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/profile.ml  | 8 +++++---
 lib/profile.mli | 5 +----
 2 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index d154478177..cde5ed5999 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -15,8 +15,7 @@ let float_of_time t = float_of_int t /. 100.
 let time_of_float f = int_of_float (f *. 100.)
 
 let get_time () =
-  let  {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
-  time_of_float (ut +. st)
+  time_of_float (Sys.time ())
 
 (* Since ocaml 3.01, gc statistics are in float *)
 let get_alloc () =
@@ -155,7 +154,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
 (* Unix measure of time is approximative and shoitt delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
-   approximation *)
+   approximation.
+   Note: Sys.time is the same as:
+     Unix.(let x = times () in x.tms_utime +. x.tms_stime)
+ *)
 
 (*
 ----------        start profile for f1
diff --git a/lib/profile.mli b/lib/profile.mli
index 5bcebfb0dd..56f78cba8a 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -8,12 +8,9 @@
 
 (** {6 This program is a small time and allocation profiler for Objective Caml } *)
 
-(*i It requires the UNIX library *)
-
 (** Adapted from Christophe Raffalli *)
 
-(** To use it, link it with the program you want to profile (do not forget
-"-cclib -lunix -custom unix.cma" among the link options).
+(** To use it, link it with the program you want to profile.
 
 To trace a function "f" you first need to get a key for it by using :
 
-- 
cgit v1.2.3