author | wenzelm |
Thu, 10 Mar 2016 12:11:23 +0100 | |
changeset 62587 | e31bf8ed5397 |
parent 62571 | 2fd90993a928 |
child 64084 | bca58a11efde |
permissions | -rw-r--r-- |
40393 | 1 |
/* Title: Pure/General/timing.scala |
46768 | 2 |
Module: PIDE |
40393 | 3 |
Author: Makarius |
4 |
||
5 |
Basic support for time measurement. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
45664 | 10 |
|
62571 | 11 |
import java.util.Locale |
12 |
||
13 |
||
45664 | 14 |
object Timing |
15 |
{ |
|
51587 | 16 |
val zero = Timing(Time.zero, Time.zero, Time.zero) |
17 |
||
47653 | 18 |
def timeit[A](message: String, enabled: Boolean = true)(e: => A) = |
19 |
if (enabled) { |
|
56691 | 20 |
val start = Time.now() |
47653 | 21 |
val result = Exn.capture(e) |
56691 | 22 |
val stop = Time.now() |
46768 | 23 |
|
56691 | 24 |
val timing = stop - start |
47653 | 25 |
if (timing.is_relevant) |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56691
diff
changeset
|
26 |
Output.warning( |
47653 | 27 |
(if (message == null || message.isEmpty) "" else message + ": ") + |
28 |
timing.message + " elapsed time") |
|
46768 | 29 |
|
47653 | 30 |
Exn.release(result) |
31 |
} |
|
32 |
else e |
|
45664 | 33 |
} |
34 |
||
51587 | 35 |
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
|
36 |
{ |
46768 | 37 |
def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant |
38 |
||
51587 | 39 |
def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) |
40 |
||
62587
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
41 |
def message: String = |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
42 |
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
|
43 |
|
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
44 |
def resources: Time = cpu + gc |
62571 | 45 |
def message_resources: String = |
46 |
{ |
|
47 |
val resources = cpu + gc |
|
48 |
val t1 = elapsed.seconds |
|
49 |
val t2 = resources.seconds |
|
50 |
val factor = |
|
62587
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
51 |
if (t1 >= 3.0 && t2 >= 3.0) |
62571 | 52 |
String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1)) |
53 |
else "" |
|
62587
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
54 |
if (t2 >= 3.0) |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
55 |
elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
56 |
else |
e31bf8ed5397
clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents:
62571
diff
changeset
|
57 |
elapsed.message_hms + " elapsed time" + factor |
62571 | 58 |
} |
59 |
||
57912 | 60 |
override def toString: String = message |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
61 |
} |