Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing



On Fri, 8 Aug 2014, Makarius wrote:

On Fri, 8 Aug 2014, Andreas Lochbihler wrote:

 When I use the Query and Sledgehammer panels heavily, PIDE regularly gets
 into a state where the theory text has a grey background, but I cannot get
 it to resume working any more (There is also no process running, the CPU
 is idle). The GUI itself is reactive, but I cannot get any feedback from
 Isabelle any more. The Syslog only shows the welcome message and Raw
 Output is empty. I then have to shut down jEdit and restart PIDE.

There must have been a protocol crash somewhere at the bottom. The next time when this happens, there are a few things that can be checked to pin it down more precisely:

  * jEdit menu Utilities / Troubleshooting / Activity Log for JVM
    exception traces -- if you run "isabelle jedit" on the command line
    there should be information on the terminal as well.

 * The following simple test of the ML/Scala protocol handler:

   - open Raw Output panel, to make it active before trying anything

   - open Console/Scala and emit this command:

       PIDE.session.protocol_command("Prover.echo", "test")

      The result "test" should appear on raw output.  This is the command
      loop of the prover process in PIDE wrapping.

Apart from a protocol crash, there might be non-termination in the protocol handler, e.g. because of problems to cancel old command transactions. Normally the protocol loop is detached from actual execution, though.

A "PIDE greyout" means that the important assign_update message is not received, e.g. due to heavy overloading, long GC, or actual breakdown of the ML side.

I am including a changeset for testing, which produces syslog messages about the critical protocol phases. This works via the "Syslog" panel, which is buffered and also restricted in size.


	Makarius
# HG changeset patch
# User wenzelm
# Date 1407582206 -7200
#      Sat Aug 09 13:03:26 2014 +0200
# Node ID 908f85843bf688f376e3621fb88d1bde804d0c0a
# Parent  9c361f94b3232d79dd7b4bbee79f1b288fbfba0c
test;

diff -r 9c361f94b323 -r 908f85843bf6 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sat Aug 09 11:43:58 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sat Aug 09 13:03:26 2014 +0200
@@ -53,6 +53,9 @@
   Isabelle_Process.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
+        fun syslog msg =
+          Output.physical_stderr (msg ^ " " ^ old_id_string ^ " " ^ new_id_string ^ "\n");
+
         val _ = Execution.discontinue ();
 
         val old_id = Document_ID.parse old_id_string;
@@ -78,9 +81,13 @@
                       list (pair int (pair string (list string))) c)]))
             end;
 
+        val _ = syslog "Document.update";
         val (removed, assign_update, state') = Document.update old_id new_id edits state;
+        val _ = syslog "Execution.terminate";
         val _ = List.app Execution.terminate removed;
+        val _ = syslog "Execution.purge";
         val _ = Execution.purge removed;
+        val _ = syslog "Isabelle_Process.reset_tracing";
         val _ = List.app Isabelle_Process.reset_tracing removed;
 
         val _ =
@@ -89,6 +96,8 @@
               let open XML.Encode
               in pair int (list (pair int (list int))) end
               |> YXML.string_of_body];
+
+        val _ = syslog "Document.start_execution";
       in Document.start_execution state' end));
 
 val _ =


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.