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

[David Greenaway]

Hi all,

I have been locally testing out the current development snapshots of
Isabelle in anticipation of the Isabelle 2013 release. So far, most
things have been very smooth; thanks everyone for your hard work.

One minor problem I am hitting is the "Tracing paused" messages when
running proofs interactively. More precisely, when a tactic (or similar)
generates too much output using the "tracing" command, the following
message is displayed:

     Tracing paused.  Stop, or continue with next 10, 100, 1000 messages?

Clicking on one of the numbers listed in the message allows more tracing
messages to be displayed, and the tactic to continue.

While I can imagine this feature is useful when debugging unification or
simplification problems (to prevent jEdit from being flooded with
tracing messages), it is problematic when attempting to process large
proofs interactively.

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.

A second related problem is when multi-threaded tactics use tracing,
such as the following:

     ML {*
       Par_List.map (fn x => (tracing (PolyML.makestring x)))
           (1 upto 1000)
     *}

In these cases, the user must click "continue" once for each thread in
the system. (In my case, it requires 16 clicks, despite only having
4 cores).

Is there any way to avoid these two problems?

(I am currently running Isabelle revision '23ed79fc2b4d',
Thu Jan 17 23:00:20 2013 +0100)

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.