[isabelle-dev] blast warnings

[Lawrence Paulson]

The point is that the claim is not a theorem, because it would need a contradiction rule in Pure. Note that auto, metis, etc. also fail.

One could consider modifying blast to forbid all variables of type prop. That may be overkill, however. I can’t think of a reason to devote much effort to handling this sort of example.

Larry

On 7 Jan 2014, at 23:32, Makarius <makarius at sketis.net> wrote:

> 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