diff options
| author | glondu | 2010-07-02 12:54:57 +0000 |
|---|---|---|
| committer | glondu | 2010-07-02 12:54:57 +0000 |
| commit | dacb4b76afe554f1a1e17d981bc98d9fc3a8e807 (patch) | |
| tree | 0c6de9a4f3a7338f32f70520d9647e6f3a356497 /lib | |
| parent | 2de4563cb6192e638df4172c725ec8814e6eb112 (diff) | |
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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/profile.ml | 8 | ||||
| -rw-r--r-- | lib/profile.mli | 5 |
2 files changed, 6 insertions, 7 deletions
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 : |