discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;
--- a/etc/options Sun Aug 25 14:35:25 2013 +0200
+++ b/etc/options Sun Aug 25 16:03:12 2013 +0200
@@ -71,8 +71,6 @@
-- "level of tracing information for multithreading"
public option parallel_proofs : int = 2
-- "level of parallel proof checking: 0, 1, 2"
-option parallel_subproofs_saturation : int = 100
- -- "upper bound for forks of nested proofs (multiplied by worker threads)"
option parallel_subproofs_threshold : real = 0.01
-- "lower bound of timing estimate for forked nested proofs (seconds)"
--- a/src/Pure/Concurrent/future.ML Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Sun Aug 25 16:03:12 2013 +0200
@@ -55,7 +55,6 @@
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val ML_statistics: bool Unsynchronized.ref
- val forked_proofs: int Unsynchronized.ref
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -200,7 +199,6 @@
(* status *)
val ML_statistics = Unsynchronized.ref false;
-val forked_proofs = Unsynchronized.ref 0;
fun report_status () = (*requires SYNCHRONIZED*)
if ! ML_statistics then
@@ -211,7 +209,6 @@
val waiting = count_workers Waiting;
val stats =
[("now", Markup.print_real (Time.toReal (Time.now ()))),
- ("tasks_proof", Markup.print_int (! forked_proofs)),
("tasks_ready", Markup.print_int ready),
("tasks_pending", Markup.print_int pending),
("tasks_running", Markup.print_int running),
--- a/src/Pure/Isar/proof.ML Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/Isar/proof.ML Sun Aug 25 16:03:12 2013 +0200
@@ -1164,7 +1164,7 @@
local
fun future_terminal_proof proof1 proof2 done int state =
- if Goal.future_enabled_level 3 andalso not (is_relevant state) then
+ if Goal.future_enabled 3 andalso not (is_relevant state) then
state |> future_proof (fn state' =>
let
val pos = Position.thread_data ();
--- a/src/Pure/Isar/toplevel.ML Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Sun Aug 25 16:03:12 2013 +0200
@@ -698,16 +698,16 @@
| SOME state =>
not (Proof.is_relevant state) andalso
(if can (Proof.assert_bottom true) state
- then Goal.future_enabled ()
+ then Goal.future_enabled 1
else
(case estimate of
- NONE => Goal.future_enabled_nested 2
+ NONE => Goal.future_enabled 2
| SOME t => Goal.future_enabled_timing t)));
fun atom_result tr st =
let
val st' =
- if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
+ if Goal.future_enabled 1 andalso Keyword.is_diag (name_of tr) then
(Goal.fork_params
{name = "Toplevel.diag", pos = pos_of tr,
pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
--- a/src/Pure/PIDE/command.ML Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/PIDE/command.ML Sun Aug 25 16:03:12 2013 +0200
@@ -130,7 +130,7 @@
local
fun run int tr st =
- if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
+ if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
(Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
(fn () => Toplevel.command_exception int tr st); ([], SOME st))
else Toplevel.command_errors int tr st;
--- a/src/Pure/Tools/ml_statistics.scala Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/Tools/ml_statistics.scala Sun Aug 25 16:03:12 2013 +0200
@@ -48,8 +48,7 @@
val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
val tasks_fields =
- ("Future tasks",
- List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+ ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
val workers_fields =
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
--- a/src/Pure/goal.ML Sun Aug 25 14:35:25 2013 +0200
+++ b/src/Pure/goal.ML Sun Aug 25 16:03:12 2013 +0200
@@ -31,9 +31,7 @@
val reset_futures: unit -> Future.group list
val shutdown_futures: unit -> unit
val skip_proofs_enabled: unit -> bool
- val future_enabled_level: int -> bool
- val future_enabled: unit -> bool
- val future_enabled_nested: int -> bool
+ val future_enabled: int -> bool
val future_enabled_timing: Time.time -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
@@ -119,21 +117,12 @@
val forked_proofs =
Synchronized.var "forked_proofs"
- (0, Inttab.empty: (Future.group * unit future) list Inttab.table);
-
-fun count_forked i =
- Synchronized.change forked_proofs (fn (m, tab) =>
- let
- val n = m + i;
- val _ = Future.forked_proofs := n;
- in (n, tab) end);
+ (Inttab.empty: (Future.group * unit future) list Inttab.table);
fun register_forked id future =
- Synchronized.change forked_proofs (fn (m, tab) =>
- let
- val group = Task_Queue.group_of_task (Future.task_of future);
- val tab' = Inttab.cons_list (id, (group, Future.map (K ()) future)) tab;
- in (m, tab') end);
+ Synchronized.change forked_proofs (fn tab =>
+ let val group = Task_Queue.group_of_task (Future.task_of future)
+ in Inttab.cons_list (id, (group, Future.map (K ()) future)) tab end);
fun status task markups =
let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
@@ -145,7 +134,6 @@
uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
let
val id = the_default 0 (Position.parse_id pos);
- val _ = count_forked 1;
val future =
(singleton o Future.forks)
@@ -167,7 +155,6 @@
(status task [Markup.failed];
Output.report (Markup.markup_only Markup.bad);
List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
- val _ = count_forked ~1;
in Exn.release result end);
val _ = status (Future.task_of future) [Markup.forked];
val _ = register_forked id future;
@@ -176,32 +163,27 @@
fun fork pri e =
fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
-fun forked_count () = #1 (Synchronized.value forked_proofs);
-
fun peek_futures id =
- map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
+ map #2 (Inttab.lookup_list (Synchronized.value forked_proofs) id);
fun check_canceled id group =
if Task_Queue.is_canceled group then ()
else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
fun purge_futures ids =
- Synchronized.change forked_proofs (fn (_, tab) =>
+ Synchronized.change forked_proofs (fn tab =>
let
val tab' = fold Inttab.delete_safe ids tab;
- val n' =
- Inttab.fold (fn (id, futures) => fn m =>
- if Inttab.defined tab' id then m + length futures
- else (List.app (check_canceled id o #1) futures; m)) tab 0;
- val _ = Future.forked_proofs := n';
- in (n', tab') end);
+ val () =
+ Inttab.fold (fn (id, futures) => fn () =>
+ if Inttab.defined tab' id then ()
+ else List.app (check_canceled id o #1) futures) tab ();
+ in tab' end);
fun reset_futures () =
- Synchronized.change_result forked_proofs (fn (_, tab) =>
- let
- val groups = Inttab.fold (fold (cons o #1) o #2) tab [];
- val _ = Future.forked_proofs := 0;
- in (groups, (0, Inttab.empty)) end);
+ Synchronized.change_result forked_proofs (fn tab =>
+ let val groups = Inttab.fold (fold (cons o #1) o #2) tab []
+ in (groups, Inttab.empty) end);
fun shutdown_futures () =
(Future.shutdown ();
@@ -223,19 +205,12 @@
val parallel_proofs = Unsynchronized.ref 1;
-fun future_enabled_level n =
+fun future_enabled n =
Multithreading.enabled () andalso ! parallel_proofs >= n andalso
is_some (Future.worker_task ());
-fun future_enabled () = future_enabled_level 1;
-
-fun future_enabled_nested n =
- future_enabled_level n andalso
- forked_count () <
- Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value ();
-
fun future_enabled_timing t =
- future_enabled () andalso
+ future_enabled 1 andalso
Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
@@ -299,7 +274,7 @@
val string_of_term = Syntax.string_of_term ctxt;
val schematic = exists is_schematic props;
- val future = future_enabled ();
+ val future = future_enabled 1;
val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
val pos = Position.thread_data ();
@@ -363,7 +338,7 @@
fun prove_sorry ctxt xs asms prop tac =
if Config.get ctxt quick_and_dirty then
prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
- else (if future_enabled () then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
+ else (if future_enabled 1 then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
fun prove_sorry_global thy xs asms prop tac =
Drule.export_without_context