Re: [isabelle] Methods with informative failure messages


you could return Seq.empty and print a warning or tracing message.
However, note that in combination with tacticals (like ?,*), your
method might fail multiple times on different goals and produce a whole
bunch of warning messages ... many of them might be useless, but I
don't think there is a general rule to filter the actual informative
ones ...


On Fr, 2018-05-25 at 11:32 -0400, Dominique Unruh wrote:
> Hi,
> 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)
> According to my experiments, the first two options are not suitable
> because
> they break method combinators like "method+" and "method?" (I would
> need
> that these will suppress the error.) And the third option does not
> support
> giving an error message.
> 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.
> Best wishes,
> Dominique.

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