# HG changeset patch
# User wenzelm
# Date 1525891557 -7200
# Node ID 6fb85346cb7966c44be2df37942995bb275c34c0
# Parent  b73678836f8ed1bcbbf3d89814fdbcacaa872921
clarified future scheduling parameters, with support for parallel_limit;

diff -r b73678836f8e -r 6fb85346cb79 etc/options
--- a/etc/options	Wed May 09 19:53:37 2018 +0200
+++ b/etc/options	Wed May 09 20:45:57 2018 +0200
@@ -71,6 +71,8 @@
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
+public option parallel_limit : int = 0
+  -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed May 09 20:45:57 2018 +0200
@@ -34,6 +34,10 @@
   val forked_results: {name: string, deps: Task_Queue.task list} ->
     (unit -> 'a) list -> 'a Exn.result list
   val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
+  val enabled: unit -> bool
+  val relevant: 'a list -> bool
+  val proofs_enabled: int -> bool
+  val proofs_enabled_timing: Time.time -> bool
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
@@ -577,6 +581,22 @@
     end);
 
 
+(* scheduling parameters *)
+
+fun enabled () =
+  Multithreading.max_threads () > 1 andalso
+    let val lim = Options.default_int "parallel_limit"
+    in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end;
+
+val relevant = (fn [] => false | [_] => false | _ => enabled ());
+
+fun proofs_enabled n =
+  ! Multithreading.parallel_proofs >= n andalso is_some (worker_task ()) andalso enabled ();
+
+fun proofs_enabled_timing t =
+  proofs_enabled 1 andalso Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
+
+
 (* fast-path operations -- bypass task queue if possible *)
 
 fun value_result (res: 'a Exn.result) =
@@ -590,7 +610,7 @@
 fun value x = value_result (Exn.Res x);
 
 fun cond_forks args es =
-  if Multithreading.enabled () then forks args es
+  if enabled () then forks args es
   else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 fun map_future f x =
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed May 09 20:45:57 2018 +0200
@@ -129,7 +129,7 @@
     val pending =
       xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
     val _ =
-      if Multithreading.relevant pending then
+      if Future.relevant pending then
         ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
       else List.app (fn e => ignore (e ())) pending;
   in xs end;
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Wed May 09 20:45:57 2018 +0200
@@ -8,10 +8,7 @@
 sig
   val max_threads: unit -> int
   val max_threads_update: int -> unit
-  val enabled: unit -> bool
-  val relevant: 'a list -> bool
   val parallel_proofs: int ref
-  val parallel_proofs_enabled: int -> bool
   val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
@@ -42,9 +39,6 @@
 
 fun max_threads () = ! max_threads_state;
 fun max_threads_update m = max_threads_state := max_threads_result m;
-fun enabled () = max_threads () > 1;
-
-val relevant = (fn [] => false | [_] => false | _ => enabled ());
 
 end;
 
@@ -53,9 +47,6 @@
 
 val parallel_proofs = ref 1;
 
-fun parallel_proofs_enabled n =
-  enabled () andalso ! parallel_proofs >= n;
-
 
 (* synchronous wait *)
 
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed May 09 20:45:57 2018 +0200
@@ -29,7 +29,7 @@
 struct
 
 fun forked_results name f xs =
-  if Multithreading.relevant xs
+  if Future.relevant xs
   then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
   else map (Exn.capture f) xs;
 
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Wed May 09 20:45:57 2018 +0200
@@ -1301,7 +1301,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 done state =
-  if Goal.future_enabled 3 andalso not (is_relevant state) then
+  if Future.proofs_enabled 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
       let val pos = Position.thread_data () in
         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 09 20:45:57 2018 +0200
@@ -668,19 +668,19 @@
   let val trs = tl (Thy_Syntax.flat_element elem)
   in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
 
-fun proof_future_enabled estimate st =
+fun future_proofs_enabled estimate st =
   (case try proof_of st of
     NONE => false
   | SOME state =>
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
-        then Goal.future_enabled 1
-        else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
+        then Future.proofs_enabled 1
+        else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
 
 fun atom_result keywords tr st =
   let
     val st' =
-      if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
+      if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
         (Execution.fork
           {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
           (fn () => command tr st); st)
@@ -696,7 +696,7 @@
         val (body_elems, end_tr) = element_rest;
         val estimate = timing_estimate elem;
       in
-        if not (proof_future_enabled estimate st')
+        if not (future_proofs_enabled estimate st')
         then
           let
             val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 09 20:45:57 2018 +0200
@@ -120,7 +120,7 @@
       |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
       |> Output.report;
     val _ =
-      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+      if not (null persistent_reports) andalso redirect andalso Future.enabled ()
       then
         Execution.print
           {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Wed May 09 20:45:57 2018 +0200
@@ -190,7 +190,7 @@
   end) ();
 
 fun run keywords int tr st =
-  if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
+  if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     (Execution.fork {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;
@@ -429,7 +429,7 @@
 
 fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
   if ignore_process print_process then ()
-  else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
+  else if pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print")
   then
     let
       val group = Future.worker_subgroup ();
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/PIDE/execution.ML	Wed May 09 20:45:57 2018 +0200
@@ -162,7 +162,7 @@
 fun fork_prints exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (_, prints) =>
-      if Multithreading.relevant prints then
+      if Future.relevant prints then
         let val pos = Position.thread_data () in
           List.app (fn {name, pri, body} =>
             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 09 20:45:57 2018 +0200
@@ -388,7 +388,7 @@
       {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
         last_timing = last_timing};
     val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
-  in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
+  in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/goal.ML	Wed May 09 20:45:57 2018 +0200
@@ -23,8 +23,6 @@
   val finish: Proof.context -> thm -> thm
   val norm_result: Proof.context -> thm -> thm
   val skip_proofs_enabled: unit -> 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: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   val is_schematic: term -> bool
@@ -111,14 +109,6 @@
     else skip
   end;
 
-fun future_enabled n =
-  Multithreading.parallel_proofs_enabled n andalso
-  is_some (Future.worker_task ());
-
-fun future_enabled_timing t =
-  future_enabled 1 andalso
-    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
-
 
 (* future_result *)
 
@@ -176,7 +166,7 @@
 
     val schematic = exists is_schematic props;
     val immediate = is_none fork_pri;
-    val future = future_enabled 1;
+    val future = Future.proofs_enabled 1;
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
@@ -258,7 +248,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 ctxt))
-  else (if future_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
+  else (if Future.proofs_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
 
 fun prove_sorry_global thy xs asms prop tac =
   Drule.export_without_context
diff -r b73678836f8e -r 6fb85346cb79 src/Pure/par_tactical.ML
--- a/src/Pure/par_tactical.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/par_tactical.ML	Wed May 09 20:45:57 2018 +0200
@@ -46,7 +46,7 @@
       Drule.strip_imp_prems (Thm.cprop_of st)
       |> map (Thm.adjust_maxidx_cterm ~1);
   in
-    if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
+    if Future.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
       let
         fun try_goal g =
           (case SINGLE tac (Goal.init g) of