src/Pure/General/timing.ML
author wenzelm
Fri, 23 Mar 2018 16:07:20 +0100
changeset 67932 04352338f7f3
parent 67001 b34fbf33a7ea
child 74158 1cb0ad6f9a2d
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: 40391
diff changeset
     1
(*  Title:      Pure/General/timing.ML
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     3
40336
wenzelm
parents: 40300
diff changeset
     4
Basic support for time measurement.
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     5
*)
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
     6
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
     7
signature BASIC_TIMING =
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
     8
sig
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
     9
  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    10
  val timeit: (unit -> 'a) -> 'a
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    11
  val timeap: ('a -> 'b) -> 'a -> 'b
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    12
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    13
end
40300
d4487353b3a0 added convenience operation seconds: real -> time;
wenzelm
parents: 32935
diff changeset
    14
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    15
signature TIMING =
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    16
sig
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    17
  include BASIC_TIMING
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    18
  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    19
  type start
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    20
  val start: unit -> start
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    21
  val result: start -> timing
42013
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    22
  val timing: ('a -> 'b) -> 'a -> timing * 'b
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51217
diff changeset
    23
  val is_relevant_time: Time.time -> bool
44440
aa2abd81f460 ignore irrelevant timings;
wenzelm
parents: 42819
diff changeset
    24
  val is_relevant: timing -> bool
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    25
  val message: timing -> string
67932
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
    26
  val protocol_message: string -> Position.T -> timing -> unit
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
    27
  val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    28
end
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    29
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    30
structure Timing: TIMING =
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    31
struct
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    32
51217
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 50781
diff changeset
    33
(* type timing *)
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    34
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    35
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    36
51217
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 50781
diff changeset
    37
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 50781
diff changeset
    38
(* timer control *)
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 50781
diff changeset
    39
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    40
abstype start = Start of
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    41
  Timer.real_timer * Time.time * Timer.cpu_timer *
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    42
    {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    43
with
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    44
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    45
fun start () =
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    46
  let
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    47
    val real_timer = Timer.startRealTimer ();
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    48
    val real_time = Timer.checkRealTimer real_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    49
    val cpu_timer = Timer.startCPUTimer ();
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    50
    val cpu_times = Timer.checkCPUTimes cpu_timer;
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    51
  in Start (real_timer, real_time, cpu_timer, cpu_times) end;
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    52
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    53
fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
31686
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    54
  let
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    55
    val real_time2 = Timer.checkRealTimer real_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    56
    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    57
    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    58
      Timer.checkCPUTimes cpu_timer;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    59
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    60
    val elapsed = real_time2 - real_time;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    61
    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
e54ae15335a1 more detailed start_timing/end_timing (in timing.ML);
wenzelm
parents:
diff changeset
    62
    val cpu = usr2 - usr + sys2 - sys + gc;
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    63
  in {elapsed = elapsed, cpu = cpu, gc = gc} end;
32935
2218b970325a show direct GC time (which is included in CPU time);
wenzelm
parents: 31757
diff changeset
    64
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    65
end;
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    66
42013
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    67
fun timing f x =
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    68
  let
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    69
    val start = start ();
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    70
    val y = f x;
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    71
  in (result start, y) end;
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    72
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    73
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    74
(* timing messages *)
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    75
42819
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    76
val min_time = Time.fromMilliseconds 1;
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    77
62826
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 59149
diff changeset
    78
fun is_relevant_time time = time >= min_time;
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51217
diff changeset
    79
42819
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    80
fun is_relevant {elapsed, cpu, gc} =
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51217
diff changeset
    81
  is_relevant_time elapsed orelse
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51217
diff changeset
    82
  is_relevant_time cpu orelse
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51217
diff changeset
    83
  is_relevant_time gc;
42819
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    84
44440
aa2abd81f460 ignore irrelevant timings;
wenzelm
parents: 42819
diff changeset
    85
fun message {elapsed, cpu, gc} =
67000
1698e9ccef2d more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents: 66415
diff changeset
    86
  Value.print_time elapsed ^ "s elapsed time, " ^
1698e9ccef2d more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents: 66415
diff changeset
    87
  Value.print_time cpu ^ "s cpu time, " ^
1698e9ccef2d more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents: 66415
diff changeset
    88
  Value.print_time gc ^ "s GC time" handle Time.Time => "";
44440
aa2abd81f460 ignore irrelevant timings;
wenzelm
parents: 42819
diff changeset
    89
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    90
fun cond_timeit enabled msg e =
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    91
  if enabled then
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
    92
    let
51606
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
    93
      val (t, result) = timing (Exn.interruptible_capture e) ();
42819
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    94
      val _ =
51606
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
    95
        if is_relevant t then
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
    96
          let val end_msg = message t
42819
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    97
          in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
cce39fdaad7b only show relevant timing;
wenzelm
parents: 42042
diff changeset
    98
        else ();
42013
1694cc477045 pure Timing.timing, without any exception handling;
wenzelm
parents: 42012
diff changeset
    99
    in Exn.release result end
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   100
  else e ();
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   101
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   102
fun timeit e = cond_timeit true "" e;
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   103
fun timeap f x = timeit (fn () => f x);
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   104
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   105
67932
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
   106
fun protocol_message name pos t =
59149
0070053570c4 suppress irrelevant timing messages (the majority);
wenzelm
parents: 56333
diff changeset
   107
  if is_relevant t then
67932
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
   108
    let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
   109
    in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
59149
0070053570c4 suppress irrelevant timing messages (the majority);
wenzelm
parents: 56333
diff changeset
   110
  else ();
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51606
diff changeset
   111
67932
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
   112
fun protocol name pos f x =
51606
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
   113
  let
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
   114
    val (t, result) = timing (Exn.interruptible_capture f) x;
67932
04352338f7f3 clarified signature;
wenzelm
parents: 67001
diff changeset
   115
    val _ = protocol_message name pos t;
51606
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
   116
  in Exn.release result end;
2843cc095a57 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents: 51228
diff changeset
   117
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   118
end;
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   119
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   120
structure Basic_Timing: BASIC_TIMING = Timing;
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 40393
diff changeset
   121
open Basic_Timing;