Re: [isabelle] Methods with informative failure messages

Thanks for the information so far.

To clarify: I am not hoping for a mechanism that gives useful information
when tacticals like + are used. I understand that that would be much to ask
for (e.g., if we have "a | b", and both fail, who's message should we

What I would like (and what I feel would be a very useful mechanism
generally, imagine the rule method actually telling us where in a large
term matching failed!) is the following:

   - Inside a tactical (like method+) that would succeed without adding
   error message (i.e., using no error message is output. (That's
   also why I don't want to use tracing, this would lead to spam in the output
   window when using tacticals.)
   - Inside a tactical that would fail, I don't care what is output (e.g.,
   the error message could be supressed).
   - If the method is used alone (i.e., apply method), then the user should
   see the error message.

I have a partial solution for this problem: I create a configuration flag
"method_error". If the user wants to get an explanation why a method fails,
then they use "using[[method_error=true]]", and then the method will fail
with an error. However, when using tacticals, it is important to switch
method_error off again. So it is a bit inconvenient.

The code used for this is simple:

val method_error = Attrib.setup_config_bool @{binding method_error} (K
fun error_ctac msg (ctx,_) = if Config.get ctx method_error
  then Seq.single (Seq.Error msg) else Seq.empty
fun error_tac msg ctx = if Config.get ctx method_error
  then K (raise ERROR(msg ())) else K Seq.empty
fun error_method msg = CONTEXT_METHOD (K (error_ctac msg))

Now a method or tactic can just use error_tac (or error_method) when it
usually would use no_tac.

But the problem is that the user only gets the error messages when
explicitly requesting them.

An alternative solution (that would need changes to Isabelle internals)
would be to use the Seq.Error solution without a flag, and to change the
behavior of tacticals that they filter errors suitably (I assume the logic
would be analogous to what how parser monads handle errors.) Makarius will
probably know best if that's a good idea or not.

Best wishes,

On 25 May 2018 at 14:09, Makarius <makarius at> wrote:

> 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
> information.
> 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.
>         Makarius

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