author | wenzelm |
Fri, 28 Apr 2017 17:17:23 +0200 | |
changeset 65613 | cfcafe9824d1 |
parent 65597 | b408ca224954 |
child 65617 | 823bbc467dfa |
permissions | -rw-r--r-- |
40393 | 1 |
/* Title: Pure/General/timing.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Basic support for time measurement. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
45664 | 9 |
|
62571 | 10 |
import java.util.Locale |
11 |
||
12 |
||
45664 | 13 |
object Timing |
14 |
{ |
|
51587 | 15 |
val zero = Timing(Time.zero, Time.zero, Time.zero) |
16 |
||
47653 | 17 |
def timeit[A](message: String, enabled: Boolean = true)(e: => A) = |
18 |
if (enabled) { |
|
56691 | 19 |
val start = Time.now() |
47653 | 20 |
val result = Exn.capture(e) |
56691 | 21 |
val stop = Time.now() |
46768 | 22 |
|
56691 | 23 |
val timing = stop - start |
47653 | 24 |
if (timing.is_relevant) |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56691
diff
changeset
|
25 |
Output.warning( |
47653 | 26 |
(if (message == null || message.isEmpty) "" else message + ": ") + |
27 |
timing.message + " elapsed time") |
|
46768 | 28 |
|
47653 | 29 |
Exn.release(result) |
30 |
} |
|
31 |
else e |
|
65597 | 32 |
|
33 |
val encode: XML.Encode.T[Timing] = (t: Timing) => |
|
34 |
{ |
|
35 |
import XML.Encode._ |
|
36 |
triple(Time.encode, Time.encode, Time.encode)(t.elapsed, t.cpu, t.gc) |
|
37 |
} |
|
38 |
||
39 |
val decode: XML.Decode.T[Timing] = (body: XML.Body) => |
|
40 |
{ |
|
41 |
import XML.Decode._ |
|
42 |
val (elapsed, cpu, gc) = triple(Time.decode, Time.decode, Time.decode)(body) |
|
43 |
Timing(elapsed, cpu, gc) |
|
44 |
} |
|
65613 | 45 |
|
46 |
def write(t: Timing): Bytes = |
|
47 |
if (t.is_zero) Bytes.empty |
|
48 |
else Bytes(YXML.string_of_body(encode(t))) |
|
49 |
||
50 |
def read(bs: Bytes): Timing = |
|
51 |
if (bs.isEmpty) zero |
|
52 |
else decode(YXML.parse_body(bs.text)) |
|
45664 | 53 |
} |
54 |
||
51587 | 55 |
sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
56 |
{ |
64089 | 57 |
def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero |
46768 | 58 |
def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant |
59 |
||
64084 | 60 |
def resources: Time = cpu + gc |
61 |
||
62 |
def factor: Option[Double] = |
|
63 |
{ |
|
64 |
val t1 = elapsed.seconds |
|
65 |
val t2 = resources.seconds |
|
66 |
if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None |
|
67 |
} |
|
68 |
||
51587 | 69 |
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) |
70 |
||
62587
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
71 |
def message: String = |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
72 |
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
73 |
|
62571 | 74 |
def message_resources: String = |
75 |
{ |
|
64084 | 76 |
val factor_text = |
77 |
factor match { |
|
78 |
case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f)) |
|
79 |
case None => "" |
|
80 |
} |
|
81 |
if (resources.seconds >= 3.0) |
|
82 |
elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text |
|
62587
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
83 |
else |
64084 | 84 |
elapsed.message_hms + " elapsed time" + factor_text |
62571 | 85 |
} |
86 |
||
57912 | 87 |
override def toString: String = message |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
88 |
} |