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

On Thu, 20 Nov 2014, Peter Lammich wrote:

With Isabelle-2014 + jedit, I get grayouts every day. Some of them resolve themselves after a few seconds (up to a minute), one or two times a day I have to restart the IDE. It's annoying, but you get used to it :(

Getting used to problems means they are likely to remain indefinitely. It is important that users invest a minimum of time to figure out what is actually the situation and provide useful feedback on that.

I can only repeat that I am not aware of any such open problems in Isabelle2014. I need tangible reports to do anything to increase the general system quality again one step further.

Informal definition of "grayout": The text in the proof buffer becomes gray, and the prover is not responding any more. You can still edit the text.

This is correct, and just a normal consequence how PIDE works: the editor is always ready to accept edits, and sends them continously to the prover. The prover reports eventually on the results.

The aspect "not responding any more" is a delicate one. For example, garbage collection on the ML side or overloading with many long-running tasks could lead to seconds of delay, sometimes half a minute. This is normal and not an immediate problem. The situation can be improved by using an adequate machine (e.g. 4 cores and 8 GB is very little by today's standards).

Actual breakdown of the prover process is something else. The Syslog panel should show ML exeptions if anything like that has happened. By showing me that, I can figure out more. By keeping the information secret, chances for improvement are much diminished.


           925,412 people so far

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