Re: [isabelle] Methods with informative failure messages

On 25/05/18 19:38, Peter Lammich wrote:
> you could return Seq.empty and print a warning or tracing message.

A proper tactic or proof method can't do that, for a variety of reasons.
Some of the semantic side-conditions for these very special (lazy)
operations are explained in "implementation" section 4.2 and 7.2.

Note that even non-lazy ML tools need to be careful about warnings and
tracings: it always needs to be guarded by some flags in the context, to
prevent spamming the user or bombing the system.

> On Fr, 2018-05-25 at 11:32 -0400, Dominique Unruh wrote:
>> I would like to implement a method that gives an informative error
>> message
>> when application fails (e.g., imagine an algebra tactic returning
>> "subgoal
>> should not contain <=" or something like that).
>> I see possibilities how a method can indicate a failure:
>>    - Raise an exception
>>    - Return a (Seq.Error (K "error message")) result.
>>    - Return Seq.empty (this is what is done by most methods)

An exception means a hard breakdown of something, and is indeed not part
of the normal tactic/method failure protocol.

Seq.empty is traditionally the only way, but without any further

Seq.Error and type context_tactic is relatively new -- it is a spin-off
from Eisbach. In principle it allows user-space proof methods to produce
information about failure, but there are presently no applications. This
mechanism is presently only used by the system in certain spots where
proof methods are incorporated into Isar proof commands (e.g. the
outermost steps of 'by').

>> Is there any best practice how to return informative messages on
>> method
>> failure?
>> I feel that this would be very helpful for the user of the method
>> because
>> often one has to do a lot of try and error to find out why a method
>> didn't
>> work on a given subgoal.

At some point I wanted to explore that for complex proof methods like
"induct" / "induction", which have many obscure failure points. I have
no idea how well it will work out.

Maybe someone else has tried something similar already.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.