join all proofs before scheduling present phase (ordered according to weight);
authorwenzelm
Mon Mar 04 11:36:16 2013 +0100 (2013-03-04 ago)
changeset 51331e7fab0b5dbe7
parent 51330 f249bd08d851
child 51332 8707df0b0255
join all proofs before scheduling present phase (ordered according to weight);
tuned;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon Mar 04 10:02:58 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Mar 04 11:36:16 2013 +0100
     1.3 @@ -165,10 +165,21 @@
     1.4  (* scheduling loader tasks *)
     1.5  
     1.6  datatype result =
     1.7 -  Result of {theory: theory, id: serial, present: unit future, commit: unit -> unit};
     1.8 +  Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
     1.9 +
    1.10 +fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
    1.11  
    1.12  fun result_theory (Result {theory, ...}) = theory;
    1.13 -fun theory_result theory = Result {theory = theory, id = 0, present = Future.value (), commit = I};
    1.14 +fun result_present (Result {present, ...}) = present;
    1.15 +fun result_commit (Result {commit, ...}) = commit;
    1.16 +fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
    1.17 +
    1.18 +fun join_proofs (Result {theory, id, present, ...}) =
    1.19 +  let
    1.20 +    val result1 = Exn.capture Thm.join_theory_proofs theory;
    1.21 +    val results2 = Future.join_results (Goal.peek_futures id);
    1.22 +  in result1 :: results2 end;
    1.23 +
    1.24  
    1.25  datatype task =
    1.26    Task of string list * (theory list -> result) |
    1.27 @@ -181,24 +192,21 @@
    1.28  
    1.29  local
    1.30  
    1.31 -fun finish_thy (Result {theory, id, present, commit}) =
    1.32 -  let
    1.33 -    val result1 = Exn.capture Thm.join_theory_proofs theory;
    1.34 -    val results2 = Future.join_results (Goal.peek_futures id);
    1.35 -    val result3 = Future.join_result present;
    1.36 -    val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
    1.37 -    val _ = commit ();
    1.38 -  in theory end;
    1.39 -
    1.40  val schedule_seq =
    1.41    String_Graph.schedule (fn deps => fn (_, task) =>
    1.42      (case task of
    1.43 -      Task (parents, body) => finish_thy (body (task_parents deps parents))
    1.44 +      Task (parents, body) =>
    1.45 +        let
    1.46 +          val result = body (task_parents deps parents);
    1.47 +          val _ = Par_Exn.release_all (join_proofs result);
    1.48 +          val _ = result_present result ();
    1.49 +          val _ = result_commit result ();
    1.50 +        in result_theory result end
    1.51      | Finished thy => thy)) #> ignore;
    1.52  
    1.53  val schedule_futures = uninterruptible (fn _ => fn tasks =>
    1.54    let
    1.55 -    val results1 = tasks
    1.56 +    val futures = tasks
    1.57        |> String_Graph.schedule (fn deps => fn (name, task) =>
    1.58          (case task of
    1.59            Task (parents, body) =>
    1.60 @@ -211,13 +219,27 @@
    1.61                  | bad =>
    1.62                      error (loader_msg ("failed to load " ^ quote name ^
    1.63                        " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    1.64 -        | Finished theory => Future.value (theory_result theory)))
    1.65 -      |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
    1.66 +        | Finished theory => Future.value (theory_result theory)));
    1.67 +
    1.68 +    val results1 = futures
    1.69 +      |> maps (fn future =>
    1.70 +          (case Future.join_result future of
    1.71 +            Exn.Res result => join_proofs result
    1.72 +          | Exn.Exn exn => [Exn.Exn exn]));
    1.73 +
    1.74 +    val results2 = futures
    1.75 +      |> map_filter (Exn.get_res o Future.join_result)
    1.76 +      |> sort result_ord
    1.77 +      |> Par_List.map (fn result => Exn.capture (result_present result) ());
    1.78 +
    1.79 +    (* FIXME more precise commit order (!?) *)
    1.80 +    val results3 = futures
    1.81 +      |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
    1.82  
    1.83      (* FIXME avoid global reset_futures (!??) *)
    1.84 -    val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
    1.85 +    val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
    1.86  
    1.87 -    val _ = Par_Exn.release_all (rev (results2 @ results1));
    1.88 +    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
    1.89    in () end);
    1.90  
    1.91  in
    1.92 @@ -253,11 +275,11 @@
    1.93  
    1.94      val id = serial ();
    1.95      val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
    1.96 -    val (theory, present) =
    1.97 +    val (theory, present, weight) =
    1.98        Thy_Load.load_thy last_timing update_time dir header text_pos text
    1.99          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   1.100      fun commit () = update_thy deps theory;
   1.101 -  in Result {theory = theory, id = id, present = present, commit = commit} end;
   1.102 +  in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
   1.103  
   1.104  fun check_deps dir name =
   1.105    (case lookup_deps name of
     2.1 --- a/src/Pure/Thy/thy_load.ML	Mon Mar 04 10:02:58 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Mar 04 11:36:16 2013 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4    val exec_ml: Path.T -> generic_theory -> generic_theory
     2.5    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     2.6    val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
     2.7 -    Position.T -> string -> theory list -> theory * unit future
     2.8 +    Position.T -> string -> theory list -> theory * (unit -> unit) * int
     2.9    val set_master_path: Path.T -> unit
    2.10    val get_master_path: unit -> Path.T
    2.11  end;
    2.12 @@ -258,19 +258,18 @@
    2.13      val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
    2.14      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    2.15  
    2.16 -    val present =
    2.17 -      Future.flat results |> Future.map (fn res0 =>
    2.18 -        let
    2.19 -          val res = filter_out (Toplevel.is_ignored o #1) res0;
    2.20 -          val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
    2.21 -        in
    2.22 -          Thy_Output.present_thy minor Keyword.command_tags
    2.23 -            (Outer_Syntax.is_markup outer_syntax) res toks
    2.24 -          |> Buffer.content
    2.25 -          |> Present.theory_output name
    2.26 -        end);
    2.27 +    fun present () =
    2.28 +      let
    2.29 +        val res = filter_out (Toplevel.is_ignored o #1) (flat (Future.joins results));
    2.30 +        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
    2.31 +      in
    2.32 +        Thy_Output.present_thy minor Keyword.command_tags
    2.33 +          (Outer_Syntax.is_markup outer_syntax) res toks
    2.34 +        |> Buffer.content
    2.35 +        |> Present.theory_output name
    2.36 +      end;
    2.37  
    2.38 -  in (thy, present) end;
    2.39 +  in (thy, present, size text) end;
    2.40  
    2.41  
    2.42  (* document antiquotation *)