Email Gateway (Aug 22 2022 at 17:22): Email Gateway (Aug 22 2022 at 17:22):From: Dominique Unruh <unruh@ut.ee>
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.
Email Gateway (Aug 22 2022 at 17:22):From: Peter Lammich <lammich@in.tum.de>
Hi,
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 ...
Email Gateway (Aug 22 2022 at 17:22):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 17:22):From: Dominique Unruh <unruh@ut.ee>
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
output).
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 Seq.fail) 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
false)
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,
Dominique.
Last updated: Apr 19 2024 at 12:27 UTC