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 Andreas 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. Makarius
Description: Zip archive