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

[Makarius]

On Fri, 18 Jan 2013, David Greenaway wrote:

> In particular, each time a complex tactic attempts to trace too much, 
> the proof stalls until the user manually brings the file to the 
> foreground in jEdit, finds the culprit statement, and then clicks one of 
> the "continue" buttons. (This potentially must be repeated several times 
> for each culprit statement, if the tracing output is several thousand 
> lines long.)
>
> For example, our proofs have quite a few commands which require complex 
> unifications, giving hundreds of messages from deep within Isabelle such 
> as:
>
>    Enter MATCH
>    λs x s a. x =?= λa x. ?P73 a x () ()
>    ...
>
> While the unification eventually succeeds, each such proof statement 
> requires human interaction in order to be processed.

I know about this snag, and I hope that it will not affect too many 
practical applications.  Aggressive unification with long traces does not 
happen so often.

On the other hand, I had such an incident somewhere in some library some 
months ago, and it was slowing down Isabelle/jEdit in a very odd way.  In 
the worst case it could also bomb it.

This observation has resulted in two refinements:

   * The limit for editor_tracing_messages that you have discovered already
     (which is also accesible in the jEdit plugin option dialog for Isabelle).

   * The funny interaction scheme within the document content to ask the
     user how to proceed.

Further refinements are imaginable.  For now I hope that the current 
scheme is sufficient for the release.


 	Makarius