[isabelle-dev] blast warnings

[Makarius]

On Tue, 31 Dec 2013, Lawrence Paulson wrote:

> (1) Do we need a general way to prevent warnings from breaking 
> interfaces? That would be great, if possible, and maybe just requires 
> inserting some sort of pause between messages to allow their 
> interruption, or some way to count messages and stop them after a limit 
> is exceeded.

Already since 2001 we have the Output.tracing channel, which is intended 
for potentially unbounded and usually less interesting high-volume output, 
with some special treatment in the front-end. That was originally done for 
Proof General.

The current Isabelle/jEdit implementation of that stops emitting tracing 
messages after the limit given by system option editor_tracing_messages is 
exceeded (for each command transaction separately).  Afterwards it waits 
for the user clicking on the output to stop or continue.  This is a bit 
awkward, but avoids bombing the front-end.  Although sometimes surprises 
remain about executions that should continue, but actually wait.


I have now modernized blast.ML a bit, to warp it from 1997 into 2001 in 
that respect.  See also Isabelle/ed36358c20d5.

You can try it like this:

   setup {* Config.put_global Blast.trace true *}

   lemma "(⋀P. P::bool) ⟹ PROP P" by blast

With Blast.trace = false, that example loops without emitting anything, 
just some ambient heating via CPU power.  Bombing no longer happens in 
that version.  I have also made one separate warning subject to context 
visibility, which is quite common these days.

So for my part, the issue is resolved.  You should nonetheless take a look 
if it is possible to get the treatment of Trueprop vs. non-Trueprop right. 
If the left-over development tool of Blast.trace is of any use, it should 
point out the situation.  (In general, cumulative maintenance costs over 
the years are greatly reduced by removing built-in tracing once things are 
properly implemented.  Such add-ons greatly complicate the code and are 
hard to get right in the first place.)


 	Makarius