Re: [isabelle] Isabelle2016-RC2 JEdit lockup with Java at 100% CPU (was: Re: Isabelle2016-RC2 Java exceptions related to search/replace)



Sorry about the subject mess-up.  I don't know how that happened.
I changed the subject for this follow-up -- I hope I did it in a reasonable way.

I have not changed any throttling options.

The "Enter MATCH ..." messages are produced in reasonably frequent situations when
I invoke Sledgehammer by typing "try" into the main edit window.  I was aware that
they were usually throttled, but in this situation it seemed that they were not.
So maybe there is some way that the throttling gets circumvented in some situations.

								- Gene Stark

On 01/31/2016 05:27 PM, Makarius wrote:
> On Sun, 31 Jan 2016, Eugene W. Stark wrote:
> 
>> I was able to recreate the situation when I reloaded the same files,
>> both on Isabelle2016-RC2 and -RC1.
>>
>> The situation seemed to be triggered by "Enter MATCH..." spew spamming
>> the output window.  Apparently there was enough of it so that it filled
>> the JVM heap and perhaps caused continuous GC (speculation).
>> Eventually, poly became quiescent and presumably stopped sending output
> 
> I guess it actually refers to the thread "JEdit lockup with Java at 100% CPU".
> 
> Since "Enter MATCH ..." is a formal "tracing" message, it should be throttled according to system option
> editor_tracing_messages (default 1000), which is accessible in Plugin Options / Isabelle / General.
> 
> Did you change that option?
> 
> 
> Another question is where these masses of "Enter MATCH ..." messages are produced. It is normally some bad situation
> that can be avoided.
> 
> 
>     Makarius





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