# HG changeset patch
# User wenzelm
# Date 1363206308 -3600
# Node ID e5f9a6d9ca82e81c22e4d89299fa2e5c9ec8c297
# Parent  821a70e29e0b43878f7c638be44af1bde30ffb7b
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;

diff -r 821a70e29e0b -r e5f9a6d9ca82 etc/options
--- a/etc/options	Wed Mar 13 17:15:25 2013 +0100
+++ b/etc/options	Wed Mar 13 21:25:08 2013 +0100
@@ -51,8 +51,10 @@
   -- "level of tracing information for multithreading"
 option parallel_proofs : int = 2
   -- "level of parallel proof checking: 0, 1, 2"
-option parallel_proofs_threshold : int = 100
-  -- "threshold for sub-proof parallelization"
+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)"
 option parallel_proofs_reuse_timing : bool = true
   -- "reuse timing information from old log file for parallel proof scheduling"
 
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -91,8 +91,8 @@
   val status: transition -> Markup.T -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val approximative_id: transition -> {file: string, offset: int, name: string} option
-  val get_timing: transition -> Time.time
-  val put_timing: Time.time -> transition -> transition
+  val get_timing: transition -> Time.time option
+  val put_timing: Time.time option -> transition -> transition
   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
@@ -346,7 +346,7 @@
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
   no_timing: bool,           (*suppress timing*)
-  timing: Time.time,         (*prescient timing information*)
+  timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
 fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
@@ -356,7 +356,7 @@
 fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
   make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
+val empty = make_transition ("", Position.none, false, false, false, NONE, []);
 
 
 (* diagnostics *)
@@ -638,14 +638,12 @@
 local
 
 fun timing_message tr (t: Timing.timing) =
-  if Timing.is_relevant_time (#elapsed t) then
-    (case approximative_id tr of
-      SOME id =>
-        (Output.protocol_message
-          (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
-        handle Fail _ => ())
-    | NONE => ())
-  else ();
+  (case approximative_id tr of
+    SOME id =>
+      (Output.protocol_message
+        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
+      handle Fail _ => ())
+  | NONE => ());
 
 fun app int (tr as Transition {trans, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
@@ -727,29 +725,38 @@
 val get_result = Result.get o Proof.context_of;
 val put_result = Proof.map_context o Result.put;
 
-fun proof_future_enabled st =
+fun timing_estimate include_head elem =
+  let
+    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
+    val timings = map get_timing trs;
+  in
+    if forall is_some timings then
+      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
+    else NONE
+  end;
+
+fun priority NONE = ~1
+  | priority (SOME estimate) =
+      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+
+fun proof_future_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 ()
-        else Goal.future_enabled_nested 2));
-
-fun priority elem =
-  let
-    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem 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;
+        else
+          (case estimate of
+            NONE => Goal.future_enabled_nested 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
         setmp_thread_position tr (fn () =>
-          (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
+          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
             (fn () => command tr st); st)) ()
       else command tr st;
   in (Result (tr, st'), st') end;
@@ -757,12 +764,13 @@
 in
 
 fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
-  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
+  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
       let
         val (head_result, st') = atom_result head_tr st;
         val (body_elems, end_tr) = element_rest;
+        val estimate = timing_estimate false elem;
       in
-        if not (proof_future_enabled st')
+        if not (proof_future_enabled estimate st')
         then
           let
             val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
@@ -776,7 +784,7 @@
               (fn state =>
                 setmp_thread_position head_tr (fn () =>
                   Goal.fork_name "Toplevel.future_proof"
-                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
+                    (priority estimate)
                     (fn () =>
                       let
                         val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -243,7 +243,8 @@
         if Multithreading.max_threads_value () < 2
         then Multithreading.max_threads := 2 else ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
-        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
+        Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
+        Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
         tracing_messages := Options.int options "editor_tracing_messages"
       end);
 
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/System/session.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -94,7 +94,7 @@
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name doc_dump rpath level timing verbose max_threads trace_threads
-    parallel_proofs parallel_proofs_threshold =
+    parallel_proofs parallel_subproofs_saturation =
   ((fn () =>
     let
       val _ =
@@ -116,7 +116,7 @@
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
-    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
+    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
     |> Unsynchronized.setmp Multithreading.trace trace_threads
     |> Unsynchronized.setmp Multithreading.max_threads
       (if Multithreading.available then max_threads
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -17,7 +17,7 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
+  val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
@@ -174,7 +174,7 @@
 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, ...}) =
+fun join_proofs (Result {theory, id, ...}) =
   let
     val result1 = Exn.capture Thm.join_theory_proofs theory;
     val results2 = Future.join_results (Goal.peek_futures id);
@@ -351,7 +351,7 @@
 fun use_theories {last_timing, master_dir} imports =
   schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
+val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
 val use_thy = use_thys o single;
 
 
@@ -361,7 +361,7 @@
   let
     val {name = (name, _), imports, ...} = header;
     val _ = kill_thy name;
-    val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
+    val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
     val _ = Thy_Header.define_keywords header;
     val parents = map (get_theory o base_name o fst) imports;
   in Thy_Load.begin_theory master_dir header parents end;
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -22,7 +22,7 @@
   val use_ml: Path.T -> unit
   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 ->
+  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     Position.T -> string -> theory list -> theory * (unit -> unit) * int
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -17,7 +17,6 @@
   val parse_spans: Token.T list -> span list
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
-  val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
   val last_element: 'a element -> 'a
@@ -144,9 +143,6 @@
 fun element (a, b) = Element (a, SOME b);
 fun atom a = Element (a, NONE);
 
-fun fold_element f (Element (a, NONE)) = f a
-  | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
-
 fun map_element f (Element (a, NONE)) = Element (f a, NONE)
   | map_element f (Element (a, SOME (elems, b))) =
       Element (f a, SOME ((map o map_element) f elems, f b));
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/Tools/build.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -50,8 +50,10 @@
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
-        (Options.int options "parallel_proofs_threshold")
+    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
+        (Options.int options "parallel_subproofs_saturation")
+    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
+        (Options.real options "parallel_subproofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
@@ -99,10 +101,10 @@
       (case Symtab.lookup timings file of
         SOME offsets =>
           (case Inttab.lookup offsets offset of
-            SOME (name', time) => if name = name' then time else Time.zeroTime
-          | NONE => Time.zeroTime)
-      | NONE => Time.zeroTime)
-  | NONE => Time.zeroTime);
+            SOME (name', time) => if name = name' then SOME time else NONE
+          | NONE => NONE)
+      | NONE => NONE)
+  | NONE => NONE);
 
 in
 
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Pure/goal.ML	Wed Mar 13 21:25:08 2013 +0100
@@ -7,7 +7,8 @@
 signature BASIC_GOAL =
 sig
   val parallel_proofs: int Unsynchronized.ref
-  val parallel_proofs_threshold: int Unsynchronized.ref
+  val parallel_subproofs_saturation: int Unsynchronized.ref
+  val parallel_subproofs_threshold: real Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -32,6 +33,7 @@
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: 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
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -191,7 +193,8 @@
 (* scheduling parameters *)
 
 val parallel_proofs = Unsynchronized.ref 1;
-val parallel_proofs_threshold = Unsynchronized.ref 100;
+val parallel_subproofs_saturation = Unsynchronized.ref 100;
+val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
 
 fun future_enabled_level n =
   Multithreading.enabled () andalso ! parallel_proofs >= n andalso
@@ -201,7 +204,10 @@
 
 fun future_enabled_nested n =
   future_enabled_level n andalso
-  forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
+  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
+
+fun future_enabled_timing t =
+  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
 
 
 (* future_result *)
diff -r 821a70e29e0b -r e5f9a6d9ca82 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 17:15:25 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 21:25:08 2013 +0100
@@ -41,10 +41,10 @@
 {
   // FIXME avoid hard-wired stuff
   private val relevant_options =
-    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
-      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
-      "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
-      "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
+    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
+      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
+      "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
+      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
       "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
       "editor_update_delay", "editor_chart_delay")