ML statistics via external process: allows monitoring RTS while ML program sleeps;

--- a/src/Pure/Concurrent/future.ML	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 07 20:19:49 2020 +0200
@@ -17,7 +17,6 @@
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val ML_statistics: bool Unsynchronized.ref
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -168,31 +167,25 @@
   fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
 
 
-
-(* status *)
-
-val ML_statistics = Unsynchronized.ref false;
+(* ML statistics *)
 
-fun report_status () = (*requires SYNCHRONIZED*)
-  if ! ML_statistics then
-    let
-      val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
-      val workers_total = length (! workers);
-      val workers_active = count_workers Working;
-      val workers_waiting = count_workers Waiting;
-      val _ =
-        ML_Statistics.set
-         {tasks_ready = ready,
-          tasks_pending = pending,
-          tasks_running = running,
-          tasks_passive = passive,
-          tasks_urgent = urgent,
-          workers_total = workers_total,
-          workers_active = workers_active,
-          workers_waiting = workers_waiting};
-      val stats = ML_Statistics.get ();
-    in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
-  else ();
+fun ML_statistics () = (*requires SYNCHRONIZED*)
+  let
+    val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
+    val workers_total = length (! workers);
+    val workers_active = count_workers Working;
+    val workers_waiting = count_workers Waiting;
+  in
+    ML_Statistics.set
+     {tasks_ready = ready,
+      tasks_pending = pending,
+      tasks_running = running,
+      tasks_passive = passive,
+      tasks_urgent = urgent,
+      workers_total = workers_total,
+      workers_active = workers_active,
+      workers_waiting = workers_waiting}
+  end;
 
 
 (* cancellation primitives *)
@@ -286,7 +279,7 @@
 (* scheduler *)
 
 fun scheduler_end () = (*requires SYNCHRONIZED*)
-  (report_status (); scheduler := NONE);
+  (ML_statistics (); scheduler := NONE);
 
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
@@ -300,8 +293,8 @@
     val _ =
       if tick then Unsynchronized.change status_ticks (fn i => i + 1) else ();
     val _ =
-      if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 10) = 0
-      then report_status () else ();
+      if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 5) = 0
+      then ML_statistics () else ();
 
     val _ =
       if not tick orelse forall (Thread.isActive o #1) (! workers) then ()

--- a/src/Pure/ML/ml_process.scala	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Aug 07 20:19:49 2020 +0200
@@ -124,7 +124,7 @@
       val ml_options2 =
         if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
         else ml_options1 ::: List("--codepage", "utf8")
-      ml_options2
+      ml_options2 ::: List("--exportstats")
     }
 
     // bash

--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 07 20:19:49 2020 +0200
@@ -50,6 +50,45 @@
   }
 
 
+  /* protocol handler */
+
+  class Protocol_Handler extends Session.Protocol_Handler
+  {
+    private var session: Session = null
+    private var monitoring: Future[Unit] = Future.value(())
+
+    override def init(init_session: Session): Unit = synchronized
+    {
+      session = init_session
+    }
+
+    override def exit(): Unit = synchronized
+    {
+      session = null
+      monitoring.cancel
+    }
+
+    private def consume(props: Properties.T): Unit = synchronized
+    {
+      if (session != null && session.session_options.bool("ML_statistics")) {
+        session.runtime_statistics.post(Session.Runtime_Statistics(props))
+      }
+    }
+
+    private def ml_pid(msg: Prover.Protocol_Output): Boolean = synchronized
+    {
+      msg.properties match {
+        case Markup.ML_Pid(pid) =>
+          monitoring = Future.thread("ML_statistics") { monitor(pid, consume = consume) }
+          true
+        case _ => false
+      }
+    }
+
+    val functions = List(Markup.ML_Pid.name -> ml_pid)
+  }
+
+
   /* memory fields (mega bytes) */
 
   def mem_print(x: Long): Option[String] =

--- a/src/Pure/PIDE/markup.ML	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 07 20:19:49 2020 +0200
@@ -209,6 +209,7 @@
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
+  val ml_pid: int -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
@@ -672,6 +673,8 @@
 
 val functionN = "function"
 
+fun ml_pid pid = [(functionN, "ML_pid"), (idN, Value.print_int pid)];
+
 val commands_accepted = [(functionN, "commands_accepted")];
 
 val assign_update = [(functionN, "assign_update")];

--- a/src/Pure/PIDE/markup.scala	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 07 20:19:49 2020 +0200
@@ -569,13 +569,22 @@
 
   class Name_Function(name: String) extends Function(name)
   {
-    def unapply(props: Properties.T): Option[(String)] =
+    def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
+  object ML_Pid extends Function("ML_pid")
+  {
+    def unapply(props: Properties.T): Option[Long] =
+      props match {
+        case List(PROPERTY, (ID, Value.Long(pid))) => Some(pid)
+        case _ => None
+      }
+  }
+
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
 
   object Command_Timing extends Properties_Function("command_timing")

--- a/src/Pure/System/isabelle_process.ML	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 07 20:19:49 2020 +0200
@@ -113,6 +113,8 @@
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
+val _ = Session.protocol_handler "isabelle.ML_Statistics$Protocol_Handler";
+
 in
 
 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
@@ -199,6 +201,7 @@
 
     fun protocol () =
      (Session.init_protocol_handlers ();
+      Output.protocol_message (Markup.ml_pid (ML_PID.get ())) [];
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());
 
@@ -227,7 +230,6 @@
 
 fun init_options () =
  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
-  Future.ML_statistics := Options.default_bool "ML_statistics";
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";