[isabelle-dev] NEWS: more informative errors in lazy enumerations
nipkow at in.tum.de
Wed Oct 17 14:52:36 CEST 2012
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.
> 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
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev