[isabelle-dev] "Tracing paused" messages undesirably cause proofs running in background to stall

[David Greenaway]

On 21/01/13 23:08, Makarius wrote:
>> After inspecting the Isabelle source a little more, I have seen that
>> there is a jEdit configuration variable:
>>
>>   editor_tracing_messages
>>
>> that allows the pause threshold to be adjusted. Setting this value to
>> a large number solves my first problem.
>
> The question might be as simple as providing a good default.  In
> Isabelle2013-RC1 it is 100 messages, which is probably about low.  How
> about 1000?  Would that make your theories run through unhindered?

The longest unification-related tracing messages I witnessed in our
proofs were a little under 1500 lines (I saw three such cases). There
were tens of proofs producing between 100 and 1000 lines.

Testing on my own machine, viewing 10,000 lines of tracing output
appears to work without any problems. When I hit a little above the
30,000 mark though, I start to see strange behaviour where the output
buffer fails to display any output.

I think a value of at least 1000 would be a sensible default; I am not
sure what value between 1000 and 10,000 lines would be best, though.

Thanks so much,
David

--


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.