[isabelle-dev] NEWS: more informative errors in lazy enumerations

[Tobias Nipkow]

Am 17/10/2012 11:09, schrieb Makarius:
> *** ML ***
> 
> * Type Seq.results and related operations support embedded error
> messages within lazy enumerations, and thus allow to provide
> informative errors in the absence of any usable results.
> 
> 
> *** General ***
> 
> * More informative error messages for Isar proof commands involving
> lazy enumerations (method applications etc.).
> 
> 
> This refers to Isabelle/bd370af308f0.  The latter application means that the
> laconic "empty result sequence" should hardly ever happen again in practice --
> it depends on the proof command implementation how nice the error message
> becomes.  Some more hot spots of the system may be brushed up eventually, but
> note that plain tactics are inherently restricted to the classic failure and
> backtracking model without error messages.
> 

Excellent!

> Side remark:
> 
> Does anybody remember a use of the 'apply_end' command? Many years ago it was
> introduced to help analyse the failure of 'qed', in symmetry to 'apply' to break
> up 'proof' and 'by' steps.  That should now work without it, just by letting
> 'qed' crash and looking at the error message.  Of course, 'apply' has other uses
> and is not affected here.

I could never remember what apply_end was called and how to apply it although I
frequently needed it. I did a quick test of the new behaviour and it does indeed
seem to give the information that one really wants: which goals are left over
(although it may take some staring at the left overs to figure out where they
came from, but that was no better with apply_end). Hence I have no complaint if
apply_end goes.

Tobias

> Myself I've almost forgotten about 'apply_end', before constantly reminded of
> its existence by the Isabelle/jEdit completion, which proposes it when the user
> tries to write 'apply'.  So there is a clear motivation to get rid of the old
> 'apply_end' feature.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev