# HG changeset patch
# User wenzelm
# Date 1377439392 -7200
# Node ID ee8b8dafef0ebafb0fec224011f9ef23586535ae
# Parent  bb5433b13ff2b074b5b6db4b4b1a3a2a1c778a17
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;

diff -r bb5433b13ff2 -r ee8b8dafef0e etc/options
--- 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)"
 
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/Concurrent/future.ML
--- 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),
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/Isar/proof.ML
--- 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 ();
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/Isar/toplevel.ML
--- 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))}
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/PIDE/command.ML
--- 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;
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/Tools/ml_statistics.scala
--- 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"))
diff -r bb5433b13ff2 -r ee8b8dafef0e src/Pure/goal.ML
--- 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