1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 2 Jul 2010 15:00:43 +0200
Subject: [PATCH] Remove dependency to Unix from module Profile
Applied-Upstream: https://gforge.inria.fr/scm/viewvc.php?view=rev&root=coq&revision=13234
Signed-off-by: Stephane Glondu <steph@glondu.net>
---
Makefile.build | 4 ++--
lib/profile.ml | 8 +++++---
lib/profile.mli | 4 +---
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/Makefile.build b/Makefile.build
index 148bb62..c4358ce 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -782,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO)
parsing/grammar.cma: $(GRAMMARCMO)
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
# toplevel/mltop.ml4 (ifdef Byte)
diff --git a/lib/profile.ml b/lib/profile.ml
index dd7e977..40bfba3 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -17,8 +17,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 () =
@@ -157,7 +156,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 0937e9e..1e28834 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -10,12 +10,10 @@
(*s 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 :
--
|
