[isabelle-dev] blast warnings

[Lawrence Paulson]

There are two questions here:

(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.

(2) Should blast be able to handle that particular example? 
    I’m not convinced.It looks pretty artificial to me. Did it arise in a real application?

Larry

On 31 Dec 2013, at 10:11, Makarius <makarius at sketis.net> wrote:

> The following problem is still open: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-December/msg00138.html
> 
> Here is again the critical example that produces tons of messages:
> 
>  lemma "(!!P. P::bool) ==> PROP P" by blast
> 
> It should be tried out in "isabelle tty", to avoid bombing any non-trivial front-end (e.g. Isabelle/jEdit or batch build).
> 
> 
> We have had various situations in the past where friendly warnings caused a total failure of existence.  There are some measures againts that, like avoiding redundant messages in the first place, or guarding message output by Context_Position.if_visible (and making sure that the flag is maintained reliably, but this is often difficult).
> 
> In the case of blast this is not so obvious.  Maybe Larry can figure out why the proof reconstruction fails so badly.  Somehow strip_Trueprop might get involved: it looses the information about presence or absence of Trueprop.