# HG changeset patch # User wenzelm # Date 1362414730 -3600 # Node ID 2cfd028a2fd987023175758a0cfe2019b72433af # Parent 4a3c453f99a13544452824753a4e0eb5fedb3827# Parent 8707df0b0255651e3dd40781bd457776d1fdd713 merged diff -r 4a3c453f99a1 -r 2cfd028a2fd9 src/Pure/Isar/proof.ML --- 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; diff -r 4a3c453f99a1 -r 2cfd028a2fd9 src/Pure/Isar/toplevel.ML --- 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; diff -r 4a3c453f99a1 -r 2cfd028a2fd9 src/Pure/System/isabelle_process.ML --- 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); diff -r 4a3c453f99a1 -r 2cfd028a2fd9 src/Pure/Thy/thy_info.ML --- 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 diff -r 4a3c453f99a1 -r 2cfd028a2fd9 src/Pure/Thy/thy_load.ML --- 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 *)