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