refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
authorwenzelm
Mon Mar 04 15:03:46 2013 +0100 (2013-03-04 ago)
changeset 513328707df0b0255
parent 51331 e7fab0b5dbe7
child 51333 2cfd028a2fd9
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/System/isabelle_process.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Mar 04 11:36:16 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Mar 04 15:03:46 2013 +0100
     1.3 @@ -1191,7 +1191,7 @@
     1.4  in
     1.5  
     1.6  fun local_future_terminal_proof meths =
     1.7 -  future_terminal_proof 2
     1.8 +  future_terminal_proof 3
     1.9      (local_terminal_proof meths)
    1.10      (local_terminal_proof meths #> context_of) local_done_proof;
    1.11  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 04 11:36:16 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 04 15:03:46 2013 +0100
     2.3 @@ -96,8 +96,9 @@
     2.4    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     2.5    val command_errors: bool -> transition -> state -> Runtime.error list * state option
     2.6    val command_exception: bool -> transition -> state -> state
     2.7 -  val element_result: transition Thy_Syntax.element -> state ->
     2.8 -    (transition * state) list future * state
     2.9 +  type result
    2.10 +  val join_results: result -> (transition * state) list
    2.11 +  val element_result: transition Thy_Syntax.element -> state -> result * state
    2.12  end;
    2.13  
    2.14  structure Toplevel: TOPLEVEL =
    2.15 @@ -705,19 +706,26 @@
    2.16  
    2.17  (* scheduled proof result *)
    2.18  
    2.19 +datatype result =
    2.20 +  Result of transition * state |
    2.21 +  Result_List of result list |
    2.22 +  Result_Future of result future;
    2.23 +
    2.24 +fun join_results (Result x) = [x]
    2.25 +  | join_results (Result_List xs) = maps join_results xs
    2.26 +  | join_results (Result_Future x) = join_results (Future.join x);
    2.27 +
    2.28  local
    2.29  
    2.30  structure Result = Proof_Data
    2.31  (
    2.32 -  type T = (transition * state) list future;
    2.33 -  val empty: T = Future.value [];
    2.34 +  type T = result;
    2.35 +  val empty: T = Result_List [];
    2.36    fun init _ = empty;
    2.37  );
    2.38  
    2.39 -fun done_proof state =
    2.40 -  if can (Proof.assert_bottom true) state
    2.41 -  then Proof.global_done_proof state
    2.42 -  else Proof.context_of (Proof.local_done_proof state);
    2.43 +val get_result = Result.get o Proof.context_of;
    2.44 +val put_result = Proof.map_context o Result.put;
    2.45  
    2.46  fun proof_future_enabled st =
    2.47    (case try proof_of st of
    2.48 @@ -744,46 +752,52 @@
    2.49            (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    2.50              (fn () => command tr st); st)) ()
    2.51        else command tr st;
    2.52 -  in ((tr, st'), st') end;
    2.53 +  in (Result (tr, st'), st') end;
    2.54  
    2.55  in
    2.56  
    2.57 -fun element_result (Thy_Syntax.Element (tr, NONE)) st =
    2.58 -      let val (result, st') = atom_result tr st
    2.59 -      in (Future.value [result], st') end
    2.60 -  | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
    2.61 +fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
    2.62 +  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    2.63        let
    2.64          val (head_result, st') = atom_result head_tr st;
    2.65 -        val (body_elems, end_tr) = proof;
    2.66 -        val body_trs = maps Thy_Syntax.flat_element body_elems;
    2.67 +        val (body_elems, end_tr) = element_rest;
    2.68        in
    2.69          if not (proof_future_enabled st')
    2.70          then
    2.71 -          let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
    2.72 -          in (Future.value (head_result :: proof_results), st'') end
    2.73 +          let
    2.74 +            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    2.75 +            val (proof_results, st'') = fold_map atom_result proof_trs st';
    2.76 +          in (Result_List (head_result :: proof_results), st'') end
    2.77          else
    2.78            let
    2.79              val finish = Context.Theory o Proof_Context.theory_of;
    2.80  
    2.81              val future_proof = Proof.future_proof
    2.82 -              (fn prf =>
    2.83 +              (fn state =>
    2.84                  setmp_thread_position head_tr (fn () =>
    2.85                    Goal.fork_name "Toplevel.future_proof"
    2.86 -                    (priority (Thy_Syntax.Element (empty, SOME proof)))
    2.87 +                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
    2.88                      (fn () =>
    2.89 -                      let val (result, result_state) =
    2.90 -                        (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    2.91 -                          => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    2.92 -                        |> fold_map atom_result body_trs ||> command end_tr;
    2.93 -                      in (result, presentation_context_of result_state) end)) ())
    2.94 -              #> (fn (result, state') => state' |> done_proof |> Result.put result);
    2.95 +                      let
    2.96 +                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    2.97 +                        val prf' = Proof_Node.apply (K state) prf;
    2.98 +                        val (result, result_state) =
    2.99 +                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
   2.100 +                          |> fold_map element_result body_elems ||> command end_tr;
   2.101 +                      in (Result_List result, presentation_context_of result_state) end)) ())
   2.102 +              #> (fn (res, state') => state' |> put_result (Result_Future res));
   2.103 +
   2.104 +            val forked_proof =
   2.105 +              proof (future_proof #>
   2.106 +                (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
   2.107 +              end_proof (fn _ => future_proof #>
   2.108 +                (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
   2.109  
   2.110              val st'' = st'
   2.111 -              |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
   2.112 +              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
   2.113 +            val end_result = Result (end_tr, st'');
   2.114              val result =
   2.115 -              Result.get (presentation_context_of st'')
   2.116 -              |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
   2.117 -
   2.118 +              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
   2.119            in (result, st'') end
   2.120        end;
   2.121  
     3.1 --- a/src/Pure/System/isabelle_process.ML	Mon Mar 04 11:36:16 2013 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Mar 04 15:03:46 2013 +0100
     3.3 @@ -242,7 +242,7 @@
     3.4          Multithreading.max_threads := Options.int options "threads";
     3.5          if Multithreading.max_threads_value () < 2
     3.6          then Multithreading.max_threads := 2 else ();
     3.7 -        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
     3.8 +        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
     3.9          Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
    3.10          tracing_messages := Options.int options "editor_tracing_messages"
    3.11        end);
     4.1 --- a/src/Pure/Thy/thy_load.ML	Mon Mar 04 11:36:16 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Mar 04 15:03:46 2013 +0100
     4.3 @@ -260,7 +260,7 @@
     4.4  
     4.5      fun present () =
     4.6        let
     4.7 -        val res = filter_out (Toplevel.is_ignored o #1) (flat (Future.joins results));
     4.8 +        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
     4.9          val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
    4.10        in
    4.11          Thy_Output.present_thy minor Keyword.command_tags