src/Pure/General/timing.scala
author wenzelm
Wed, 09 Mar 2016 16:42:30 +0100
changeset 62571 2fd90993a928
parent 57912 dd9550f84106
child 62587 e31bf8ed5397
permissions -rw-r--r--
print timing like lib/scripts/timestop.bash;
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
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
     2
    Module:     PIDE
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     4
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     5
Basic support for time measurement.
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
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     8
package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     9
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    10
62571
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    11
import java.util.Locale
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    12
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    13
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    14
object Timing
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    15
{
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    16
  val zero = Timing(Time.zero, Time.zero, Time.zero)
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    17
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    18
  def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    19
    if (enabled) {
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    20
      val start = Time.now()
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    21
      val result = Exn.capture(e)
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    22
      val stop = Time.now()
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    23
56691
ad5d7461b370 tuned signature, in accordance to ML version;
wenzelm
parents: 55618
diff changeset
    24
      val timing = stop - start
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    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
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    27
          (if (message == null || message.isEmpty) "" else message + ": ") +
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    28
            timing.message + " elapsed time")
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    29
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    30
      Exn.release(result)
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    31
    }
4605d4341b8b some builtin session timing;
wenzelm
parents: 46768
diff changeset
    32
    else e
45664
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    33
}
ac6e704dcd12 tuned signature (according to ML version);
wenzelm
parents: 45249
diff changeset
    34
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    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
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    37
  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    38
51587
7050c4656fd8 more operations on Time, Timing;
wenzelm
parents: 47653
diff changeset
    39
  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
    40
62571
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    41
  def message_resources: String =
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    42
  {
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    43
    val resources = cpu + gc
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    44
    val t1 = elapsed.seconds
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    45
    val t2 = resources.seconds
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    46
    val factor =
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    47
      if (t1 >= 5.0 && t2 >= 5.0)
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    48
        String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    49
      else ""
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    50
    elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    51
  }
2fd90993a928 print timing like lib/scripts/timestop.bash;
wenzelm
parents: 57912
diff changeset
    52
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    53
  def message: String =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    54
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
46768
46acd255810d relevant timing as in ML;
wenzelm
parents: 45674
diff changeset
    55
57912
wenzelm
parents: 56782
diff changeset
    56
  override def toString: String = message
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    57
}