--- a/Admin/Windows/Cygwin/isabelle/postinstall Fri Jan 18 20:01:59 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/postinstall Fri Jan 18 20:31:22 2013 +0100
@@ -1,8 +1,12 @@
-#!/bin/dash
+#!/bin/bash
PATH=/bin
+CONTRIB="$(cygpath -u "$(cygpath -w /)\..")"
+peflags -x8192000 -z500 "$CONTRIB/polyml-5.5.0/x86-cygwin/poly.exe"
+
bash /etc/postinstall/base-files-mketc.sh.done
mkpasswd -l >/etc/passwd
mkgroup -l >/etc/group
+
--- a/Admin/Windows/Cygwin/isabelle/rebaseall Fri Jan 18 20:01:59 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall Fri Jan 18 20:31:22 2013 +0100
@@ -14,3 +14,4 @@
dash /bin/rebaseall -T "$FILE_LIST"
rm -f "$FILE_LIST"
+
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:01:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 20:31:22 2013 +0100
@@ -5445,7 +5445,7 @@
have *: "S Int closure T = S" using assms by auto
have "~(rel_interior S <= rel_frontier T)"
using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
- closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
+ closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure
--- a/src/Pure/Concurrent/future.ML Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Jan 18 20:31:22 2013 +0100
@@ -52,6 +52,7 @@
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val ML_statistics: bool Unsynchronized.ref
+ val forked_proofs: int Unsynchronized.ref
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -187,6 +188,7 @@
(* status *)
val ML_statistics = Unsynchronized.ref false;
+val forked_proofs = Unsynchronized.ref 0;
fun report_status () = (*requires SYNCHRONIZED*)
if ! ML_statistics then
@@ -197,6 +199,7 @@
val waiting = count_workers Waiting;
val stats =
[("now", signed_string_of_real (Time.toReal (Time.now ()))),
+ ("tasks_proof", Markup.print_int (! forked_proofs)),
("tasks_ready", Markup.print_int ready),
("tasks_pending", Markup.print_int pending),
("tasks_running", Markup.print_int running),
@@ -253,12 +256,11 @@
Task_Queue.running task (fn () =>
setmp_worker_task task (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
- val _ = Multithreading.tracing 2 (fn () =>
- let
- val s = Task_Queue.str_of_task_groups task;
- fun micros time = string_of_int (Time.toNanoseconds time div 1000);
- val (run, wait, deps) = Task_Queue.timing_of_task task;
- in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end);
+ val _ =
+ if ! Multithreading.trace >= 2 then
+ Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+ handle Fail msg => warning msg
+ else ();
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
--- a/src/Pure/Concurrent/task_queue.ML Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Fri Jan 18 20:31:22 2013 +0100
@@ -22,7 +22,7 @@
val pri_of_task: task -> int
val str_of_task: task -> string
val str_of_task_groups: task -> string
- val timing_of_task: task -> Time.time * Time.time * string list
+ val task_statistics: task -> Properties.T
val running: task -> (unit -> 'a) -> 'a
val joining: task -> (unit -> 'a) -> 'a
val waiting: task -> task list -> (unit -> 'a) -> 'a
@@ -114,14 +114,17 @@
name: string,
id: int,
pri: int option,
- timing: timing Synchronized.var option}
+ timing: timing Synchronized.var option,
+ pos: Position.T}
with
val dummy_task =
- Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE};
+ Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
+ pos = Position.none};
fun new_task group name pri =
- Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()};
+ Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
+ pos = Position.thread_data ()};
fun group_of_task (Task {group, ...}) = group;
fun name_of_task (Task {name, ...}) = name;
@@ -132,9 +135,6 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
-fun timing_of_task (Task {timing, ...}) =
- (case timing of NONE => timing_start | SOME var => Synchronized.value var);
-
fun update_timing update (Task {timing, ...}) e =
uninterruptible (fn restore_attributes => fn () =>
let
@@ -147,6 +147,18 @@
fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
+fun task_statistics (Task {name, id, timing, pos, ...}) =
+ let
+ val (run, wait, wait_deps) =
+ (case timing of NONE => timing_start | SOME var => Synchronized.value var);
+ fun micros time = string_of_int (Time.toNanoseconds time div 1000);
+ in
+ [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+ ("task_name", name), ("task_id", Markup.print_int id),
+ ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
+ Position.properties_of pos
+ end;
+
end;
structure Tasks = Table(type key = task val ord = task_ord);
--- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Jan 18 20:31:22 2013 +0100
@@ -43,7 +43,8 @@
("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
val tasks_fields =
- ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+ ("Future tasks",
+ List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
val workers_fields =
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
--- a/src/Pure/PIDE/markup.ML Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Jan 18 20:31:22 2013 +0100
@@ -134,6 +134,7 @@
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
+ val task_statistics: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
@@ -412,6 +413,8 @@
val ML_statistics = (functionN, "ML_statistics");
+val task_statistics = (functionN, "task_statistics");
+
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
--- a/src/Pure/PIDE/markup.scala Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/PIDE/markup.scala Fri Jan 18 20:31:22 2013 +0100
@@ -330,6 +330,15 @@
case _ => None
}
}
+
+ object Task_Statistics
+ {
+ def unapply(props: Properties.T): Option[Properties.T] =
+ props match {
+ case (FUNCTION, "task_statistics") :: stats => Some(stats)
+ case _ => None
+ }
+ }
}
--- a/src/Pure/System/session.scala Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/System/session.scala Fri Jan 18 20:31:22 2013 +0100
@@ -364,6 +364,9 @@
case Markup.ML_Statistics(props) if output.is_protocol =>
statistics.event(Session.Statistics(props))
+ case Markup.Task_Statistics(props) if output.is_protocol =>
+ // FIXME
+
case _ if output.is_init =>
phase = Session.Ready
--- a/src/Pure/Tools/build.ML Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Tools/build.ML Fri Jan 18 20:31:22 2013 +0100
@@ -19,13 +19,21 @@
else NONE
| ML_statistics _ _ = NONE;
+fun task_statistics (function :: stats) "" =
+ if function = Markup.task_statistics then SOME stats
+ else NONE
+ | task_statistics _ _ = NONE;
+
fun protocol_message props output =
(case ML_statistics props output of
SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
| NONE =>
- (case Markup.dest_loading_theory props of
- SOME name => writeln ("\floading_theory = " ^ name)
- | NONE => raise Fail "Undefined Output.protocol_message"));
+ (case task_statistics props output of
+ SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
+ | NONE =>
+ (case Markup.dest_loading_theory props of
+ SOME name => writeln ("\floading_theory = " ^ name)
+ | NONE => raise Fail "Undefined Output.protocol_message")));
(* build *)
--- a/src/Pure/Tools/build.scala Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/Tools/build.scala Fri Jan 18 20:31:22 2013 +0100
@@ -561,14 +561,16 @@
private val SESSION_PARENT_PATH = "\fSession.parent_path = "
- sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
+ sealed case class Log_Info(
+ stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
def parse_log(text: String): Log_Info =
{
val lines = split_lines(text)
val stats = Props.parse_lines("\fML_statistics = ", lines)
+ val tasks = Props.parse_lines("\ftask_statistics = ", lines)
val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
- Log_Info(stats, timing)
+ Log_Info(stats, tasks, timing)
}
--- a/src/Pure/goal.ML Fri Jan 18 20:01:59 2013 +0100
+++ b/src/Pure/goal.ML Fri Jan 18 20:31:22 2013 +0100
@@ -116,9 +116,7 @@
Synchronized.change forked_proofs (fn (m, groups, tab) =>
let
val n = m + i;
- val _ =
- Multithreading.tracing 2 (fn () =>
- ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
+ val _ = Future.forked_proofs := n;
in (n, groups, tab) end);
fun register_forked id future =
@@ -176,7 +174,7 @@
fun reset_futures () =
Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
- (groups, (0, [], Inttab.empty)));
+ (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
end;