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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
