--- a/src/Pure/Isar/proof.ML Wed Feb 20 12:04:42 2013 +0100
+++ b/src/Pure/Isar/proof.ML Mon Mar 04 17:32:10 2013 +0100
@@ -1191,7 +1191,7 @@
in
fun local_future_terminal_proof meths =
- future_terminal_proof 2
+ future_terminal_proof 3
(local_terminal_proof meths)
(local_terminal_proof meths #> context_of) local_done_proof;
--- a/src/Pure/Isar/toplevel.ML Wed Feb 20 12:04:42 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 04 17:32:10 2013 +0100
@@ -96,8 +96,9 @@
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
- val element_result: transition Thy_Syntax.element -> state ->
- (transition * state) list future * state
+ type result
+ val join_results: result -> (transition * state) list
+ val element_result: transition Thy_Syntax.element -> state -> result * state
end;
structure Toplevel: TOPLEVEL =
@@ -705,19 +706,26 @@
(* scheduled proof result *)
+datatype result =
+ Result of transition * state |
+ Result_List of result list |
+ Result_Future of result future;
+
+fun join_results (Result x) = [x]
+ | join_results (Result_List xs) = maps join_results xs
+ | join_results (Result_Future x) = join_results (Future.join x);
+
local
structure Result = Proof_Data
(
- type T = (transition * state) list future;
- val empty: T = Future.value [];
+ type T = result;
+ val empty: T = Result_List [];
fun init _ = empty;
);
-fun done_proof state =
- if can (Proof.assert_bottom true) state
- then Proof.global_done_proof state
- else Proof.context_of (Proof.local_done_proof state);
+val get_result = Result.get o Proof.context_of;
+val put_result = Proof.map_context o Result.put;
fun proof_future_enabled st =
(case try proof_of st of
@@ -744,46 +752,52 @@
(Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
(fn () => command tr st); st)) ()
else command tr st;
- in ((tr, st'), st') end;
+ in (Result (tr, st'), st') end;
in
-fun element_result (Thy_Syntax.Element (tr, NONE)) st =
- let val (result, st') = atom_result tr st
- in (Future.value [result], st') end
- | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
+fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
+ | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
let
val (head_result, st') = atom_result head_tr st;
- val (body_elems, end_tr) = proof;
- val body_trs = maps Thy_Syntax.flat_element body_elems;
+ val (body_elems, end_tr) = element_rest;
in
if not (proof_future_enabled st')
then
- let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
- in (Future.value (head_result :: proof_results), st'') end
+ let
+ val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
+ val (proof_results, st'') = fold_map atom_result proof_trs st';
+ in (Result_List (head_result :: proof_results), st'') end
else
let
val finish = Context.Theory o Proof_Context.theory_of;
val future_proof = Proof.future_proof
- (fn prf =>
+ (fn state =>
setmp_thread_position head_tr (fn () =>
Goal.fork_name "Toplevel.future_proof"
- (priority (Thy_Syntax.Element (empty, SOME proof)))
+ (priority (Thy_Syntax.Element (empty, SOME element_rest)))
(fn () =>
- let val (result, result_state) =
- (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
- => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
- |> fold_map atom_result body_trs ||> command end_tr;
- in (result, presentation_context_of result_state) end)) ())
- #> (fn (result, state') => state' |> done_proof |> Result.put result);
+ let
+ val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
+ val prf' = Proof_Node.apply (K state) prf;
+ val (result, result_state) =
+ State (SOME (Proof (prf', (finish, orig_gthy))), prev)
+ |> fold_map element_result body_elems ||> command end_tr;
+ in (Result_List result, presentation_context_of result_state) end)) ())
+ #> (fn (res, state') => state' |> put_result (Result_Future res));
+
+ val forked_proof =
+ proof (future_proof #>
+ (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
+ end_proof (fn _ => future_proof #>
+ (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
val st'' = st'
- |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+ |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
+ val end_result = Result (end_tr, st'');
val result =
- Result.get (presentation_context_of st'')
- |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
-
+ Result_List [head_result, Result.get (presentation_context_of st''), end_result];
in (result, st'') end
end;
--- a/src/Pure/System/isabelle_process.ML Wed Feb 20 12:04:42 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Mar 04 17:32:10 2013 +0100
@@ -242,7 +242,7 @@
Multithreading.max_threads := Options.int options "threads";
if Multithreading.max_threads_value () < 2
then Multithreading.max_threads := 2 else ();
- Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
+ Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
tracing_messages := Options.int options "editor_tracing_messages"
end);
--- a/src/Pure/Thy/thy_info.ML Wed Feb 20 12:04:42 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Mar 04 17:32:10 2013 +0100
@@ -164,7 +164,22 @@
(* scheduling loader tasks *)
-type result = theory * serial * unit future * (unit -> unit);
+datatype result =
+ Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
+
+fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
+
+fun result_theory (Result {theory, ...}) = theory;
+fun result_present (Result {present, ...}) = present;
+fun result_commit (Result {commit, ...}) = commit;
+fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
+
+fun join_proofs (Result {theory, id, present, ...}) =
+ let
+ val result1 = Exn.capture Thm.join_theory_proofs theory;
+ val results2 = Future.join_results (Goal.peek_futures id);
+ in result1 :: results2 end;
+
datatype task =
Task of string list * (theory list -> result) |
@@ -177,24 +192,21 @@
local
-fun finish_thy ((thy, id, present, commit): result) =
- let
- val result1 = Exn.capture Thm.join_theory_proofs thy;
- val results2 = Future.join_results (Goal.peek_futures id);
- val result3 = Future.join_result present;
- val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
- val _ = commit ();
- in thy end;
-
val schedule_seq =
String_Graph.schedule (fn deps => fn (_, task) =>
(case task of
- Task (parents, body) => finish_thy (body (task_parents deps parents))
+ Task (parents, body) =>
+ let
+ val result = body (task_parents deps parents);
+ val _ = Par_Exn.release_all (join_proofs result);
+ val _ = result_present result ();
+ val _ = result_commit result ();
+ in result_theory result end
| Finished thy => thy)) #> ignore;
val schedule_futures = uninterruptible (fn _ => fn tasks =>
let
- val results1 = tasks
+ val futures = tasks
|> String_Graph.schedule (fn deps => fn (name, task) =>
(case task of
Task (parents, body) =>
@@ -203,17 +215,31 @@
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
(fn () =>
(case filter (not o can Future.join o #2) deps of
- [] => body (map (#1 o Future.join) (task_parents deps parents))
+ [] => body (map (result_theory o Future.join) (task_parents deps parents))
| bad =>
error (loader_msg ("failed to load " ^ quote name ^
" (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
- | Finished thy => Future.value (thy, 0, Future.value (), I)))
- |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
+ | Finished theory => Future.value (theory_result theory)));
+
+ val results1 = futures
+ |> maps (fn future =>
+ (case Future.join_result future of
+ Exn.Res result => join_proofs result
+ | Exn.Exn exn => [Exn.Exn exn]));
+
+ val results2 = futures
+ |> map_filter (Exn.get_res o Future.join_result)
+ |> sort result_ord
+ |> Par_List.map (fn result => Exn.capture (result_present result) ());
+
+ (* FIXME more precise commit order (!?) *)
+ val results3 = futures
+ |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
(* FIXME avoid global reset_futures (!??) *)
- val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
+ val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
- val _ = Par_Exn.release_all (rev (results2 @ results1));
+ val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
in () end);
in
@@ -249,11 +275,11 @@
val id = serial ();
val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
- val (theory, present) =
+ val (theory, present, weight) =
Thy_Load.load_thy last_timing update_time dir header text_pos text
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
- in (theory, id, present, commit) end;
+ in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
fun check_deps dir name =
(case lookup_deps name of
--- a/src/Pure/Thy/thy_load.ML Wed Feb 20 12:04:42 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Mon Mar 04 17:32:10 2013 +0100
@@ -23,7 +23,7 @@
val exec_ml: Path.T -> generic_theory -> generic_theory
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
- Position.T -> string -> theory list -> theory * unit future
+ Position.T -> string -> theory list -> theory * (unit -> unit) * int
val set_master_path: Path.T -> unit
val get_master_path: unit -> Path.T
end;
@@ -258,19 +258,18 @@
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 =
- Future.flat results |> Future.map (fn res0 =>
- let
- val res = filter_out (Toplevel.is_ignored o #1) res0;
- val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
- in
- Thy_Output.present_thy minor Keyword.command_tags
- (Outer_Syntax.is_markup outer_syntax) res toks
- |> Buffer.content
- |> Present.theory_output name
- end);
+ fun present () =
+ let
+ val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
+ val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
+ in
+ Thy_Output.present_thy minor Keyword.command_tags
+ (Outer_Syntax.is_markup outer_syntax) res toks
+ |> Buffer.content
+ |> Present.theory_output name
+ end;
- in (thy, present) end;
+ in (thy, present, size text) end;
(* document antiquotation *)