--- a/etc/options Thu Feb 21 12:22:26 2013 +0100
+++ b/etc/options Thu Feb 21 15:10:04 2013 +0100
@@ -53,6 +53,8 @@
-- "level of parallel proof checking: 0, 1, 2"
option parallel_proofs_threshold : int = 100
-- "threshold for sub-proof parallelization"
+option parallel_proofs_reuse_timing : bool = true
+ -- "reuse timing information from old log file for parallel proof scheduling"
section "Detail of Proof Recording"
--- a/src/Pure/General/timing.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/General/timing.ML Thu Feb 21 15:10:04 2013 +0100
@@ -20,6 +20,7 @@
val start: unit -> start
val result: start -> timing
val timing: ('a -> 'b) -> 'a -> timing * 'b
+ val is_relevant_time: Time.time -> bool
val is_relevant: timing -> bool
val message: timing -> string
end
@@ -27,10 +28,13 @@
structure Timing: TIMING =
struct
-(* timer control *)
+(* type timing *)
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
+
+(* timer control *)
+
abstype start = Start of
Timer.real_timer * Time.time * Timer.cpu_timer *
{gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
@@ -70,10 +74,12 @@
val min_time = Time.fromMilliseconds 1;
+fun is_relevant_time time = Time.>= (time, min_time);
+
fun is_relevant {elapsed, cpu, gc} =
- Time.>= (elapsed, min_time) orelse
- Time.>= (cpu, min_time) orelse
- Time.>= (gc, min_time);
+ is_relevant_time elapsed orelse
+ is_relevant_time cpu orelse
+ is_relevant_time gc;
fun message {elapsed, cpu, gc} =
Time.toString elapsed ^ "s elapsed time, " ^
--- a/src/Pure/Isar/keyword.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/keyword.ML Thu Feb 21 15:10:04 2013 +0100
@@ -63,6 +63,7 @@
val is_theory_load: string -> bool
val is_theory: string -> bool
val is_proof: string -> bool
+ val is_proof_body: string -> bool
val is_theory_goal: string -> bool
val is_proof_goal: string -> bool
val is_schematic_goal: string -> bool
@@ -230,10 +231,13 @@
(* command categories *)
-fun command_category ks name =
- (case command_keyword name of
- NONE => false
- | SOME k => member (op = o pairself kind_of) ks k);
+fun command_category ks =
+ let val tab = Symtab.make_set (map kind_of ks) in
+ fn name =>
+ (case command_keyword name of
+ NONE => false
+ | SOME k => Symtab.defined tab (kind_of k))
+ end;
val is_diag = command_category [diag];
val is_control = command_category [control];
@@ -256,6 +260,10 @@
prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
prf_asm, prf_asm_goal, prf_script];
+val is_proof_body = command_category
+ [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
+ prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
val is_schematic_goal = command_category [thy_schematic_goal];
--- a/src/Pure/Isar/outer_syntax.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Thu Feb 21 15:10:04 2013 +0100
@@ -36,7 +36,7 @@
val isar: TextIO.instream -> bool -> isar
val span_cmts: Token.T list -> Token.T list
val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
- val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+ val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
(Toplevel.transition * Toplevel.transition list) list
end;
@@ -331,13 +331,16 @@
handle ERROR msg => (Toplevel.malformed proper_range msg, true)
end;
-fun read_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
let
val read = read_span outer_syntax o Thy_Syntax.span_content;
val (tr, proper_head) = read head |>> Toplevel.modify_init init;
- val proof_trs = map read proof |> filter #2 |> map #1;
+ val proof_trs =
+ (case opt_proof of
+ NONE => []
+ | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
in
- if proper_head andalso proper_proof andalso
+ if proper_head andalso
not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
--- a/src/Pure/Isar/proof.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/proof.ML Thu Feb 21 15:10:04 2013 +0100
@@ -114,6 +114,7 @@
val show_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
+ val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
@@ -1188,7 +1189,7 @@
andalso not (is_relevant state)
then
snd (proof2 (fn state' =>
- Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
+ Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
else proof1 meths state;
in
--- a/src/Pure/Isar/toplevel.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Feb 21 15:10:04 2013 +0100
@@ -89,6 +89,9 @@
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val status: transition -> Markup.T -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
+ val approximative_id: transition -> {file: string, offset: int, name: string} option
+ val get_timing: transition -> Time.time
+ val put_timing: Time.time -> transition -> transition
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
val proof_result: bool -> transition * transition list -> state ->
@@ -340,16 +343,17 @@
int_only: bool, (*interactive-only*)
print: bool, (*print result state*)
no_timing: bool, (*suppress timing*)
+ timing: Time.time, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
-fun make_transition (name, pos, int_only, print, no_timing, trans) =
- Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
- trans = trans};
+fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
+ Transition {name = name, pos = pos, int_only = int_only, print = print,
+ no_timing = no_timing, timing = timing, trans = trans};
-fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
- make_transition (f (name, pos, int_only, print, no_timing, trans));
+fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
+ make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
-val empty = make_transition ("", Position.none, false, false, false, []);
+val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
(* diagnostics *)
@@ -367,26 +371,26 @@
(* modify transitions *)
-fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
- (name, pos, int_only, print, no_timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
+ (name, pos, int_only, print, no_timing, timing, trans));
-fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
- (name, pos, int_only, print, no_timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
+ (name, pos, int_only, print, no_timing, timing, trans));
-fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
- (name, pos, int_only, print, no_timing, trans));
+fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
+ (name, pos, int_only, print, no_timing, timing, trans));
-val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
- (name, pos, int_only, print, true, trans));
+val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
+ (name, pos, int_only, print, true, timing, trans));
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
- (name, pos, int_only, print, no_timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
+ (name, pos, int_only, print, no_timing, timing, tr :: trans));
-val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
- (name, pos, int_only, print, no_timing, []));
+val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
+ (name, pos, int_only, print, no_timing, timing, []));
-fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
- (name, pos, int_only, print, no_timing, trans));
+fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
+ (name, pos, int_only, print, no_timing, timing, trans));
val print = set_print true;
@@ -587,6 +591,19 @@
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
+(* approximative identification within source file *)
+
+fun approximative_id tr =
+ let
+ val name = name_of tr;
+ val pos = pos_of tr;
+ in
+ (case (Position.file_of pos, Position.offset_of pos) of
+ (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name}
+ | _ => NONE)
+ end;
+
+
(* thread position *)
fun setmp_thread_position (Transition {pos, ...}) f x =
@@ -610,14 +627,31 @@
(* apply transitions *)
+fun get_timing (Transition {timing, ...}) = timing;
+fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
+ (name, pos, int_only, print, no_timing, timing, trans));
+
local
+fun timing_message tr t =
+ if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
+ then
+ (case approximative_id tr of
+ SOME id =>
+ (Output.protocol_message
+ (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
+ handle Fail _ => ())
+ | NONE => ())
+ else ();
+
fun app int (tr as Transition {trans, print, no_timing, ...}) =
setmp_thread_position tr (fn state =>
let
fun do_timing f x = (warning (command_msg "" tr); timeap f x);
fun do_profiling f x = profile (! profiling) f x;
+ val start = Timing.start ();
+
val (result, status) =
state |>
(apply_trans int trans
@@ -625,6 +659,8 @@
|> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
+
+ val _ = timing_message tr (Timing.result start);
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
in
@@ -672,7 +708,8 @@
fun proof_result immediate (tr, proof_trs) st =
let val st' = command tr st in
- if immediate orelse null proof_trs orelse not (can proof_of st')
+ if immediate orelse null proof_trs orelse not (can proof_of st') orelse
+ Proof.is_relevant (proof_of st')
then
let val (results, st'') = fold_map command_result proof_trs st'
in (Future.value ((tr, st') :: results), st'') end
@@ -681,9 +718,13 @@
val (body_trs, end_tr) = split_last proof_trs;
val finish = Context.Theory o Proof_Context.theory_of;
+ val timing_estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
+ val timing_order = Real.floor (Real.max (Math.log10 (Time.toReal timing_estimate), ~3.0));
+ val pri = Int.min (timing_order - 3, ~1);
+
val future_proof = Proof.global_future_proof
(fn prf =>
- Goal.fork_name "Toplevel.future_proof"
+ Goal.fork_name "Toplevel.future_proof" pri
(fn () =>
let val (result, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
--- a/src/Pure/PIDE/markup.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Feb 21 15:10:04 2013 +0100
@@ -92,7 +92,14 @@
val elapsedN: string
val cpuN: string
val gcN: string
+ val timing_propertiesN: string list
val timing_properties: Timing.timing -> Properties.T
+ val parse_timing_properties: Properties.T -> Timing.timing
+ val command_timingN: string
+ val command_timing_properties:
+ {file: string, offset: int, name: string} -> Time.time -> Properties.T
+ val parse_command_timing_properties:
+ Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
val timingN: string val timing: Timing.timing -> T
val subgoalsN: string
val proof_stateN: string val proof_state: int -> T
@@ -135,6 +142,7 @@
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
val task_statistics: Properties.entry
+ val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
@@ -332,11 +340,41 @@
val cpuN = "cpu";
val gcN = "gc";
+val timing_propertiesN = [elapsedN, cpuN, gcN];
+
fun timing_properties {elapsed, cpu, gc} =
[(elapsedN, Time.toString elapsed),
(cpuN, Time.toString cpu),
(gcN, Time.toString gc)];
+fun get_time props name =
+ (case AList.lookup (op =) props name of
+ NONE => Time.zeroTime
+ | SOME s => seconds (the_default 0.0 (Real.fromString s)));
+
+fun parse_timing_properties props =
+ {elapsed = get_time props elapsedN,
+ cpu = get_time props cpuN,
+ gc = get_time props gcN};
+
+
+(* command timing *)
+
+val command_timingN = "command_timing";
+
+fun command_timing_properties {file, offset, name} elapsed =
+ [(fileN, file), (offsetN, print_int offset),
+ (nameN, name), (elapsedN, Time.toString elapsed)];
+
+fun parse_command_timing_properties props =
+ (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
+ (SOME file, SOME offset, SOME name) =>
+ SOME ({file = file, offset = parse_int offset, name = name}, get_time props elapsedN)
+ | _ => NONE);
+
+
+(* session timing *)
+
val timingN = "timing";
fun timing t = (timingN, timing_properties t);
@@ -415,6 +453,8 @@
val task_statistics = (functionN, "task_statistics");
+val command_timing = (functionN, "command_timing");
+
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
--- a/src/Pure/PIDE/xml.scala Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/PIDE/xml.scala Thu Feb 21 15:10:04 2013 +0100
@@ -188,6 +188,7 @@
// main methods
def cache_string(x: String): String = synchronized { _cache_string(x) }
+ def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
--- a/src/Pure/Pure.thy Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Pure.thy Thu Feb 21 15:10:04 2013 +0100
@@ -41,8 +41,8 @@
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" :: thy_decl
- and "sublocale" "interpretation" :: thy_schematic_goal
- and "interpret" :: prf_goal % "proof" (* FIXME schematic? *)
+ and "sublocale" "interpretation" :: thy_goal
+ and "interpret" :: prf_goal % "proof"
and "class" :: thy_decl
and "subclass" :: thy_goal
and "instantiation" :: thy_decl
--- a/src/Pure/Thy/thy_info.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Feb 21 15:10:04 2013 +0100
@@ -17,7 +17,8 @@
val loaded_files: string -> Path.T list
val remove_thy: string -> unit
val kill_thy: string -> unit
- val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
+ val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
+ (string * Position.T) list -> unit
val use_thys: (string * Position.T) list -> unit
val use_thy: string * Position.T -> unit
val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
@@ -221,7 +222,7 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
+fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents =
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -234,7 +235,7 @@
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
val (theory, present) =
- Thy_Load.load_thy update_time dir header (Path.position thy_path) text
+ Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
in (theory, present, commit) end;
@@ -259,9 +260,9 @@
in
-fun require_thys initiators dir strs tasks =
- fold_map (require_thy initiators dir) strs tasks |>> forall I
-and require_thy initiators dir (str, require_pos) tasks =
+fun require_thys last_timing initiators dir strs tasks =
+ fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
+and require_thy last_timing initiators dir (str, require_pos) tasks =
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
@@ -280,7 +281,7 @@
val parents = map (base_name o #1) imports;
val (parents_current, tasks') =
- require_thys (name :: initiators)
+ require_thys last_timing (name :: initiators)
(Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
val all_current = current andalso parents_current;
@@ -293,7 +294,8 @@
let
val update_time = serial ();
val load =
- load_thy initiators update_time dep text (name, theory_pos) uses keywords;
+ load_thy last_timing initiators update_time dep
+ text (name, theory_pos) uses keywords;
in Task (parents, load) end);
val tasks'' = new_entry name parents task tasks';
@@ -305,10 +307,10 @@
(* use_thy *)
-fun use_thys_wrt dir arg =
- schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
+fun use_theories {last_timing, master_dir} imports =
+ schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
-val use_thys = use_thys_wrt Path.current;
+val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
val use_thy = use_thys o single;
@@ -318,7 +320,7 @@
let
val {name = (name, _), imports, ...} = header;
val _ = kill_thy name;
- val _ = use_thys_wrt master_dir imports;
+ val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
val _ = Thy_Header.define_keywords header;
val parents = map (get_theory o base_name o fst) imports;
in Thy_Load.begin_theory master_dir header parents end;
--- a/src/Pure/Thy/thy_load.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Thu Feb 21 15:10:04 2013 +0100
@@ -22,8 +22,8 @@
val use_ml: Path.T -> unit
val exec_ml: Path.T -> generic_theory -> generic_theory
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
- val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
- theory list -> theory * unit future
+ val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
+ Position.T -> string -> theory list -> theory * unit future
val set_master_path: Path.T -> unit
val get_master_path: unit -> Path.T
end;
@@ -214,10 +214,13 @@
|> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
|> Theory.checkpoint;
-fun excursion init elements =
+fun excursion last_timing init elements =
let
val immediate = not (Goal.future_enabled ());
+ fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
+ fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
+
fun proof_result (tr, trs) (st, _) =
let
val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
@@ -225,7 +228,7 @@
in (result, (st', pos')) end;
fun element_result elem x =
- fold_map proof_result
+ fold_map (proof_result o put_timings)
(Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
val (results, (end_state, end_pos)) =
@@ -234,7 +237,7 @@
val thy = Toplevel.end_theory end_pos end_state;
in (flat results, thy) end;
-fun load_thy update_time master_dir header text_pos text parents =
+fun load_thy last_timing update_time master_dir header text_pos text parents =
let
val time = ! Toplevel.timing;
@@ -255,7 +258,7 @@
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
+ val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
val present =
--- a/src/Pure/Thy/thy_syntax.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Thu Feb 21 15:10:04 2013 +0100
@@ -15,8 +15,10 @@
val span_content: span -> Token.T list
val present_span: span -> Output.output
val parse_spans: Token.T list -> span list
- type element = {head: span, proof: span list, proper_proof: bool}
- val parse_elements: span list -> element list
+ datatype 'a element = Element of 'a * ('a element list * 'a) option
+ val map_element: ('a -> 'b) -> 'a element -> 'b element
+ val flat_element: 'a element -> 'a list
+ val parse_elements: span list -> span element list
end;
structure Thy_Syntax: THY_SYNTAX =
@@ -134,10 +136,17 @@
(** specification elements: commands with optional proof **)
-type element = {head: span, proof: span list, proper_proof: bool};
+datatype 'a element = Element of 'a * ('a element list * 'a) option;
+
+fun element (a, b) = Element (a, SOME b);
+fun atom a = Element (a, NONE);
-fun make_element head proof proper_proof =
- {head = head, proof = proof, proper_proof = proper_proof};
+fun map_element f (Element (a, NONE)) = Element (f a, NONE)
+ | map_element f (Element (a, SOME (elems, b))) =
+ Element (f a, SOME ((map o map_element) f elems, f b));
+
+fun flat_element (Element (a, NONE)) = [a]
+ | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
(* scanning spans *)
@@ -159,24 +168,21 @@
fun command_with pred =
Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
-val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
- if d <= 0 then Scan.fail
- else
- command_with Keyword.is_qed_global >> pair ~1 ||
- command_with Keyword.is_proof_goal >> pair (d + 1) ||
- (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
- Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+val proof_atom =
+ Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
-val element =
- command_with Keyword.is_theory_goal -- proof
- >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
- Scan.one not_eof >> (fn a => make_element a [] true);
+fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
+and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
+
+val other_element =
+ command_with Keyword.is_theory_goal -- proof_rest >> element ||
+ Scan.one not_eof >> atom;
in
val parse_elements =
Source.of_list #>
- Source.source stopper (Scan.bulk element) NONE #>
+ Source.source stopper (Scan.bulk other_element) NONE #>
Source.exhaust;
end;
--- a/src/Pure/Tools/build.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Tools/build.ML Thu Feb 21 15:10:04 2013 +0100
@@ -16,30 +16,23 @@
local
-fun ML_statistics (function :: stats) "" =
- if function = Markup.ML_statistics then SOME stats
- else NONE
- | ML_statistics _ _ = NONE;
+(* FIXME avoid hardwired stuff!? *)
+val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
-fun task_statistics (function :: stats) "" =
- if function = Markup.task_statistics then SOME stats
- else NONE
- | task_statistics _ _ = NONE;
-
-val print_properties = YXML.string_of_body o XML.Encode.properties;
+fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
in
fun protocol_message props output =
- (case ML_statistics props output of
- SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
- | NONE =>
- (case task_statistics props output of
- SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
- | NONE =>
- (case Markup.dest_loading_theory props of
- SOME name => writeln ("\floading_theory = " ^ name)
- | NONE => raise Fail "Undefined Output.protocol_message")));
+ (case props of
+ function :: args =>
+ if member (op =) protocol_echo function then
+ writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+ else
+ (case Markup.dest_loading_theory props of
+ SOME name => writeln ("\floading_theory = " ^ name)
+ | NONE => protocol_undef ())
+ | [] => protocol_undef ());
end;
@@ -51,8 +44,8 @@
fun no_document options =
(case Options.string options "document" of "" => true | "false" => true | _ => false);
-fun use_thys options =
- Thy_Info.use_thys
+fun use_theories last_timing options =
+ Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
|> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
|> Unsynchronized.setmp print_mode
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())
@@ -78,25 +71,49 @@
|> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
|> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
-fun use_theories (options, thys) =
+fun use_theories_condition last_timing (options, thys) =
let val condition = space_explode "," (Options.string options "condition") in
(case filter_out (can getenv_strict) condition of
- [] => use_thys options (map (rpair Position.none) thys)
+ [] => use_theories last_timing options (map (rpair Position.none) thys)
| conds =>
Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
" (undefined " ^ commas conds ^ ")\n"))
end;
+
+(* command timings *)
+
+type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *)
+
+val empty_timings: timings = Symtab.empty;
+
+fun update_timings props =
+ (case Markup.parse_command_timing_properties props of
+ SOME ({file, offset, name}, time) =>
+ Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
+ | NONE => I);
+
+fun lookup_timings timings tr =
+ (case Toplevel.approximative_id tr of
+ SOME {file, offset, name} =>
+ (case Symtab.lookup timings file of
+ SOME offsets =>
+ (case Inttab.lookup offsets offset of
+ SOME (name', time) => if name = name' then time else Time.zeroTime
+ | NONE => Time.zeroTime)
+ | NONE => Time.zeroTime)
+ | NONE => Time.zeroTime);
+
in
fun build args_file = Command_Line.tool (fn () =>
let
- val (do_output, (options, (verbose, (browser_info, (parent_name,
- (name, theories)))))) =
+ val (command_timings, (do_output, (options, (verbose, (browser_info,
+ (parent_name, (name, theories))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
- pair bool (pair Options.decode (pair bool (pair string (pair string
- (pair string ((list (pair Options.decode (list string)))))))))
+ pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
+ (pair string (pair string ((list (pair Options.decode (list string))))))))))
end;
val document_variants =
@@ -122,9 +139,11 @@
(false, "") ""
verbose;
+ val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+
val res1 =
theories |>
- (List.app use_theories
+ (List.app (use_theories_condition last_timing)
|> Session.with_timing name verbose
|> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
--- a/src/Pure/Tools/build.scala Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Tools/build.scala Thu Feb 21 15:10:04 2013 +0100
@@ -288,41 +288,71 @@
object Queue
{
- def apply(tree: Session_Tree): Queue =
+ def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
{
val graph = tree.graph
+ val sessions = graph.keys.toList
+
+ val timings = sessions.map((name: String) =>
+ if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
+ else (name, (Nil, 0.0)))
+ val command_timings =
+ Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
+ val session_timing =
+ Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
def outdegree(name: String): Int = graph.imm_succs(name).size
def timeout(name: String): Double = tree(name).options.real("timeout")
object Ordering extends scala.math.Ordering[String]
{
+ def compare_timing(name1: String, name2: String): Int =
+ {
+ val t1 = session_timing(name1)
+ val t2 = session_timing(name2)
+ if (t1 == 0.0 || t2 == 0.0) 0
+ else t1 compare t2
+ }
+
def compare(name1: String, name2: String): Int =
outdegree(name2) compare outdegree(name1) match {
case 0 =>
- timeout(name2) compare timeout(name1) match {
- case 0 => name1 compare name2
+ compare_timing(name2, name1) match {
+ case 0 =>
+ timeout(name2) compare timeout(name1) match {
+ case 0 => name1 compare name2
+ case ord => ord
+ }
case ord => ord
}
case ord => ord
}
}
- new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
+ new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
}
}
- final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
+ final class Queue private(
+ graph: Graph[String, Session_Info],
+ order: SortedSet[String],
+ val command_timings: String => List[Properties.T])
{
def is_inner(name: String): Boolean = !graph.is_maximal(name)
def is_empty: Boolean = graph.is_empty
- def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
+ def - (name: String): Queue =
+ new Queue(graph.del_node(name),
+ order - name, // FIXME scala-2.10.0 TreeSet problem!?
+ command_timings)
def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
{
- val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
+ val it = order.iterator.dropWhile(name =>
+ skip(name)
+ || !graph.defined(name) // FIXME scala-2.10.0 TreeSet problem!?
+ || !graph.is_minimal(name))
if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
else None
}
@@ -419,7 +449,7 @@
private class Job(progress: Build.Progress,
name: String, val info: Session_Info, output: Path, do_output: Boolean,
- verbose: Boolean, browser_info: Path)
+ verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
{
// global browser info dir
if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
@@ -443,10 +473,10 @@
else
{
import XML.Encode._
- pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
- pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
- (do_output, (info.options, (verbose, (browser_info, (parent,
- (name, info.theories)))))))
+ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
+ pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+ (command_timings, (do_output, (info.options, (verbose, (browser_info,
+ (parent, (name, info.theories))))))))
}))
private val env =
@@ -546,17 +576,26 @@
sealed case class Log_Info(
- name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
+ name: String,
+ stats: List[Properties.T],
+ tasks: List[Properties.T],
+ command_timings: List[Properties.T],
+ session_timing: Properties.T)
- def parse_log(text: String): Log_Info =
+ def parse_log(full_stats: Boolean, text: String): Log_Info =
{
val lines = split_lines(text)
+ val xml_cache = new XML.Cache()
+ def parse_lines(prfx: String): List[Properties.T] =
+ Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
+
val name =
lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
- val stats = Props.parse_lines("\fML_statistics = ", lines)
- val tasks = Props.parse_lines("\ftask_statistics = ", lines)
- val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
- Log_Info(name, stats, tasks, timing)
+ val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
+ val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
+ val command_timings = parse_lines("\fcommand_timing = ")
+ val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
+ Log_Info(name, stats, tasks, command_timings, session_timing)
}
@@ -612,16 +651,20 @@
verbose: Boolean = false,
sessions: List[String] = Nil): Int =
{
+ /* session tree and dependencies */
+
val full_tree = find_sessions(options, more_dirs)
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions, session_groups, sessions)
val deps = dependencies(progress, true, verbose, list_files, selected_tree)
- val queue = Queue(selected_tree)
def make_stamp(name: String): String =
sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
+
+ /* persistent information */
+
val (input_dirs, output_dir, browser_info) =
if (system_mode) {
val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
@@ -633,6 +676,40 @@
Path.explode("$ISABELLE_BROWSER_INFO"))
}
+ def find_log(name: String): Option[(Path, Path)] =
+ input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
+
+
+ /* queue with scheduling information */
+
+ def load_timings(name: String): (List[Properties.T], Double) =
+ {
+ val (path, text) =
+ find_log(name + ".gz") match {
+ case Some((_, path)) => (path, File.read_gzip(path))
+ case None =>
+ find_log(name) match {
+ case Some((_, path)) => (path, File.read(path))
+ case None => (Path.current, "")
+ }
+ }
+ try {
+ val info = parse_log(false, text)
+ val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
+ (info.command_timings, session_timing)
+ }
+ catch {
+ case ERROR(msg) =>
+ java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
+ (Nil, 0.0)
+ }
+ }
+
+ val queue = Queue(selected_tree, load_timings)
+
+
+ /* main build process */
+
// prepare log dir
Isabelle_System.mkdirs(output_dir + LOG)
@@ -718,9 +795,9 @@
val (current, heap) =
{
- input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
- case Some(dir) =>
- read_stamps(dir + log_gz(name)) match {
+ find_log(name + ".gz") match {
+ case Some((dir, path)) =>
+ read_stamps(path) match {
case Some((s, h1, h2)) =>
val heap = heap_stamp(Some(dir + Path.basic(name)))
(s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
@@ -740,7 +817,9 @@
}
else if (parent_result.rc == 0) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
- val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
+ val job =
+ new Job(progress, name, info, output, do_output, verbose, browser_info,
+ queue.command_timings(name))
loop(pending, running + (name -> (parent_result.heap, job)), results)
}
else {
@@ -754,6 +833,9 @@
}
}
+
+ /* build results */
+
val results =
if (deps.is_empty) {
progress.echo("### Nothing to build")
--- a/src/Pure/goal.ML Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/goal.ML Thu Feb 21 15:10:04 2013 +0100
@@ -24,8 +24,8 @@
val check_finished: Proof.context -> thm -> thm
val finish: Proof.context -> thm -> thm
val norm_result: thm -> thm
- val fork_name: string -> (unit -> 'a) -> 'a future
- val fork: (unit -> 'a) -> 'a future
+ val fork_name: string -> int -> (unit -> 'a) -> 'a future
+ val fork: int -> (unit -> 'a) -> 'a future
val peek_futures: serial -> unit future list
val reset_futures: unit -> Future.group list
val future_enabled_level: int -> bool
@@ -134,7 +134,7 @@
in
-fun fork_name name e =
+fun fork_name name pri e =
uninterruptible (fn _ => fn () =>
let
val pos = Position.thread_data ();
@@ -143,7 +143,7 @@
val future =
(singleton o Future.forks)
- {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+ {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
(fn () =>
let
val task = the (Future.worker_task ());
@@ -167,7 +167,7 @@
val _ = register_forked id future;
in future end) ();
-fun fork e = fork_name "Goal.fork" e;
+fun fork pri e = fork_name "Goal.fork" pri e;
fun forked_count () = #1 (Synchronized.value forked_proofs);
@@ -285,7 +285,7 @@
val res =
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
then result ()
- else future_result ctxt' (fork result) (Thm.term_of stmt);
+ else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
in
Conjunction.elim_balanced (length props) res
|> map (Assumption.export false ctxt' ctxt)