# HG changeset patch # User Andreas Lochbihler # Date 1361957625 -3600 # Node ID 8c15e50aedadf6cdec2347aa788779747060c596 # Parent be7e9a675ec9f67f3a15ce6e65c8f4e950fe8447# Parent 8799eadf61fb668800e49b45bb351fbfb6ab081c merged diff -r be7e9a675ec9 -r 8c15e50aedad src/Doc/Tutorial/ToyList/ToyList.thy --- a/src/Doc/Tutorial/ToyList/ToyList.thy Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy Wed Feb 27 10:33:45 2013 +0100 @@ -3,13 +3,14 @@ begin (*<*) -ML {* +ML {* (* FIXME somewhat non-standard, fragile *) let val texts = map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) ["ToyList1", "ToyList2"]; val trs = Outer_Syntax.parse Position.start (implode texts); - in @{assert} (Toplevel.is_toplevel (fold Toplevel.command trs Toplevel.toplevel)) end; + val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; + in @{assert} (Toplevel.is_toplevel end_state) end; *} (*>*) diff -r be7e9a675ec9 -r 8c15e50aedad src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Wed Feb 27 10:33:30 2013 +0100 +++ b/src/HOL/Word/Word.thy Wed Feb 27 10:33:45 2013 +0100 @@ -1644,11 +1644,10 @@ apply (erule (2) udvd_decr0) done -ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *} - lemma udvd_incr2_K: "p < a + s \ a <= a + s \ K udvd s \ K udvd p - a \ a <= p \ 0 < K \ p <= p + K & p + K <= a + s" + using [[simproc del: linordered_ring_less_cancel_factor]] apply (unfold udvd_def) apply clarify apply (simp add: uint_arith_simps split: split_if_asm) @@ -1662,8 +1661,6 @@ apply simp done -ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *} - (* links with rbl operations *) lemma word_succ_rbl: "to_bl w = bl \ to_bl (word_succ w) = (rev (rbl_succ (rev bl)))" diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/Concurrent/future.ML Wed Feb 27 10:33:45 2013 +0100 @@ -154,10 +154,6 @@ fun broadcast cond = (*requires SYNCHRONIZED*) ConditionVar.broadcast cond; -fun broadcast_work () = (*requires SYNCHRONIZED*) - (ConditionVar.broadcast work_available; - ConditionVar.broadcast work_finished); - end; @@ -331,7 +327,7 @@ val _ = workers := alive; in Multithreading.tracing 0 (fn () => - "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads") + "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads") end; @@ -380,7 +376,7 @@ (Multithreading.tracing 1 (fn () => string_of_int (length (! canceled)) ^ " canceled groups"); Unsynchronized.change canceled (filter_out (null o cancel_now)); - broadcast_work ()); + signal work_available); (* delay loop *) @@ -398,9 +394,9 @@ in continue end handle exn => if Exn.is_interrupt exn then - (Multithreading.tracing 1 (fn () => "Interrupt"); + (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt"); List.app cancel_later (cancel_all ()); - broadcast_work (); true) + signal work_available; true) else reraise exn; fun scheduler_loop () = @@ -682,11 +678,14 @@ (* shutdown *) fun shutdown () = - if Multithreading.available then + if not Multithreading.available then () + else if is_some (worker_task ()) then + raise Fail "Cannot shutdown while running as worker thread" + else SYNCHRONIZED "shutdown" (fn () => - while scheduler_active () do - (wait scheduler_event; broadcast_work ())) - else (); + while scheduler_active () do + (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait"); + wait scheduler_event)); (*final declarations of this structure!*) diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/Isar/runtime.ML Wed Feb 27 10:33:45 2013 +0100 @@ -12,7 +12,8 @@ exception TOPLEVEL_ERROR val debug: bool Unsynchronized.ref val exn_context: Proof.context option -> exn -> exn - val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list + type error = ((serial * string) * string option) + val exn_messages_ids: (exn -> Position.T) -> exn -> error list val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list val exn_message: (exn -> Position.T) -> exn -> string val debugging: ('a -> 'b) -> 'a -> 'b @@ -43,6 +44,8 @@ (* exn_message *) +type error = ((serial * string) * string option); + local fun if_context NONE _ _ = [] diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Feb 27 10:33:45 2013 +0100 @@ -94,7 +94,8 @@ 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 command_exception: bool -> transition -> state -> state + val command_errors: bool -> transition -> state -> Runtime.error list * state option val element_result: transition Thy_Syntax.element -> state -> (transition * state) list future * state end; @@ -636,8 +637,7 @@ local fun timing_message tr (t: Timing.timing) = - if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr)) - then + if Timing.is_relevant_time (#elapsed t) then (case approximative_id tr of SOME id => (Output.protocol_message @@ -685,15 +685,21 @@ end; -(* nested commands *) +(* managed commands *) -fun command tr st = - (case transition (! interact) tr st of +fun command_exception int tr st = + (case transition int tr st of SOME (st', NONE) => st' | SOME (_, SOME (exn, info)) => if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info) | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr)); +fun command_errors int tr st = + (case transition int tr st of + SOME (st', NONE) => ([], SOME st') + | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE) + | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE)); + (* scheduled proof result *) @@ -704,12 +710,23 @@ fun init _ = empty; ); +fun priority trs = + let val estimate = fold (curry Time.+ o get_timing) trs Time.zeroTime in + if estimate = Time.zeroTime then ~1 + else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1) + end; + fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st = let - val future_enabled = Goal.future_enabled (); + val command = command_exception (! interact); fun atom_result tr st = - let val st' = command tr st + let + val st' = + if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then + setmp_thread_position tr (fn () => + (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) () + else command tr st; in ((tr, st'), st') end; val proof_trs = @@ -717,9 +734,9 @@ NONE => [] | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored); - val st' = command head_tr st; + val (_, st') = atom_result head_tr st; in - if not future_enabled orelse is_ignored head_tr orelse + if not (Goal.future_enabled ()) orelse is_ignored head_tr orelse null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st') then let val (results, st'') = fold_map atom_result proof_trs st' @@ -729,20 +746,16 @@ val (body_trs, end_tr) = split_last proof_trs; val finish = Context.Theory o Proof_Context.theory_of; - val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime; - val pri = - if estimate = Time.zeroTime then ~1 - else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1); - val future_proof = Proof.global_future_proof (fn prf => - Goal.fork_name "Toplevel.future_proof" pri - (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)) + setmp_thread_position head_tr (fn () => + Goal.fork_name "Toplevel.future_proof" (priority proof_trs) + (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)) ()) #-> Result.put; val st'' = st' diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/ML/ml_compiler.ML Wed Feb 27 10:33:45 2013 +0100 @@ -7,7 +7,7 @@ signature ML_COMPILER = sig val exn_position: exn -> Position.T - val exn_messages_ids: exn -> ((serial * string) * string option) list + val exn_messages_ids: exn -> Runtime.error list val exn_messages: exn -> (serial * string) list val exn_message: exn -> string val eval: bool -> Position.T -> ML_Lex.token list -> unit diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/PIDE/command.ML Wed Feb 27 10:33:45 2013 +0100 @@ -62,10 +62,11 @@ local fun run int tr st = - (case Toplevel.transition int tr st of - SOME (st', NONE) => ([], SOME st') - | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE) - | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE)); + if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then + Toplevel.setmp_thread_position tr (fn () => + (Goal.fork_name "Toplevel.diag" ~1 + (fn () => Toplevel.command_exception int tr st); ([], SOME st))) () + else Toplevel.command_errors int tr st; fun check_cmts tr cmts st = Toplevel.setmp_thread_position tr diff -r be7e9a675ec9 -r 8c15e50aedad src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Feb 27 10:33:30 2013 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Feb 27 10:33:45 2013 +0100 @@ -164,7 +164,7 @@ (* scheduling loader tasks *) -type result = theory * unit future * (unit -> unit); +type result = theory * serial * unit future * (unit -> unit); datatype task = Task of string list * (theory list -> result) | @@ -177,8 +177,14 @@ local -fun finish_thy ((thy, present, commit): result) = - (Thm.join_theory_proofs thy; Future.join present; commit (); thy); +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) => @@ -186,22 +192,29 @@ Task (parents, body) => finish_thy (body (task_parents deps parents)) | Finished thy => thy)) #> ignore; -val schedule_futures = uninterruptible (fn _ => - String_Graph.schedule (fn deps => fn (name, task) => - (case task of - Task (parents, body) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = NONE, - 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)) - | bad => - error (loader_msg ("failed to load " ^ quote name ^ - " (unresolved " ^ commas_quote (map #1 bad) ^ ")") []))) - | Finished thy => Future.value (thy, Future.value (), I))) - #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]) - #> rev #> Par_Exn.release_all) #> ignore; +val schedule_futures = uninterruptible (fn _ => fn tasks => + let + val results1 = tasks + |> String_Graph.schedule (fn deps => fn (name, task) => + (case task of + Task (parents, body) => + (singleton o Future.forks) + {name = "theory:" ^ name, group = NONE, + 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)) + | 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]); + + (* FIXME avoid global reset_futures (!??) *) + val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ())); + + val _ = Par_Exn.release_all (rev (results2 @ results1)); + in () end); in @@ -234,11 +247,13 @@ val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); + val id = serial (); + val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path); val (theory, present) = - Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text + 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, present, commit) end; + in (theory, id, present, commit) end; fun check_deps dir name = (case lookup_deps name of