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

Hi Makarius,

The greyout happened again (with Isabelle2014-RC3). This time, I had typed

thm $

and placed the cursor at $, then opened Query/Find theorems and searched for simp_implies.

I've attached the activity log and the output of the syslog. The Prover.echo command still works. There are no exceptions in the shell from which I have started PIDE.

Hope this helps

On 09/08/14 13:17, Makarius wrote:
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.


Description: Zip archive

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