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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev