1.1 --- a/Admin/Windows/Cygwin/isabelle/postinstall Fri Jan 18 20:01:59 2013 +0100
1.2 +++ b/Admin/Windows/Cygwin/isabelle/postinstall Fri Jan 18 20:31:22 2013 +0100
1.3 @@ -1,8 +1,12 @@
1.4 -#!/bin/dash
1.5 +#!/bin/bash
1.6
1.7 PATH=/bin
1.8
1.9 +CONTRIB="$(cygpath -u "$(cygpath -w /)\..")"
1.10 +peflags -x8192000 -z500 "$CONTRIB/polyml-5.5.0/x86-cygwin/poly.exe"
1.11 +
1.12 bash /etc/postinstall/base-files-mketc.sh.done
1.13
1.14 mkpasswd -l >/etc/passwd
1.15 mkgroup -l >/etc/group
1.16 +
2.1 --- a/Admin/Windows/Cygwin/isabelle/rebaseall Fri Jan 18 20:01:59 2013 +0100
2.2 +++ b/Admin/Windows/Cygwin/isabelle/rebaseall Fri Jan 18 20:31:22 2013 +0100
2.3 @@ -14,3 +14,4 @@
2.4 dash /bin/rebaseall -T "$FILE_LIST"
2.5
2.6 rm -f "$FILE_LIST"
2.7 +
3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:01:59 2013 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:31:22 2013 +0100
3.3 @@ -5445,7 +5445,7 @@
3.4 have *: "S Int closure T = S" using assms by auto
3.5 have "~(rel_interior S <= rel_frontier T)"
3.6 using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
3.7 - closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
3.8 + closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
3.9 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
3.10 using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
3.11 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure
4.1 --- a/src/Pure/Concurrent/future.ML Fri Jan 18 20:01:59 2013 +0100
4.2 +++ b/src/Pure/Concurrent/future.ML Fri Jan 18 20:31:22 2013 +0100
4.3 @@ -52,6 +52,7 @@
4.4 val peek: 'a future -> 'a Exn.result option
4.5 val is_finished: 'a future -> bool
4.6 val ML_statistics: bool Unsynchronized.ref
4.7 + val forked_proofs: int Unsynchronized.ref
4.8 val interruptible_task: ('a -> 'b) -> 'a -> 'b
4.9 val cancel_group: group -> unit
4.10 val cancel: 'a future -> unit
4.11 @@ -187,6 +188,7 @@
4.12 (* status *)
4.13
4.14 val ML_statistics = Unsynchronized.ref false;
4.15 +val forked_proofs = Unsynchronized.ref 0;
4.16
4.17 fun report_status () = (*requires SYNCHRONIZED*)
4.18 if ! ML_statistics then
4.19 @@ -197,6 +199,7 @@
4.20 val waiting = count_workers Waiting;
4.21 val stats =
4.22 [("now", signed_string_of_real (Time.toReal (Time.now ()))),
4.23 + ("tasks_proof", Markup.print_int (! forked_proofs)),
4.24 ("tasks_ready", Markup.print_int ready),
4.25 ("tasks_pending", Markup.print_int pending),
4.26 ("tasks_running", Markup.print_int running),
4.27 @@ -253,12 +256,11 @@
4.28 Task_Queue.running task (fn () =>
4.29 setmp_worker_task task (fn () =>
4.30 fold (fn job => fn ok => job valid andalso ok) jobs true) ());
4.31 - val _ = Multithreading.tracing 2 (fn () =>
4.32 - let
4.33 - val s = Task_Queue.str_of_task_groups task;
4.34 - fun micros time = string_of_int (Time.toNanoseconds time div 1000);
4.35 - val (run, wait, deps) = Task_Queue.timing_of_task task;
4.36 - in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
4.37 + val _ =
4.38 + if ! Multithreading.trace >= 2 then
4.39 + Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
4.40 + handle Fail msg => warning msg
4.41 + else ();
4.42 val _ = SYNCHRONIZED "finish" (fn () =>
4.43 let
4.44 val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
5.1 --- a/src/Pure/Concurrent/task_queue.ML Fri Jan 18 20:01:59 2013 +0100
5.2 +++ b/src/Pure/Concurrent/task_queue.ML Fri Jan 18 20:31:22 2013 +0100
5.3 @@ -22,7 +22,7 @@
5.4 val pri_of_task: task -> int
5.5 val str_of_task: task -> string
5.6 val str_of_task_groups: task -> string
5.7 - val timing_of_task: task -> Time.time * Time.time * string list
5.8 + val task_statistics: task -> Properties.T
5.9 val running: task -> (unit -> 'a) -> 'a
5.10 val joining: task -> (unit -> 'a) -> 'a
5.11 val waiting: task -> task list -> (unit -> 'a) -> 'a
5.12 @@ -114,14 +114,17 @@
5.13 name: string,
5.14 id: int,
5.15 pri: int option,
5.16 - timing: timing Synchronized.var option}
5.17 + timing: timing Synchronized.var option,
5.18 + pos: Position.T}
5.19 with
5.20
5.21 val dummy_task =
5.22 - Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
5.23 + Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
5.24 + pos = Position.none};
5.25
5.26 fun new_task group name pri =
5.27 - Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
5.28 + Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
5.29 + pos = Position.thread_data ()};
5.30
5.31 fun group_of_task (Task {group, ...}) = group;
5.32 fun name_of_task (Task {name, ...}) = name;
5.33 @@ -132,9 +135,6 @@
5.34
5.35 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
5.36
5.37 -fun timing_of_task (Task {timing, ...}) =
5.38 - (case timing of NONE => timing_start | SOME var => Synchronized.value var);
5.39 -
5.40 fun update_timing update (Task {timing, ...}) e =
5.41 uninterruptible (fn restore_attributes => fn () =>
5.42 let
5.43 @@ -147,6 +147,18 @@
5.44 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
5.45 prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
5.46
5.47 +fun task_statistics (Task {name, id, timing, pos, ...}) =
5.48 + let
5.49 + val (run, wait, wait_deps) =
5.50 + (case timing of NONE => timing_start | SOME var => Synchronized.value var);
5.51 + fun micros time = string_of_int (Time.toNanoseconds time div 1000);
5.52 + in
5.53 + [("now", signed_string_of_real (Time.toReal (Time.now ()))),
5.54 + ("task_name", name), ("task_id", Markup.print_int id),
5.55 + ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
5.56 + Position.properties_of pos
5.57 + end;
5.58 +
5.59 end;
5.60
5.61 structure Tasks = Table(type key = task val ord = task_ord);
6.1 --- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 20:01:59 2013 +0100
6.2 +++ b/src/Pure/ML/ml_statistics.scala Fri Jan 18 20:31:22 2013 +0100
6.3 @@ -43,7 +43,8 @@
6.4 ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
6.5
6.6 val tasks_fields =
6.7 - ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
6.8 + ("Future tasks",
6.9 + List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
6.10
6.11 val workers_fields =
6.12 ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
7.1 --- a/src/Pure/PIDE/markup.ML Fri Jan 18 20:01:59 2013 +0100
7.2 +++ b/src/Pure/PIDE/markup.ML Fri Jan 18 20:31:22 2013 +0100
7.3 @@ -134,6 +134,7 @@
7.4 val invoke_scala: string -> string -> Properties.T
7.5 val cancel_scala: string -> Properties.T
7.6 val ML_statistics: Properties.entry
7.7 + val task_statistics: Properties.entry
7.8 val loading_theory: string -> Properties.T
7.9 val dest_loading_theory: Properties.T -> string option
7.10 val no_output: Output.output * Output.output
7.11 @@ -412,6 +413,8 @@
7.12
7.13 val ML_statistics = (functionN, "ML_statistics");
7.14
7.15 +val task_statistics = (functionN, "task_statistics");
7.16 +
7.17 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
7.18
7.19 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
8.1 --- a/src/Pure/PIDE/markup.scala Fri Jan 18 20:01:59 2013 +0100
8.2 +++ b/src/Pure/PIDE/markup.scala Fri Jan 18 20:31:22 2013 +0100
8.3 @@ -330,6 +330,15 @@
8.4 case _ => None
8.5 }
8.6 }
8.7 +
8.8 + object Task_Statistics
8.9 + {
8.10 + def unapply(props: Properties.T): Option[Properties.T] =
8.11 + props match {
8.12 + case (FUNCTION, "task_statistics") :: stats => Some(stats)
8.13 + case _ => None
8.14 + }
8.15 + }
8.16 }
8.17
8.18
9.1 --- a/src/Pure/System/session.scala Fri Jan 18 20:01:59 2013 +0100
9.2 +++ b/src/Pure/System/session.scala Fri Jan 18 20:31:22 2013 +0100
9.3 @@ -364,6 +364,9 @@
9.4 case Markup.ML_Statistics(props) if output.is_protocol =>
9.5 statistics.event(Session.Statistics(props))
9.6
9.7 + case Markup.Task_Statistics(props) if output.is_protocol =>
9.8 + // FIXME
9.9 +
9.10 case _ if output.is_init =>
9.11 phase = Session.Ready
9.12
10.1 --- a/src/Pure/Tools/build.ML Fri Jan 18 20:01:59 2013 +0100
10.2 +++ b/src/Pure/Tools/build.ML Fri Jan 18 20:31:22 2013 +0100
10.3 @@ -19,13 +19,21 @@
10.4 else NONE
10.5 | ML_statistics _ _ = NONE;
10.6
10.7 +fun task_statistics (function :: stats) "" =
10.8 + if function = Markup.task_statistics then SOME stats
10.9 + else NONE
10.10 + | task_statistics _ _ = NONE;
10.11 +
10.12 fun protocol_message props output =
10.13 (case ML_statistics props output of
10.14 SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
10.15 | NONE =>
10.16 - (case Markup.dest_loading_theory props of
10.17 - SOME name => writeln ("\floading_theory = " ^ name)
10.18 - | NONE => raise Fail "Undefined Output.protocol_message"));
10.19 + (case task_statistics props output of
10.20 + SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
10.21 + | NONE =>
10.22 + (case Markup.dest_loading_theory props of
10.23 + SOME name => writeln ("\floading_theory = " ^ name)
10.24 + | NONE => raise Fail "Undefined Output.protocol_message")));
10.25
10.26
10.27 (* build *)
11.1 --- a/src/Pure/Tools/build.scala Fri Jan 18 20:01:59 2013 +0100
11.2 +++ b/src/Pure/Tools/build.scala Fri Jan 18 20:31:22 2013 +0100
11.3 @@ -561,14 +561,16 @@
11.4 private val SESSION_PARENT_PATH = "\fSession.parent_path = "
11.5
11.6
11.7 - sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
11.8 + sealed case class Log_Info(
11.9 + stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
11.10
11.11 def parse_log(text: String): Log_Info =
11.12 {
11.13 val lines = split_lines(text)
11.14 val stats = Props.parse_lines("\fML_statistics = ", lines)
11.15 + val tasks = Props.parse_lines("\ftask_statistics = ", lines)
11.16 val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
11.17 - Log_Info(stats, timing)
11.18 + Log_Info(stats, tasks, timing)
11.19 }
11.20
11.21
12.1 --- a/src/Pure/goal.ML Fri Jan 18 20:01:59 2013 +0100
12.2 +++ b/src/Pure/goal.ML Fri Jan 18 20:31:22 2013 +0100
12.3 @@ -116,9 +116,7 @@
12.4 Synchronized.change forked_proofs (fn (m, groups, tab) =>
12.5 let
12.6 val n = m + i;
12.7 - val _ =
12.8 - Multithreading.tracing 2 (fn () =>
12.9 - ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
12.10 + val _ = Future.forked_proofs := n;
12.11 in (n, groups, tab) end);
12.12
12.13 fun register_forked id future =
12.14 @@ -176,7 +174,7 @@
12.15
12.16 fun reset_futures () =
12.17 Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
12.18 - (groups, (0, [], Inttab.empty)));
12.19 + (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
12.20
12.21 end;
12.22