1.1 --- a/etc/options Thu Feb 21 12:22:26 2013 +0100
1.2 +++ b/etc/options Thu Feb 21 15:10:04 2013 +0100
1.3 @@ -53,6 +53,8 @@
1.4 -- "level of parallel proof checking: 0, 1, 2"
1.5 option parallel_proofs_threshold : int = 100
1.6 -- "threshold for sub-proof parallelization"
1.7 +option parallel_proofs_reuse_timing : bool = true
1.8 + -- "reuse timing information from old log file for parallel proof scheduling"
1.9
1.10
1.11 section "Detail of Proof Recording"
2.1 --- a/src/Pure/General/timing.ML Thu Feb 21 12:22:26 2013 +0100
2.2 +++ b/src/Pure/General/timing.ML Thu Feb 21 15:10:04 2013 +0100
2.3 @@ -20,6 +20,7 @@
2.4 val start: unit -> start
2.5 val result: start -> timing
2.6 val timing: ('a -> 'b) -> 'a -> timing * 'b
2.7 + val is_relevant_time: Time.time -> bool
2.8 val is_relevant: timing -> bool
2.9 val message: timing -> string
2.10 end
2.11 @@ -27,10 +28,13 @@
2.12 structure Timing: TIMING =
2.13 struct
2.14
2.15 -(* timer control *)
2.16 +(* type timing *)
2.17
2.18 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
2.19
2.20 +
2.21 +(* timer control *)
2.22 +
2.23 abstype start = Start of
2.24 Timer.real_timer * Time.time * Timer.cpu_timer *
2.25 {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
2.26 @@ -70,10 +74,12 @@
2.27
2.28 val min_time = Time.fromMilliseconds 1;
2.29
2.30 +fun is_relevant_time time = Time.>= (time, min_time);
2.31 +
2.32 fun is_relevant {elapsed, cpu, gc} =
2.33 - Time.>= (elapsed, min_time) orelse
2.34 - Time.>= (cpu, min_time) orelse
2.35 - Time.>= (gc, min_time);
2.36 + is_relevant_time elapsed orelse
2.37 + is_relevant_time cpu orelse
2.38 + is_relevant_time gc;
2.39
2.40 fun message {elapsed, cpu, gc} =
2.41 Time.toString elapsed ^ "s elapsed time, " ^
3.1 --- a/src/Pure/Isar/keyword.ML Thu Feb 21 12:22:26 2013 +0100
3.2 +++ b/src/Pure/Isar/keyword.ML Thu Feb 21 15:10:04 2013 +0100
3.3 @@ -63,6 +63,7 @@
3.4 val is_theory_load: string -> bool
3.5 val is_theory: string -> bool
3.6 val is_proof: string -> bool
3.7 + val is_proof_body: string -> bool
3.8 val is_theory_goal: string -> bool
3.9 val is_proof_goal: string -> bool
3.10 val is_schematic_goal: string -> bool
3.11 @@ -230,10 +231,13 @@
3.12
3.13 (* command categories *)
3.14
3.15 -fun command_category ks name =
3.16 - (case command_keyword name of
3.17 - NONE => false
3.18 - | SOME k => member (op = o pairself kind_of) ks k);
3.19 +fun command_category ks =
3.20 + let val tab = Symtab.make_set (map kind_of ks) in
3.21 + fn name =>
3.22 + (case command_keyword name of
3.23 + NONE => false
3.24 + | SOME k => Symtab.defined tab (kind_of k))
3.25 + end;
3.26
3.27 val is_diag = command_category [diag];
3.28 val is_control = command_category [control];
3.29 @@ -256,6 +260,10 @@
3.30 prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
3.31 prf_asm, prf_asm_goal, prf_script];
3.32
3.33 +val is_proof_body = command_category
3.34 + [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
3.35 + prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
3.36 +
3.37 val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
3.38 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
3.39 val is_schematic_goal = command_category [thy_schematic_goal];
4.1 --- a/src/Pure/Isar/outer_syntax.ML Thu Feb 21 12:22:26 2013 +0100
4.2 +++ b/src/Pure/Isar/outer_syntax.ML Thu Feb 21 15:10:04 2013 +0100
4.3 @@ -36,7 +36,7 @@
4.4 val isar: TextIO.instream -> bool -> isar
4.5 val span_cmts: Token.T list -> Token.T list
4.6 val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
4.7 - val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
4.8 + val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
4.9 (Toplevel.transition * Toplevel.transition list) list
4.10 end;
4.11
4.12 @@ -331,13 +331,16 @@
4.13 handle ERROR msg => (Toplevel.malformed proper_range msg, true)
4.14 end;
4.15
4.16 -fun read_element outer_syntax init {head, proof, proper_proof} =
4.17 +fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
4.18 let
4.19 val read = read_span outer_syntax o Thy_Syntax.span_content;
4.20 val (tr, proper_head) = read head |>> Toplevel.modify_init init;
4.21 - val proof_trs = map read proof |> filter #2 |> map #1;
4.22 + val proof_trs =
4.23 + (case opt_proof of
4.24 + NONE => []
4.25 + | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
4.26 in
4.27 - if proper_head andalso proper_proof andalso
4.28 + if proper_head andalso
4.29 not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
4.30 else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
4.31 end;
5.1 --- a/src/Pure/Isar/proof.ML Thu Feb 21 12:22:26 2013 +0100
5.2 +++ b/src/Pure/Isar/proof.ML Thu Feb 21 15:10:04 2013 +0100
5.3 @@ -114,6 +114,7 @@
5.4 val show_cmd: Method.text option -> (thm list list -> state -> state) ->
5.5 (Attrib.binding * (string * string list) list) list -> bool -> state -> state
5.6 val schematic_goal: state -> bool
5.7 + val is_relevant: state -> bool
5.8 val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
5.9 val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
5.10 val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
5.11 @@ -1188,7 +1189,7 @@
5.12 andalso not (is_relevant state)
5.13 then
5.14 snd (proof2 (fn state' =>
5.15 - Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
5.16 + Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
5.17 else proof1 meths state;
5.18
5.19 in
6.1 --- a/src/Pure/Isar/toplevel.ML Thu Feb 21 12:22:26 2013 +0100
6.2 +++ b/src/Pure/Isar/toplevel.ML Thu Feb 21 15:10:04 2013 +0100
6.3 @@ -89,6 +89,9 @@
6.4 val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
6.5 val status: transition -> Markup.T -> unit
6.6 val add_hook: (transition -> state -> state -> unit) -> unit
6.7 + val approximative_id: transition -> {file: string, offset: int, name: string} option
6.8 + val get_timing: transition -> Time.time
6.9 + val put_timing: Time.time -> transition -> transition
6.10 val transition: bool -> transition -> state -> (state * (exn * string) option) option
6.11 val command: transition -> state -> state
6.12 val proof_result: bool -> transition * transition list -> state ->
6.13 @@ -340,16 +343,17 @@
6.14 int_only: bool, (*interactive-only*)
6.15 print: bool, (*print result state*)
6.16 no_timing: bool, (*suppress timing*)
6.17 + timing: Time.time, (*prescient timing information*)
6.18 trans: trans list}; (*primitive transitions (union)*)
6.19
6.20 -fun make_transition (name, pos, int_only, print, no_timing, trans) =
6.21 - Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
6.22 - trans = trans};
6.23 +fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
6.24 + Transition {name = name, pos = pos, int_only = int_only, print = print,
6.25 + no_timing = no_timing, timing = timing, trans = trans};
6.26
6.27 -fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
6.28 - make_transition (f (name, pos, int_only, print, no_timing, trans));
6.29 +fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
6.30 + make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
6.31
6.32 -val empty = make_transition ("", Position.none, false, false, false, []);
6.33 +val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
6.34
6.35
6.36 (* diagnostics *)
6.37 @@ -367,26 +371,26 @@
6.38
6.39 (* modify transitions *)
6.40
6.41 -fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
6.42 - (name, pos, int_only, print, no_timing, trans));
6.43 +fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
6.44 + (name, pos, int_only, print, no_timing, timing, trans));
6.45
6.46 -fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
6.47 - (name, pos, int_only, print, no_timing, trans));
6.48 +fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
6.49 + (name, pos, int_only, print, no_timing, timing, trans));
6.50
6.51 -fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
6.52 - (name, pos, int_only, print, no_timing, trans));
6.53 +fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
6.54 + (name, pos, int_only, print, no_timing, timing, trans));
6.55
6.56 -val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
6.57 - (name, pos, int_only, print, true, trans));
6.58 +val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
6.59 + (name, pos, int_only, print, true, timing, trans));
6.60
6.61 -fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
6.62 - (name, pos, int_only, print, no_timing, tr :: trans));
6.63 +fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
6.64 + (name, pos, int_only, print, no_timing, timing, tr :: trans));
6.65
6.66 -val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
6.67 - (name, pos, int_only, print, no_timing, []));
6.68 +val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
6.69 + (name, pos, int_only, print, no_timing, timing, []));
6.70
6.71 -fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
6.72 - (name, pos, int_only, print, no_timing, trans));
6.73 +fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
6.74 + (name, pos, int_only, print, no_timing, timing, trans));
6.75
6.76 val print = set_print true;
6.77
6.78 @@ -587,6 +591,19 @@
6.79 fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
6.80
6.81
6.82 +(* approximative identification within source file *)
6.83 +
6.84 +fun approximative_id tr =
6.85 + let
6.86 + val name = name_of tr;
6.87 + val pos = pos_of tr;
6.88 + in
6.89 + (case (Position.file_of pos, Position.offset_of pos) of
6.90 + (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name}
6.91 + | _ => NONE)
6.92 + end;
6.93 +
6.94 +
6.95 (* thread position *)
6.96
6.97 fun setmp_thread_position (Transition {pos, ...}) f x =
6.98 @@ -610,14 +627,31 @@
6.99
6.100 (* apply transitions *)
6.101
6.102 +fun get_timing (Transition {timing, ...}) = timing;
6.103 +fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
6.104 + (name, pos, int_only, print, no_timing, timing, trans));
6.105 +
6.106 local
6.107
6.108 +fun timing_message tr t =
6.109 + if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
6.110 + then
6.111 + (case approximative_id tr of
6.112 + SOME id =>
6.113 + (Output.protocol_message
6.114 + (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
6.115 + handle Fail _ => ())
6.116 + | NONE => ())
6.117 + else ();
6.118 +
6.119 fun app int (tr as Transition {trans, print, no_timing, ...}) =
6.120 setmp_thread_position tr (fn state =>
6.121 let
6.122 fun do_timing f x = (warning (command_msg "" tr); timeap f x);
6.123 fun do_profiling f x = profile (! profiling) f x;
6.124
6.125 + val start = Timing.start ();
6.126 +
6.127 val (result, status) =
6.128 state |>
6.129 (apply_trans int trans
6.130 @@ -625,6 +659,8 @@
6.131 |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
6.132
6.133 val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
6.134 +
6.135 + val _ = timing_message tr (Timing.result start);
6.136 in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
6.137
6.138 in
6.139 @@ -672,7 +708,8 @@
6.140
6.141 fun proof_result immediate (tr, proof_trs) st =
6.142 let val st' = command tr st in
6.143 - if immediate orelse null proof_trs orelse not (can proof_of st')
6.144 + if immediate orelse null proof_trs orelse not (can proof_of st') orelse
6.145 + Proof.is_relevant (proof_of st')
6.146 then
6.147 let val (results, st'') = fold_map command_result proof_trs st'
6.148 in (Future.value ((tr, st') :: results), st'') end
6.149 @@ -681,9 +718,13 @@
6.150 val (body_trs, end_tr) = split_last proof_trs;
6.151 val finish = Context.Theory o Proof_Context.theory_of;
6.152
6.153 + val timing_estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
6.154 + val timing_order = Real.floor (Real.max (Math.log10 (Time.toReal timing_estimate), ~3.0));
6.155 + val pri = Int.min (timing_order - 3, ~1);
6.156 +
6.157 val future_proof = Proof.global_future_proof
6.158 (fn prf =>
6.159 - Goal.fork_name "Toplevel.future_proof"
6.160 + Goal.fork_name "Toplevel.future_proof" pri
6.161 (fn () =>
6.162 let val (result, result_state) =
6.163 (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
7.1 --- a/src/Pure/PIDE/markup.ML Thu Feb 21 12:22:26 2013 +0100
7.2 +++ b/src/Pure/PIDE/markup.ML Thu Feb 21 15:10:04 2013 +0100
7.3 @@ -92,7 +92,14 @@
7.4 val elapsedN: string
7.5 val cpuN: string
7.6 val gcN: string
7.7 + val timing_propertiesN: string list
7.8 val timing_properties: Timing.timing -> Properties.T
7.9 + val parse_timing_properties: Properties.T -> Timing.timing
7.10 + val command_timingN: string
7.11 + val command_timing_properties:
7.12 + {file: string, offset: int, name: string} -> Time.time -> Properties.T
7.13 + val parse_command_timing_properties:
7.14 + Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
7.15 val timingN: string val timing: Timing.timing -> T
7.16 val subgoalsN: string
7.17 val proof_stateN: string val proof_state: int -> T
7.18 @@ -135,6 +142,7 @@
7.19 val cancel_scala: string -> Properties.T
7.20 val ML_statistics: Properties.entry
7.21 val task_statistics: Properties.entry
7.22 + val command_timing: Properties.entry
7.23 val loading_theory: string -> Properties.T
7.24 val dest_loading_theory: Properties.T -> string option
7.25 val no_output: Output.output * Output.output
7.26 @@ -332,11 +340,41 @@
7.27 val cpuN = "cpu";
7.28 val gcN = "gc";
7.29
7.30 +val timing_propertiesN = [elapsedN, cpuN, gcN];
7.31 +
7.32 fun timing_properties {elapsed, cpu, gc} =
7.33 [(elapsedN, Time.toString elapsed),
7.34 (cpuN, Time.toString cpu),
7.35 (gcN, Time.toString gc)];
7.36
7.37 +fun get_time props name =
7.38 + (case AList.lookup (op =) props name of
7.39 + NONE => Time.zeroTime
7.40 + | SOME s => seconds (the_default 0.0 (Real.fromString s)));
7.41 +
7.42 +fun parse_timing_properties props =
7.43 + {elapsed = get_time props elapsedN,
7.44 + cpu = get_time props cpuN,
7.45 + gc = get_time props gcN};
7.46 +
7.47 +
7.48 +(* command timing *)
7.49 +
7.50 +val command_timingN = "command_timing";
7.51 +
7.52 +fun command_timing_properties {file, offset, name} elapsed =
7.53 + [(fileN, file), (offsetN, print_int offset),
7.54 + (nameN, name), (elapsedN, Time.toString elapsed)];
7.55 +
7.56 +fun parse_command_timing_properties props =
7.57 + (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
7.58 + (SOME file, SOME offset, SOME name) =>
7.59 + SOME ({file = file, offset = parse_int offset, name = name}, get_time props elapsedN)
7.60 + | _ => NONE);
7.61 +
7.62 +
7.63 +(* session timing *)
7.64 +
7.65 val timingN = "timing";
7.66 fun timing t = (timingN, timing_properties t);
7.67
7.68 @@ -415,6 +453,8 @@
7.69
7.70 val task_statistics = (functionN, "task_statistics");
7.71
7.72 +val command_timing = (functionN, "command_timing");
7.73 +
7.74 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
7.75
7.76 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
8.1 --- a/src/Pure/PIDE/xml.scala Thu Feb 21 12:22:26 2013 +0100
8.2 +++ b/src/Pure/PIDE/xml.scala Thu Feb 21 15:10:04 2013 +0100
8.3 @@ -188,6 +188,7 @@
8.4
8.5 // main methods
8.6 def cache_string(x: String): String = synchronized { _cache_string(x) }
8.7 + def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
8.8 def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
8.9 def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
8.10 def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
9.1 --- a/src/Pure/Pure.thy Thu Feb 21 12:22:26 2013 +0100
9.2 +++ b/src/Pure/Pure.thy Thu Feb 21 15:10:04 2013 +0100
9.3 @@ -41,8 +41,8 @@
9.4 and "include" "including" :: prf_decl
9.5 and "print_bundles" :: diag
9.6 and "context" "locale" :: thy_decl
9.7 - and "sublocale" "interpretation" :: thy_schematic_goal
9.8 - and "interpret" :: prf_goal % "proof" (* FIXME schematic? *)
9.9 + and "sublocale" "interpretation" :: thy_goal
9.10 + and "interpret" :: prf_goal % "proof"
9.11 and "class" :: thy_decl
9.12 and "subclass" :: thy_goal
9.13 and "instantiation" :: thy_decl
10.1 --- a/src/Pure/Thy/thy_info.ML Thu Feb 21 12:22:26 2013 +0100
10.2 +++ b/src/Pure/Thy/thy_info.ML Thu Feb 21 15:10:04 2013 +0100
10.3 @@ -17,7 +17,8 @@
10.4 val loaded_files: string -> Path.T list
10.5 val remove_thy: string -> unit
10.6 val kill_thy: string -> unit
10.7 - val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
10.8 + val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
10.9 + (string * Position.T) list -> unit
10.10 val use_thys: (string * Position.T) list -> unit
10.11 val use_thy: string * Position.T -> unit
10.12 val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
10.13 @@ -221,7 +222,7 @@
10.14 fun required_by _ [] = ""
10.15 | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
10.16
10.17 -fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
10.18 +fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents =
10.19 let
10.20 val _ = kill_thy name;
10.21 val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
10.22 @@ -234,7 +235,7 @@
10.23 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
10.24
10.25 val (theory, present) =
10.26 - Thy_Load.load_thy update_time dir header (Path.position thy_path) text
10.27 + Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
10.28 (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
10.29 fun commit () = update_thy deps theory;
10.30 in (theory, present, commit) end;
10.31 @@ -259,9 +260,9 @@
10.32
10.33 in
10.34
10.35 -fun require_thys initiators dir strs tasks =
10.36 - fold_map (require_thy initiators dir) strs tasks |>> forall I
10.37 -and require_thy initiators dir (str, require_pos) tasks =
10.38 +fun require_thys last_timing initiators dir strs tasks =
10.39 + fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
10.40 +and require_thy last_timing initiators dir (str, require_pos) tasks =
10.41 let
10.42 val path = Path.expand (Path.explode str);
10.43 val name = Path.implode (Path.base path);
10.44 @@ -280,7 +281,7 @@
10.45
10.46 val parents = map (base_name o #1) imports;
10.47 val (parents_current, tasks') =
10.48 - require_thys (name :: initiators)
10.49 + require_thys last_timing (name :: initiators)
10.50 (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
10.51
10.52 val all_current = current andalso parents_current;
10.53 @@ -293,7 +294,8 @@
10.54 let
10.55 val update_time = serial ();
10.56 val load =
10.57 - load_thy initiators update_time dep text (name, theory_pos) uses keywords;
10.58 + load_thy last_timing initiators update_time dep
10.59 + text (name, theory_pos) uses keywords;
10.60 in Task (parents, load) end);
10.61
10.62 val tasks'' = new_entry name parents task tasks';
10.63 @@ -305,10 +307,10 @@
10.64
10.65 (* use_thy *)
10.66
10.67 -fun use_thys_wrt dir arg =
10.68 - schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
10.69 +fun use_theories {last_timing, master_dir} imports =
10.70 + schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
10.71
10.72 -val use_thys = use_thys_wrt Path.current;
10.73 +val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
10.74 val use_thy = use_thys o single;
10.75
10.76
10.77 @@ -318,7 +320,7 @@
10.78 let
10.79 val {name = (name, _), imports, ...} = header;
10.80 val _ = kill_thy name;
10.81 - val _ = use_thys_wrt master_dir imports;
10.82 + val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
10.83 val _ = Thy_Header.define_keywords header;
10.84 val parents = map (get_theory o base_name o fst) imports;
10.85 in Thy_Load.begin_theory master_dir header parents end;
11.1 --- a/src/Pure/Thy/thy_load.ML Thu Feb 21 12:22:26 2013 +0100
11.2 +++ b/src/Pure/Thy/thy_load.ML Thu Feb 21 15:10:04 2013 +0100
11.3 @@ -22,8 +22,8 @@
11.4 val use_ml: Path.T -> unit
11.5 val exec_ml: Path.T -> generic_theory -> generic_theory
11.6 val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
11.7 - val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
11.8 - theory list -> theory * unit future
11.9 + val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
11.10 + Position.T -> string -> theory list -> theory * unit future
11.11 val set_master_path: Path.T -> unit
11.12 val get_master_path: unit -> Path.T
11.13 end;
11.14 @@ -214,10 +214,13 @@
11.15 |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
11.16 |> Theory.checkpoint;
11.17
11.18 -fun excursion init elements =
11.19 +fun excursion last_timing init elements =
11.20 let
11.21 val immediate = not (Goal.future_enabled ());
11.22
11.23 + fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
11.24 + fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
11.25 +
11.26 fun proof_result (tr, trs) (st, _) =
11.27 let
11.28 val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
11.29 @@ -225,7 +228,7 @@
11.30 in (result, (st', pos')) end;
11.31
11.32 fun element_result elem x =
11.33 - fold_map proof_result
11.34 + fold_map (proof_result o put_timings)
11.35 (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
11.36
11.37 val (results, (end_state, end_pos)) =
11.38 @@ -234,7 +237,7 @@
11.39 val thy = Toplevel.end_theory end_pos end_state;
11.40 in (flat results, thy) end;
11.41
11.42 -fun load_thy update_time master_dir header text_pos text parents =
11.43 +fun load_thy last_timing update_time master_dir header text_pos text parents =
11.44 let
11.45 val time = ! Toplevel.timing;
11.46
11.47 @@ -255,7 +258,7 @@
11.48 (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
11.49
11.50 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
11.51 - val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
11.52 + val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
11.53 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
11.54
11.55 val present =
12.1 --- a/src/Pure/Thy/thy_syntax.ML Thu Feb 21 12:22:26 2013 +0100
12.2 +++ b/src/Pure/Thy/thy_syntax.ML Thu Feb 21 15:10:04 2013 +0100
12.3 @@ -15,8 +15,10 @@
12.4 val span_content: span -> Token.T list
12.5 val present_span: span -> Output.output
12.6 val parse_spans: Token.T list -> span list
12.7 - type element = {head: span, proof: span list, proper_proof: bool}
12.8 - val parse_elements: span list -> element list
12.9 + datatype 'a element = Element of 'a * ('a element list * 'a) option
12.10 + val map_element: ('a -> 'b) -> 'a element -> 'b element
12.11 + val flat_element: 'a element -> 'a list
12.12 + val parse_elements: span list -> span element list
12.13 end;
12.14
12.15 structure Thy_Syntax: THY_SYNTAX =
12.16 @@ -134,10 +136,17 @@
12.17
12.18 (** specification elements: commands with optional proof **)
12.19
12.20 -type element = {head: span, proof: span list, proper_proof: bool};
12.21 +datatype 'a element = Element of 'a * ('a element list * 'a) option;
12.22
12.23 -fun make_element head proof proper_proof =
12.24 - {head = head, proof = proof, proper_proof = proper_proof};
12.25 +fun element (a, b) = Element (a, SOME b);
12.26 +fun atom a = Element (a, NONE);
12.27 +
12.28 +fun map_element f (Element (a, NONE)) = Element (f a, NONE)
12.29 + | map_element f (Element (a, SOME (elems, b))) =
12.30 + Element (f a, SOME ((map o map_element) f elems, f b));
12.31 +
12.32 +fun flat_element (Element (a, NONE)) = [a]
12.33 + | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
12.34
12.35
12.36 (* scanning spans *)
12.37 @@ -159,24 +168,21 @@
12.38 fun command_with pred =
12.39 Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
12.40
12.41 -val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
12.42 - if d <= 0 then Scan.fail
12.43 - else
12.44 - command_with Keyword.is_qed_global >> pair ~1 ||
12.45 - command_with Keyword.is_proof_goal >> pair (d + 1) ||
12.46 - (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
12.47 - Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
12.48 +val proof_atom =
12.49 + Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
12.50
12.51 -val element =
12.52 - command_with Keyword.is_theory_goal -- proof
12.53 - >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
12.54 - Scan.one not_eof >> (fn a => make_element a [] true);
12.55 +fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
12.56 +and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
12.57 +
12.58 +val other_element =
12.59 + command_with Keyword.is_theory_goal -- proof_rest >> element ||
12.60 + Scan.one not_eof >> atom;
12.61
12.62 in
12.63
12.64 val parse_elements =
12.65 Source.of_list #>
12.66 - Source.source stopper (Scan.bulk element) NONE #>
12.67 + Source.source stopper (Scan.bulk other_element) NONE #>
12.68 Source.exhaust;
12.69
12.70 end;
13.1 --- a/src/Pure/Tools/build.ML Thu Feb 21 12:22:26 2013 +0100
13.2 +++ b/src/Pure/Tools/build.ML Thu Feb 21 15:10:04 2013 +0100
13.3 @@ -16,30 +16,23 @@
13.4
13.5 local
13.6
13.7 -fun ML_statistics (function :: stats) "" =
13.8 - if function = Markup.ML_statistics then SOME stats
13.9 - else NONE
13.10 - | ML_statistics _ _ = NONE;
13.11 +(* FIXME avoid hardwired stuff!? *)
13.12 +val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
13.13
13.14 -fun task_statistics (function :: stats) "" =
13.15 - if function = Markup.task_statistics then SOME stats
13.16 - else NONE
13.17 - | task_statistics _ _ = NONE;
13.18 -
13.19 -val print_properties = YXML.string_of_body o XML.Encode.properties;
13.20 +fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
13.21
13.22 in
13.23
13.24 fun protocol_message props output =
13.25 - (case ML_statistics props output of
13.26 - SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
13.27 - | NONE =>
13.28 - (case task_statistics props output of
13.29 - SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
13.30 - | NONE =>
13.31 - (case Markup.dest_loading_theory props of
13.32 - SOME name => writeln ("\floading_theory = " ^ name)
13.33 - | NONE => raise Fail "Undefined Output.protocol_message")));
13.34 + (case props of
13.35 + function :: args =>
13.36 + if member (op =) protocol_echo function then
13.37 + writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
13.38 + else
13.39 + (case Markup.dest_loading_theory props of
13.40 + SOME name => writeln ("\floading_theory = " ^ name)
13.41 + | NONE => protocol_undef ())
13.42 + | [] => protocol_undef ());
13.43
13.44 end;
13.45
13.46 @@ -51,8 +44,8 @@
13.47 fun no_document options =
13.48 (case Options.string options "document" of "" => true | "false" => true | _ => false);
13.49
13.50 -fun use_thys options =
13.51 - Thy_Info.use_thys
13.52 +fun use_theories last_timing options =
13.53 + Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
13.54 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
13.55 |> Unsynchronized.setmp print_mode
13.56 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
13.57 @@ -78,25 +71,49 @@
13.58 |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
13.59 |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
13.60
13.61 -fun use_theories (options, thys) =
13.62 +fun use_theories_condition last_timing (options, thys) =
13.63 let val condition = space_explode "," (Options.string options "condition") in
13.64 (case filter_out (can getenv_strict) condition of
13.65 - [] => use_thys options (map (rpair Position.none) thys)
13.66 + [] => use_theories last_timing options (map (rpair Position.none) thys)
13.67 | conds =>
13.68 Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
13.69 " (undefined " ^ commas conds ^ ")\n"))
13.70 end;
13.71
13.72 +
13.73 +(* command timings *)
13.74 +
13.75 +type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *)
13.76 +
13.77 +val empty_timings: timings = Symtab.empty;
13.78 +
13.79 +fun update_timings props =
13.80 + (case Markup.parse_command_timing_properties props of
13.81 + SOME ({file, offset, name}, time) =>
13.82 + Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
13.83 + | NONE => I);
13.84 +
13.85 +fun lookup_timings timings tr =
13.86 + (case Toplevel.approximative_id tr of
13.87 + SOME {file, offset, name} =>
13.88 + (case Symtab.lookup timings file of
13.89 + SOME offsets =>
13.90 + (case Inttab.lookup offsets offset of
13.91 + SOME (name', time) => if name = name' then time else Time.zeroTime
13.92 + | NONE => Time.zeroTime)
13.93 + | NONE => Time.zeroTime)
13.94 + | NONE => Time.zeroTime);
13.95 +
13.96 in
13.97
13.98 fun build args_file = Command_Line.tool (fn () =>
13.99 let
13.100 - val (do_output, (options, (verbose, (browser_info, (parent_name,
13.101 - (name, theories)))))) =
13.102 + val (command_timings, (do_output, (options, (verbose, (browser_info,
13.103 + (parent_name, (name, theories))))))) =
13.104 File.read (Path.explode args_file) |> YXML.parse_body |>
13.105 let open XML.Decode in
13.106 - pair bool (pair Options.decode (pair bool (pair string (pair string
13.107 - (pair string ((list (pair Options.decode (list string)))))))))
13.108 + pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
13.109 + (pair string (pair string ((list (pair Options.decode (list string))))))))))
13.110 end;
13.111
13.112 val document_variants =
13.113 @@ -122,9 +139,11 @@
13.114 (false, "") ""
13.115 verbose;
13.116
13.117 + val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
13.118 +
13.119 val res1 =
13.120 theories |>
13.121 - (List.app use_theories
13.122 + (List.app (use_theories_condition last_timing)
13.123 |> Session.with_timing name verbose
13.124 |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
13.125 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
14.1 --- a/src/Pure/Tools/build.scala Thu Feb 21 12:22:26 2013 +0100
14.2 +++ b/src/Pure/Tools/build.scala Thu Feb 21 15:10:04 2013 +0100
14.3 @@ -288,41 +288,71 @@
14.4
14.5 object Queue
14.6 {
14.7 - def apply(tree: Session_Tree): Queue =
14.8 + def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
14.9 {
14.10 val graph = tree.graph
14.11 + val sessions = graph.keys.toList
14.12 +
14.13 + val timings = sessions.map((name: String) =>
14.14 + if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
14.15 + else (name, (Nil, 0.0)))
14.16 + val command_timings =
14.17 + Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
14.18 + val session_timing =
14.19 + Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
14.20
14.21 def outdegree(name: String): Int = graph.imm_succs(name).size
14.22 def timeout(name: String): Double = tree(name).options.real("timeout")
14.23
14.24 object Ordering extends scala.math.Ordering[String]
14.25 {
14.26 + def compare_timing(name1: String, name2: String): Int =
14.27 + {
14.28 + val t1 = session_timing(name1)
14.29 + val t2 = session_timing(name2)
14.30 + if (t1 == 0.0 || t2 == 0.0) 0
14.31 + else t1 compare t2
14.32 + }
14.33 +
14.34 def compare(name1: String, name2: String): Int =
14.35 outdegree(name2) compare outdegree(name1) match {
14.36 case 0 =>
14.37 - timeout(name2) compare timeout(name1) match {
14.38 - case 0 => name1 compare name2
14.39 + compare_timing(name2, name1) match {
14.40 + case 0 =>
14.41 + timeout(name2) compare timeout(name1) match {
14.42 + case 0 => name1 compare name2
14.43 + case ord => ord
14.44 + }
14.45 case ord => ord
14.46 }
14.47 case ord => ord
14.48 }
14.49 }
14.50
14.51 - new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
14.52 + new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
14.53 }
14.54 }
14.55
14.56 - final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
14.57 + final class Queue private(
14.58 + graph: Graph[String, Session_Info],
14.59 + order: SortedSet[String],
14.60 + val command_timings: String => List[Properties.T])
14.61 {
14.62 def is_inner(name: String): Boolean = !graph.is_maximal(name)
14.63
14.64 def is_empty: Boolean = graph.is_empty
14.65
14.66 - def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
14.67 + def - (name: String): Queue =
14.68 + new Queue(graph.del_node(name),
14.69 + order - name, // FIXME scala-2.10.0 TreeSet problem!?
14.70 + command_timings)
14.71
14.72 def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
14.73 {
14.74 - val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
14.75 + val it = order.iterator.dropWhile(name =>
14.76 + skip(name)
14.77 + || !graph.defined(name) // FIXME scala-2.10.0 TreeSet problem!?
14.78 + || !graph.is_minimal(name))
14.79 if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
14.80 else None
14.81 }
14.82 @@ -419,7 +449,7 @@
14.83
14.84 private class Job(progress: Build.Progress,
14.85 name: String, val info: Session_Info, output: Path, do_output: Boolean,
14.86 - verbose: Boolean, browser_info: Path)
14.87 + verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
14.88 {
14.89 // global browser info dir
14.90 if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
14.91 @@ -443,10 +473,10 @@
14.92 else
14.93 {
14.94 import XML.Encode._
14.95 - pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
14.96 - pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
14.97 - (do_output, (info.options, (verbose, (browser_info, (parent,
14.98 - (name, info.theories)))))))
14.99 + pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
14.100 + pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
14.101 + (command_timings, (do_output, (info.options, (verbose, (browser_info,
14.102 + (parent, (name, info.theories))))))))
14.103 }))
14.104
14.105 private val env =
14.106 @@ -546,17 +576,26 @@
14.107
14.108
14.109 sealed case class Log_Info(
14.110 - name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
14.111 + name: String,
14.112 + stats: List[Properties.T],
14.113 + tasks: List[Properties.T],
14.114 + command_timings: List[Properties.T],
14.115 + session_timing: Properties.T)
14.116
14.117 - def parse_log(text: String): Log_Info =
14.118 + def parse_log(full_stats: Boolean, text: String): Log_Info =
14.119 {
14.120 val lines = split_lines(text)
14.121 + val xml_cache = new XML.Cache()
14.122 + def parse_lines(prfx: String): List[Properties.T] =
14.123 + Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
14.124 +
14.125 val name =
14.126 lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
14.127 - val stats = Props.parse_lines("\fML_statistics = ", lines)
14.128 - val tasks = Props.parse_lines("\ftask_statistics = ", lines)
14.129 - val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
14.130 - Log_Info(name, stats, tasks, timing)
14.131 + val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
14.132 + val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
14.133 + val command_timings = parse_lines("\fcommand_timing = ")
14.134 + val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
14.135 + Log_Info(name, stats, tasks, command_timings, session_timing)
14.136 }
14.137
14.138
14.139 @@ -612,16 +651,20 @@
14.140 verbose: Boolean = false,
14.141 sessions: List[String] = Nil): Int =
14.142 {
14.143 + /* session tree and dependencies */
14.144 +
14.145 val full_tree = find_sessions(options, more_dirs)
14.146 val (selected, selected_tree) =
14.147 full_tree.selection(requirements, all_sessions, session_groups, sessions)
14.148
14.149 val deps = dependencies(progress, true, verbose, list_files, selected_tree)
14.150 - val queue = Queue(selected_tree)
14.151
14.152 def make_stamp(name: String): String =
14.153 sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
14.154
14.155 +
14.156 + /* persistent information */
14.157 +
14.158 val (input_dirs, output_dir, browser_info) =
14.159 if (system_mode) {
14.160 val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
14.161 @@ -633,6 +676,40 @@
14.162 Path.explode("$ISABELLE_BROWSER_INFO"))
14.163 }
14.164
14.165 + def find_log(name: String): Option[(Path, Path)] =
14.166 + input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
14.167 +
14.168 +
14.169 + /* queue with scheduling information */
14.170 +
14.171 + def load_timings(name: String): (List[Properties.T], Double) =
14.172 + {
14.173 + val (path, text) =
14.174 + find_log(name + ".gz") match {
14.175 + case Some((_, path)) => (path, File.read_gzip(path))
14.176 + case None =>
14.177 + find_log(name) match {
14.178 + case Some((_, path)) => (path, File.read(path))
14.179 + case None => (Path.current, "")
14.180 + }
14.181 + }
14.182 + try {
14.183 + val info = parse_log(false, text)
14.184 + val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
14.185 + (info.command_timings, session_timing)
14.186 + }
14.187 + catch {
14.188 + case ERROR(msg) =>
14.189 + java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
14.190 + (Nil, 0.0)
14.191 + }
14.192 + }
14.193 +
14.194 + val queue = Queue(selected_tree, load_timings)
14.195 +
14.196 +
14.197 + /* main build process */
14.198 +
14.199 // prepare log dir
14.200 Isabelle_System.mkdirs(output_dir + LOG)
14.201
14.202 @@ -718,9 +795,9 @@
14.203
14.204 val (current, heap) =
14.205 {
14.206 - input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
14.207 - case Some(dir) =>
14.208 - read_stamps(dir + log_gz(name)) match {
14.209 + find_log(name + ".gz") match {
14.210 + case Some((dir, path)) =>
14.211 + read_stamps(path) match {
14.212 case Some((s, h1, h2)) =>
14.213 val heap = heap_stamp(Some(dir + Path.basic(name)))
14.214 (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
14.215 @@ -740,7 +817,9 @@
14.216 }
14.217 else if (parent_result.rc == 0) {
14.218 progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
14.219 - val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
14.220 + val job =
14.221 + new Job(progress, name, info, output, do_output, verbose, browser_info,
14.222 + queue.command_timings(name))
14.223 loop(pending, running + (name -> (parent_result.heap, job)), results)
14.224 }
14.225 else {
14.226 @@ -754,6 +833,9 @@
14.227 }
14.228 }
14.229
14.230 +
14.231 + /* build results */
14.232 +
14.233 val results =
14.234 if (deps.is_empty) {
14.235 progress.echo("### Nothing to build")
15.1 --- a/src/Pure/goal.ML Thu Feb 21 12:22:26 2013 +0100
15.2 +++ b/src/Pure/goal.ML Thu Feb 21 15:10:04 2013 +0100
15.3 @@ -24,8 +24,8 @@
15.4 val check_finished: Proof.context -> thm -> thm
15.5 val finish: Proof.context -> thm -> thm
15.6 val norm_result: thm -> thm
15.7 - val fork_name: string -> (unit -> 'a) -> 'a future
15.8 - val fork: (unit -> 'a) -> 'a future
15.9 + val fork_name: string -> int -> (unit -> 'a) -> 'a future
15.10 + val fork: int -> (unit -> 'a) -> 'a future
15.11 val peek_futures: serial -> unit future list
15.12 val reset_futures: unit -> Future.group list
15.13 val future_enabled_level: int -> bool
15.14 @@ -134,7 +134,7 @@
15.15
15.16 in
15.17
15.18 -fun fork_name name e =
15.19 +fun fork_name name pri e =
15.20 uninterruptible (fn _ => fn () =>
15.21 let
15.22 val pos = Position.thread_data ();
15.23 @@ -143,7 +143,7 @@
15.24
15.25 val future =
15.26 (singleton o Future.forks)
15.27 - {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
15.28 + {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
15.29 (fn () =>
15.30 let
15.31 val task = the (Future.worker_task ());
15.32 @@ -167,7 +167,7 @@
15.33 val _ = register_forked id future;
15.34 in future end) ();
15.35
15.36 -fun fork e = fork_name "Goal.fork" e;
15.37 +fun fork pri e = fork_name "Goal.fork" pri e;
15.38
15.39 fun forked_count () = #1 (Synchronized.value forked_proofs);
15.40
15.41 @@ -285,7 +285,7 @@
15.42 val res =
15.43 if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
15.44 then result ()
15.45 - else future_result ctxt' (fork result) (Thm.term_of stmt);
15.46 + else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
15.47 in
15.48 Conjunction.elim_balanced (length props) res
15.49 |> map (Assumption.export false ctxt' ctxt)