src/Pure/General/timing.scala
author wenzelm
Thu, 25 May 2017 17:28:11 +0200
changeset 65920 9e65c03e94da
parent 65617 823bbc467dfa
child 67858 cba5c5657378
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/timing.scala
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     3
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
     4
Support for time measurement.
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     5
*/
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     6
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     8
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
     9
62571
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    10
import java.util.Locale
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    11
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    12
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    13
object Timing
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    14
{
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    15
  val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    16
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    17
  def timeit[A](
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    18
    message: String = "",
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    19
    enabled: Boolean = true,
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    20
    output: String => Unit = Output.warning(_))(e: => A): A =
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    21
  {
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    22
    if (enabled) {
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    23
      val start = Time.now()
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    24
      val result = Exn.capture(e)
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    25
      val stop = Time.now()
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    26
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    27
      val timing = stop - start
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    28
      if (timing.is_relevant) {
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    29
        output(
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    30
          (if (message == null || message == "") "" else message + ": ") +
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    31
            timing.message + " elapsed time")
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    32
      }
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    33
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    34
      Exn.release(result)
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    35
    }
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    36
    else e
65920
9e65c03e94da clarified signature;
wenzelm
parents: 65617
diff changeset
    37
  }
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    38
}
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    39
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    40
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
    41
{
64089
10d719dbb3ee more permissive timing data;
wenzelm
parents: 64084
diff changeset
    42
  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    43
  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    44
64084
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    45
  def resources: Time = cpu + gc
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    46
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    47
  def factor: Option[Double] =
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    48
  {
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    49
    val t1 = elapsed.seconds
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    50
    val t2 = resources.seconds
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    51
    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    52
  }
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    53
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    54
  def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    55
62587
e31bf8ed5397 clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents: 62571
diff changeset
    56
  def message: String =
e31bf8ed5397 clarified messages, notably on Windows where CPU time of poly.exe is not measured;
wenzelm
parents: 62571
diff changeset
    57
    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
    58
62571
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    59
  def message_resources: String =
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    60
  {
64084
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    61
    val factor_text =
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    62
      factor match {
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    63
        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    64
        case None => ""
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    65
      }
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    66
    if (resources.seconds >= 3.0)
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    67
      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
    68
    else
64084
bca58a11efde more operations;
wenzelm
parents: 62587
diff changeset
    69
      elapsed.message_hms + " elapsed time" + factor_text
62571
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    70
  }
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    71
57912
wenzelm
parents: 56782
diff changeset
    72
  override def toString: String = message
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    73
}