support for prescient timing information within command transactions;
authorwenzelm
Tue Feb 19 12:58:32 2013 +0100 (2013-02-19 ago)
changeset 5121765ab2c4f4c32
parent 51216 e6e7685fc8f8
child 51218 6425a0d3b7ac
support for prescient timing information within command transactions;
src/Pure/General/timing.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/General/timing.ML	Tue Feb 19 10:55:11 2013 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Tue Feb 19 12:58:32 2013 +0100
     1.3 @@ -16,6 +16,8 @@
     1.4  sig
     1.5    include BASIC_TIMING
     1.6    type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
     1.7 +  val zero: timing
     1.8 +  val add: timing -> timing -> timing
     1.9    type start
    1.10    val start: unit -> start
    1.11    val result: start -> timing
    1.12 @@ -27,10 +29,20 @@
    1.13  structure Timing: TIMING =
    1.14  struct
    1.15  
    1.16 -(* timer control *)
    1.17 +(* type timing *)
    1.18  
    1.19  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
    1.20  
    1.21 +val zero = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
    1.22 +
    1.23 +fun add (t1: timing) (t2: timing) =
    1.24 + {elapsed = Time.+ (#elapsed t1, #elapsed t2),
    1.25 +  cpu = Time.+ (#cpu t1, #cpu t2),
    1.26 +  gc = Time.+ (#gc t1, #gc t2)};
    1.27 +
    1.28 +
    1.29 +(* timer control *)
    1.30 +
    1.31  abstype start = Start of
    1.32    Timer.real_timer * Time.time * Timer.cpu_timer *
    1.33      {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
     2.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 10:55:11 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 12:58:32 2013 +0100
     2.3 @@ -89,6 +89,9 @@
     2.4    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     2.5    val status: transition -> Markup.T -> unit
     2.6    val add_hook: (transition -> state -> state -> unit) -> unit
     2.7 +  val approximative_id: transition -> Properties.T
     2.8 +  val get_timing: transition -> Timing.timing
     2.9 +  val put_timing: Timing.timing -> transition -> transition
    2.10    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    2.11    val command: transition -> state -> state
    2.12    val proof_result: bool -> transition * transition list -> state ->
    2.13 @@ -340,16 +343,17 @@
    2.14    int_only: bool,            (*interactive-only*)
    2.15    print: bool,               (*print result state*)
    2.16    no_timing: bool,           (*suppress timing*)
    2.17 +  timing: Timing.timing,     (*prescient timing information*)
    2.18    trans: trans list};        (*primitive transitions (union)*)
    2.19  
    2.20 -fun make_transition (name, pos, int_only, print, no_timing, trans) =
    2.21 -  Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
    2.22 -    trans = trans};
    2.23 +fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
    2.24 +  Transition {name = name, pos = pos, int_only = int_only, print = print,
    2.25 +    no_timing = no_timing, timing = timing, trans = trans};
    2.26  
    2.27 -fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
    2.28 -  make_transition (f (name, pos, int_only, print, no_timing, trans));
    2.29 +fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
    2.30 +  make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
    2.31  
    2.32 -val empty = make_transition ("", Position.none, false, false, false, []);
    2.33 +val empty = make_transition ("", Position.none, false, false, false, Timing.zero, []);
    2.34  
    2.35  
    2.36  (* diagnostics *)
    2.37 @@ -367,26 +371,26 @@
    2.38  
    2.39  (* modify transitions *)
    2.40  
    2.41 -fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
    2.42 -  (name, pos, int_only, print, no_timing, trans));
    2.43 +fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
    2.44 +  (name, pos, int_only, print, no_timing, timing, trans));
    2.45  
    2.46 -fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
    2.47 -  (name, pos, int_only, print, no_timing, trans));
    2.48 +fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
    2.49 +  (name, pos, int_only, print, no_timing, timing, trans));
    2.50  
    2.51 -fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
    2.52 -  (name, pos, int_only, print, no_timing, trans));
    2.53 +fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
    2.54 +  (name, pos, int_only, print, no_timing, timing, trans));
    2.55  
    2.56 -val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
    2.57 -  (name, pos, int_only, print, true, trans));
    2.58 +val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
    2.59 +  (name, pos, int_only, print, true, timing, trans));
    2.60  
    2.61 -fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
    2.62 -  (name, pos, int_only, print, no_timing, tr :: trans));
    2.63 +fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
    2.64 +  (name, pos, int_only, print, no_timing, timing, tr :: trans));
    2.65  
    2.66 -val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
    2.67 -  (name, pos, int_only, print, no_timing, []));
    2.68 +val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
    2.69 +  (name, pos, int_only, print, no_timing, timing, []));
    2.70  
    2.71 -fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
    2.72 -  (name, pos, int_only, print, no_timing, trans));
    2.73 +fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
    2.74 +  (name, pos, int_only, print, no_timing, timing, trans));
    2.75  
    2.76  val print = set_print true;
    2.77  
    2.78 @@ -610,13 +614,19 @@
    2.79  
    2.80  (* apply transitions *)
    2.81  
    2.82 +fun approximative_id tr =
    2.83 +  (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    2.84 +
    2.85 +fun get_timing (Transition {timing, ...}) = timing;
    2.86 +fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
    2.87 +  (name, pos, int_only, print, no_timing, timing, trans));
    2.88 +
    2.89  local
    2.90  
    2.91  fun timing_message tr t =
    2.92    if Timing.is_relevant t then
    2.93      Output.protocol_message
    2.94 -      (Markup.command_timing :: (Markup.nameN, name_of tr) ::
    2.95 -        Position.properties_of (pos_of tr) @ Markup.timing_properties t) ""
    2.96 +      (Markup.command_timing :: approximative_id tr @ Markup.timing_properties t) ""
    2.97      handle Fail _ => ()
    2.98    else ();
    2.99  
     3.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 19 10:55:11 2013 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 12:58:32 2013 +0100
     3.3 @@ -92,6 +92,7 @@
     3.4    val elapsedN: string
     3.5    val cpuN: string
     3.6    val gcN: string
     3.7 +  val timing_propertiesN: string list
     3.8    val timing_properties: Timing.timing -> Properties.T
     3.9    val timingN: string val timing: Timing.timing -> T
    3.10    val subgoalsN: string
    3.11 @@ -333,6 +334,8 @@
    3.12  val cpuN = "cpu";
    3.13  val gcN = "gc";
    3.14  
    3.15 +val timing_propertiesN = [elapsedN, cpuN, gcN];
    3.16 +
    3.17  fun timing_properties {elapsed, cpu, gc} =
    3.18   [(elapsedN, Time.toString elapsed),
    3.19    (cpuN, Time.toString cpu),
     4.1 --- a/src/Pure/Thy/thy_info.ML	Tue Feb 19 10:55:11 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Feb 19 12:58:32 2013 +0100
     4.3 @@ -17,7 +17,8 @@
     4.4    val loaded_files: string -> Path.T list
     4.5    val remove_thy: string -> unit
     4.6    val kill_thy: string -> unit
     4.7 -  val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
     4.8 +  val use_theories: {last_timing: Toplevel.transition -> Timing.timing, master_dir: Path.T} ->
     4.9 +    (string * Position.T) list -> unit
    4.10    val use_thys: (string * Position.T) list -> unit
    4.11    val use_thy: string * Position.T -> unit
    4.12    val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
    4.13 @@ -221,7 +222,7 @@
    4.14  fun required_by _ [] = ""
    4.15    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    4.16  
    4.17 -fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
    4.18 +fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents =
    4.19    let
    4.20      val _ = kill_thy name;
    4.21      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
    4.22 @@ -234,7 +235,7 @@
    4.23      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    4.24  
    4.25      val (theory, present) =
    4.26 -      Thy_Load.load_thy update_time dir header (Path.position thy_path) text
    4.27 +      Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
    4.28          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    4.29      fun commit () = update_thy deps theory;
    4.30    in (theory, present, commit) end;
    4.31 @@ -259,9 +260,9 @@
    4.32  
    4.33  in
    4.34  
    4.35 -fun require_thys initiators dir strs tasks =
    4.36 -      fold_map (require_thy initiators dir) strs tasks |>> forall I
    4.37 -and require_thy initiators dir (str, require_pos) tasks =
    4.38 +fun require_thys last_timing initiators dir strs tasks =
    4.39 +      fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
    4.40 +and require_thy last_timing initiators dir (str, require_pos) tasks =
    4.41    let
    4.42      val path = Path.expand (Path.explode str);
    4.43      val name = Path.implode (Path.base path);
    4.44 @@ -280,7 +281,7 @@
    4.45  
    4.46            val parents = map (base_name o #1) imports;
    4.47            val (parents_current, tasks') =
    4.48 -            require_thys (name :: initiators)
    4.49 +            require_thys last_timing (name :: initiators)
    4.50                (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
    4.51  
    4.52            val all_current = current andalso parents_current;
    4.53 @@ -293,7 +294,8 @@
    4.54                    let
    4.55                      val update_time = serial ();
    4.56                      val load =
    4.57 -                      load_thy initiators update_time dep text (name, theory_pos) uses keywords;
    4.58 +                      load_thy last_timing initiators update_time dep
    4.59 +                        text (name, theory_pos) uses keywords;
    4.60                    in Task (parents, load) end);
    4.61  
    4.62            val tasks'' = new_entry name parents task tasks';
    4.63 @@ -305,10 +307,10 @@
    4.64  
    4.65  (* use_thy *)
    4.66  
    4.67 -fun use_thys_wrt dir arg =
    4.68 -  schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
    4.69 +fun use_theories {last_timing, master_dir} imports =
    4.70 +  schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
    4.71  
    4.72 -val use_thys = use_thys_wrt Path.current;
    4.73 +val use_thys = use_theories {last_timing = K Timing.zero, master_dir = Path.current};
    4.74  val use_thy = use_thys o single;
    4.75  
    4.76  
    4.77 @@ -318,7 +320,7 @@
    4.78    let
    4.79      val {name = (name, _), imports, ...} = header;
    4.80      val _ = kill_thy name;
    4.81 -    val _ = use_thys_wrt master_dir imports;
    4.82 +    val _ = use_theories {last_timing = K Timing.zero, master_dir = master_dir} imports;
    4.83      val _ = Thy_Header.define_keywords header;
    4.84      val parents = map (get_theory o base_name o fst) imports;
    4.85    in Thy_Load.begin_theory master_dir header parents end;
     5.1 --- a/src/Pure/Thy/thy_load.ML	Tue Feb 19 10:55:11 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Feb 19 12:58:32 2013 +0100
     5.3 @@ -22,8 +22,8 @@
     5.4    val use_ml: Path.T -> unit
     5.5    val exec_ml: Path.T -> generic_theory -> generic_theory
     5.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     5.7 -  val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
     5.8 -    theory list -> theory * unit future
     5.9 +  val load_thy: (Toplevel.transition -> Timing.timing) -> int -> Path.T -> Thy_Header.header ->
    5.10 +    Position.T -> string -> theory list -> theory * unit future
    5.11    val set_master_path: Path.T -> unit
    5.12    val get_master_path: unit -> Path.T
    5.13  end;
    5.14 @@ -214,10 +214,13 @@
    5.15    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
    5.16    |> Theory.checkpoint;
    5.17  
    5.18 -fun excursion init elements =
    5.19 +fun excursion last_timing init elements =
    5.20    let
    5.21      val immediate = not (Goal.future_enabled ());
    5.22  
    5.23 +    fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
    5.24 +    fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
    5.25 +
    5.26      fun proof_result (tr, trs) (st, _) =
    5.27        let
    5.28          val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
    5.29 @@ -225,7 +228,7 @@
    5.30        in (result, (st', pos')) end;
    5.31  
    5.32      fun element_result elem x =
    5.33 -      fold_map proof_result
    5.34 +      fold_map (proof_result o put_timings)
    5.35          (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
    5.36  
    5.37      val (results, (end_state, end_pos)) =
    5.38 @@ -234,7 +237,7 @@
    5.39      val thy = Toplevel.end_theory end_pos end_state;
    5.40    in (flat results, thy) end;
    5.41  
    5.42 -fun load_thy update_time master_dir header text_pos text parents =
    5.43 +fun load_thy last_timing update_time master_dir header text_pos text parents =
    5.44    let
    5.45      val time = ! Toplevel.timing;
    5.46  
    5.47 @@ -255,7 +258,7 @@
    5.48        (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    5.49  
    5.50      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    5.51 -    val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
    5.52 +    val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
    5.53      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    5.54  
    5.55      val present =
     6.1 --- a/src/Pure/Tools/build.ML	Tue Feb 19 10:55:11 2013 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 12:58:32 2013 +0100
     6.3 @@ -44,8 +44,8 @@
     6.4  fun no_document options =
     6.5    (case Options.string options "document" of "" => true | "false" => true | _ => false);
     6.6  
     6.7 -fun use_thys options =
     6.8 -  Thy_Info.use_thys
     6.9 +fun use_theories last_timing options =
    6.10 +  Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    6.11      |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    6.12      |> Unsynchronized.setmp print_mode
    6.13          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    6.14 @@ -71,10 +71,10 @@
    6.15      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    6.16      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    6.17  
    6.18 -fun use_theories (options, thys) =
    6.19 +fun use_theories_condition last_timing (options, thys) =
    6.20    let val condition = space_explode "," (Options.string options "condition") in
    6.21      (case filter_out (can getenv_strict) condition of
    6.22 -      [] => use_thys options (map (rpair Position.none) thys)
    6.23 +      [] => use_theories last_timing options (map (rpair Position.none) thys)
    6.24      | conds =>
    6.25          Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    6.26            " (undefined " ^ commas conds ^ ")\n"))
    6.27 @@ -117,7 +117,7 @@
    6.28  
    6.29        val res1 =
    6.30          theories |>
    6.31 -          (List.app use_theories
    6.32 +          (List.app (use_theories_condition (K Timing.zero))  (* FIXME *)
    6.33              |> Session.with_timing name verbose
    6.34              |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
    6.35              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")