[isabelle-dev] "Tracing paused" messages undesirably cause proofs running in background to stall
makarius at sketis.net
Sun Jan 20 15:13:59 CET 2013
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
> 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.
More information about the isabelle-dev